noncomputable def Matroid.IsBase.coords {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) (e : α) : Finset ↑B

The intersection of M.fundCircuit e B with B as a Finset B in a finitary matroid.

Equations

• hB.coords e = ⋯.toFinset

theorem Matroid.IsBase.coords_of_mem {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) (he : e ∈ B) : hB.coords e = {⟨e, he⟩}

theorem Matroid.IsBase.coords_of_notMem_ground {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) (heE : e ∉ M.E) : hB.coords e = ∅

theorem Matroid.IsBase.coords_toSet {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) : ↑(hB.coords e) = Subtype.val ⁻¹' M.fundCircuit e B

theorem Matroid.IsBase.fundCircuit_eq_insert_map {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] [DecidableEq α] (hB : M.IsBase B) : M.fundCircuit e B = ↑(insert e (Finset.map (Function.Embedding.setSubtype B) (hB.coords e)))

noncomputable def Matroid.IsBase.fundCoord {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) (R : Type u_7) [Semiring R] (e : α) : ↑B →₀ R

The column of the B-fundamental matrix of M corresponding to e, as a Finsupp.

Equations

• hB.fundCoord R e = Finsupp.indicator (hB.coords e) fun (x : ↑B) (x_1 : x ∈ hB.coords e) => 1

theorem Matroid.IsBase.fundCoord_of_mem {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) (he : e ∈ B) : hB.fundCoord R e = Finsupp.single ⟨e, he⟩ 1

@[simp]

theorem Matroid.IsBase.fundCoord_mem {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) (e : ↑B) : hB.fundCoord R ↑e = Finsupp.single e 1

theorem Matroid.IsBase.fundCoord_of_notMem_ground {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) (he : e ∉ M.E) : hB.fundCoord R e = 0

theorem Matroid.IsBase.support_fundCoord_subset {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) : Function.support (hB.fundCoord R) ⊆ M.E

theorem Matroid.IsBase.fundCoord_support {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) : Subtype.val '' ↑(hB.fundCoord R e).support = M.fundCircuit e B ∩ B

theorem Matroid.IsBase.mem_fundCoord_support {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) (e : ↑B) {f : α} : e ∈ (hB.fundCoord R f).support ↔ ↑e ∈ M.fundCircuit f B

theorem Matroid.IsBase.fundCoord_isBase {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) : (Matroid.ofFun R M.E (hB.fundCoord R)).IsBase B

theorem Matroid.IsBase.fundCoord_eq_linearCombination {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) : hB.fundCoord R e = (Finsupp.linearCombination R fun (x : ↑B) => Finsupp.single x 1) (hB.fundCoord R e)

theorem Matroid.IsBase.fundCoord_isStandard {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) (R : Type u_8) [DivisionRing R] : (repOfFun R M.E (hB.fundCoord R)).IsStandard

theorem Matroid.fundCoord_fundCircuit {α : Type u_1} {e : α} {B : Set α} {M : Matroid α} [M.Finitary] {R : Type u_7} [DivisionRing R] (hB : M.IsBase B) (heB : e ∉ B) (heE : e ∈ M.E) : (Matroid.ofFun R M.E (hB.fundCoord R)).IsCircuit (M.fundCircuit e B)

theorem Matroid.IsBase.fundCoord_row_support {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) (R : Type u_8) [DivisionRing R] (e : ↑B) : (Function.support fun (x : α) => (hB.fundCoord R x) e) = M.fundCocircuit (↑e) B