noncomputable def Matroid.Rep.cycleSpace {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : Submodule 𝔽 (α →₀ 𝔽)

The cycleSpace of an 𝔽-representation v of M : Matroid α is the set of vectors in α →₀ 𝔽 that are supported on a finite subset of M.E and give a linear combination of zero with the elements of v. This space contains a vector supported on every circuit. This is the right null space of a matrix representation of M.

Equations

• v.cycleSpace = (Finsupp.linearCombination 𝔽 ⇑v).ker ⊓ Finsupp.supported 𝔽 𝔽 M.E

noncomputable def Matroid.Rep.supportedCycleSpace {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : Submodule 𝔽 ↥(Finsupp.supported 𝔽 𝔽 M.E)

supportedCycleSpace is the cycle space as a subspace of Finsupp.supported 𝔽 𝔽 M.E.

Equations

• v.supportedCycleSpace = (Finsupp.linearCombinationOn α W 𝔽 (⇑v) M.E).ker

theorem Matroid.Rep.supported_finiteDimensional {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.Finite] : ∀ (x : M.Rep 𝔽 W), FiniteDimensional 𝔽 ↥(Finsupp.supported 𝔽 𝔽 M.E)

theorem Matroid.Rep.mem_cycleSpace_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {c : α →₀ 𝔽} (v : M.Rep 𝔽 W) : c ∈ v.cycleSpace ↔ (Finsupp.linearCombination 𝔽 ⇑v) c = 0 ∧ Function.support ⇑c ⊆ M.E

theorem Matroid.Rep.mem_supportedCycleSpace_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {c : ↥(Finsupp.supported 𝔽 𝔽 M.E)} : c ∈ v.supportedCycleSpace ↔ (Finsupp.linearCombination 𝔽 ⇑v) ↑c = 0

theorem Matroid.Rep.support_subset_ground_of_mem_cycleSpace {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {c : α →₀ 𝔽} (v : M.Rep 𝔽 W) (hc : c ∈ v.cycleSpace) : Function.support ⇑c ⊆ M.E

noncomputable def Matroid.Rep.cycleSpaceEquiv {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : ↥v.cycleSpace ≃ₗ[𝔽] ↥v.supportedCycleSpace

Equations

• v.cycleSpaceEquiv = { toFun := fun (x : ↥v.cycleSpace) => ⟨⟨↑x, ⋯⟩, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : ↥v.supportedCycleSpace) => ⟨↑↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Matroid.Rep.cycleSpaceEquiv_apply_coe_coe {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (x : ↥v.cycleSpace) : ↑↑(v.cycleSpaceEquiv x) = ↑x

@[simp]

theorem Matroid.Rep.cycleSpaceEquiv_symm_apply_coe {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (x : ↥v.supportedCycleSpace) : ↑(v.cycleSpaceEquiv.symm x) = ↑↑x

@[instance_reducible]

noncomputable instance Matroid.Rep.supportedCycleSpace.addCommGroup {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : AddCommGroup ↥v.supportedCycleSpace

Nested Submodule carriers do not get AddCommGroup by instance search; provide it.

Equations

• Matroid.Rep.supportedCycleSpace.addCommGroup v = v.supportedCycleSpace.addCommGroup

instance Matroid.Rep.cycleSpace_finiteDimensional {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.Finite] (v : M.Rep 𝔽 W) : FiniteDimensional 𝔽 ↥v.cycleSpace

instance Matroid.Rep.supportedCycleSpace_finiteDimensional' {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.Finite] (v : M.Rep 𝔽 W) : FiniteDimensional 𝔽 ↥v.supportedCycleSpace

@[simp]

theorem Matroid.Rep.supportedCycleSpace_comp {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (φ : W →ₗ[𝔽] W') (hφ : Disjoint (Submodule.span 𝔽 (Set.range ⇑v)) φ.ker) : (v.comp φ hφ).supportedCycleSpace = v.supportedCycleSpace

@[simp]

theorem Matroid.Rep.cycleSpace_comp {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (φ : W →ₗ[𝔽] W') (hφ : Disjoint (Submodule.span 𝔽 (Set.range ⇑v)) φ.ker) : (v.comp φ hφ).cycleSpace = v.cycleSpace

@[simp]

theorem Matroid.Rep.cycleSpace_comp' {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (φ : W →ₗ[𝔽] W') (hφ : φ.ker = ⊥) : (v.comp' φ hφ).cycleSpace = v.cycleSpace

@[simp]

theorem Matroid.Rep.cycleSpace_compEquiv {α : Type u_1} {W : Type u_3} {W' : Type u_4} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [AddCommGroup W'] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (φ : W ≃ₗ[𝔽] W') : (v.compEquiv φ).cycleSpace = v.cycleSpace

@[simp]

theorem Matroid.Rep.restrictSpan_cycleSpace {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : v.restrictSpan.cycleSpace = v.cycleSpace

@[simp]

theorem Matroid.Rep.standardRep'_cycleSpace {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {B : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hB : M.IsBase B) : (v.standardRep' hB).cycleSpace = v.cycleSpace

@[simp]

theorem Matroid.Rep.standardRep_cycleSpace {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {B : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hB : M.IsBase B) : (v.standardRep hB).cycleSpace = v.cycleSpace

theorem Matroid.Rep.cyclic_of_linearCombination {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (c : α →₀ 𝔽) (hcE : ↑c.support ⊆ M.E) (hcv : (Finsupp.linearCombination 𝔽 ⇑v) c = 0) : M.Cyclic ↑c.support

If some linear combination of columns of M.E is zero, the nonzero indices form a cyclic set.

theorem Matroid.Rep.support_cyclic_of_mem_cycleSpace {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {c : α →₀ 𝔽} (hc : c ∈ v.cycleSpace) : M.Cyclic ↑c.support

theorem Matroid.Rep.exists_finsupp_of_isCircuit {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {C : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hC : M.IsCircuit C) : ∃ (c : α →₀ 𝔽), ↑c.support = C ∧ (Finsupp.linearCombination 𝔽 ⇑v) c = 0

theorem Matroid.Rep.exists_mem_cycleSpace_of_isCircuit {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {C : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hC : M.IsCircuit C) : ∃ w ∈ v.cycleSpace, ↑w.support = C

noncomputable def Matroid.Finsupp.dualFunMap {α : Type u_1} {𝔽 : Type u_7} [Field 𝔽] : Module.Dual 𝔽 (α →₀ 𝔽) →ₗ[𝔽] α → 𝔽

For a member φ of the dual module of α →₀ R, the vector in α → R whose ith entry is the value of φ at Finsupp.single a i.

Equations

• Matroid.Finsupp.dualFunMap = { toFun := fun (φ : Module.Dual 𝔽 (α →₀ 𝔽)) (a : α) => φ (Finsupp.single a 1), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matroid.Finsupp.dualFunMap_apply {α : Type u_1} {𝔽 : Type u_7} [Field 𝔽] (φ : Module.Dual 𝔽 (α →₀ 𝔽)) (a : α) : dualFunMap φ a = φ (Finsupp.single a 1)

def Matroid.mySupported {α : Type u_1} (𝔽 : Type u_9) [Field 𝔽] (s : Set α) : Submodule 𝔽 (α → 𝔽)

Equations

• Matroid.mySupported 𝔽 s = { carrier := {f : α → 𝔽 | ∀ i ∉ s, f i = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def Matroid.Finsupp.dualSupportedFunMap {α : Type u_9} (R : Type u_10) [CommSemiring R] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : Module.Dual R ↥(Finsupp.supported R R s) →ₗ[R] α → R

For s : Set α, and a member φ of the dual module of Finsupp.supported R R s, the vector in α → R whose ith entry is the value of φ at Finsupp.single a i.

Equations

• One or more equations did not get rendered due to their size.

theorem Matroid.Finsupp.dualSupportedFunMap_apply_notMem {α : Type u_9} {R : Type u_10} [CommSemiring R] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (φ : Module.Dual R ↥(Finsupp.supported R R s)) {a : α} (ha : a ∉ s) : (dualSupportedFunMap R s) φ a = 0

theorem Matroid.Finsupp.dualSupportedFunMap_apply_mem {α : Type u_9} {R : Type u_10} [CommSemiring R] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (φ : Module.Dual R ↥(Finsupp.supported R R s)) {a : α} (ha : a ∈ s) : (dualSupportedFunMap R s) φ a = φ ⟨Finsupp.single a 1, ⋯⟩

theorem Matroid.Finsupp.dualSupportedFunMap_apply {α : Type u_9} (R : Type u_10) [CommSemiring R] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (φ : Module.Dual R ↥(Finsupp.supported R R s)) (a : α) : (dualSupportedFunMap R s) φ a = if has : a ∈ s then φ ⟨Finsupp.single a 1, ⋯⟩ else 0

@[simp]

theorem Matroid.mem_mySupported_iff {α : Type u_1} {𝔽 : Type u_7} [Field 𝔽] {s : Set α} {x : α → 𝔽} : x ∈ mySupported 𝔽 s ↔ Function.support x ⊆ s

@[simp]

theorem Matroid.coe_restrictDom {α : Type u_9} {M : Type u_10} {R : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) [DecidablePred fun (x : α) => x ∈ s] (f : ↥(Finsupp.supported M R s)) : ↑((Finsupp.restrictDom M R s) ↑f) = ↑f

noncomputable def Matroid.Rep.cocycleSpace {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : Submodule 𝔽 (α → 𝔽)

The cocycleSpace of an 𝔽-representation of M : Matroid α is the set of vectors in α → 𝔽 that are supported on M.E, and are orthogonal to every vector in the cycleSpace. If M is finite, this corresponds to the row space of a matrix representation of M.

Equations

• v.cocycleSpace = Submodule.map Matroid.Finsupp.dualFunMap v.cycleSpace.dualAnnihilator ⊓ Matroid.mySupported 𝔽 M.E

theorem Matroid.Rep.cocycleSpace_eq' {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) [DecidablePred fun (x : α) => x ∈ M.E] : v.cocycleSpace = Submodule.map (Finsupp.dualSupportedFunMap 𝔽 M.E) v.supportedCycleSpace.dualAnnihilator

@[simp]

theorem Matroid.Rep.cocycleSpace_comp {α : Type u_1} {W' : Type u_4} {M : Matroid α} [AddCommGroup W'] {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (φ : W →ₗ[𝔽] W') (hφ : Disjoint (Submodule.span 𝔽 (Set.range ⇑v)) φ.ker) : (v.comp φ hφ).cocycleSpace = v.cocycleSpace

@[simp]

theorem Matroid.Rep.cocycleSpace_comp' {α : Type u_1} {W' : Type u_4} {M : Matroid α} [AddCommGroup W'] {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (φ : W →ₗ[𝔽] W') (hφ : φ.ker = ⊥) : (v.comp' φ hφ).cocycleSpace = v.cocycleSpace

@[simp]

theorem Matroid.Rep.cocycleSpace_compEquiv {α : Type u_1} {W' : Type u_4} {M : Matroid α} [AddCommGroup W'] {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] [Module 𝔽 W'] (v : M.Rep 𝔽 W) (φ : W ≃ₗ[𝔽] W') : (v.compEquiv φ).cocycleSpace = v.cocycleSpace

@[simp]

theorem Matroid.Rep.restrictSpan_cocycleSpace {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : v.restrictSpan.cocycleSpace = v.cocycleSpace

@[simp]

theorem Matroid.Rep.standardRep'_cocycleSpace {α : Type u_1} {B : Set α} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hB : M.IsBase B) : (v.standardRep' hB).cocycleSpace = v.cocycleSpace

@[simp]

theorem Matroid.Rep.standardRep_cocycleSpace {α : Type u_1} {B : Set α} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hB : M.IsBase B) : (v.standardRep hB).cocycleSpace = v.cocycleSpace

theorem Matroid.Rep.mem_cocycleSpace_iff_of_support {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {x : α → 𝔽} (hx : Function.support x ⊆ M.E) : x ∈ v.cocycleSpace ↔ ∀ y ∈ v.cycleSpace, (Finsupp.linearCombination 𝔽 x) y = 0

theorem Matroid.Rep.mem_cocycleSpace_iff {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {x : α → 𝔽} : x ∈ v.cocycleSpace ↔ (∀ y ∈ v.cycleSpace, (Finsupp.linearCombination 𝔽 x) y = 0) ∧ Function.support x ⊆ M.E

theorem Matroid.Rep.row_mem_cocycleSpace {α : Type u_1} {β : Type u_2} {M : Matroid α} {𝔽 : Type u_7} [Field 𝔽] (v : M.Rep 𝔽 (β → 𝔽)) (b : β) : (fun (x : α) => v x b) ∈ v.cocycleSpace

theorem Matroid.Rep.mem_cycleSpace_iff_forall_of_support {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {y : α →₀ 𝔽} (hy : Function.support ⇑y ⊆ M.E) : y ∈ v.cycleSpace ↔ ∀ x ∈ v.cocycleSpace, (Finsupp.linearCombination 𝔽 x) y = 0

theorem Matroid.Rep.mem_cycleSpace_iff_forall {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {y : α →₀ 𝔽} : y ∈ v.cycleSpace ↔ (∀ x ∈ v.cocycleSpace, (Finsupp.linearCombination 𝔽 x) y = 0) ∧ Function.support ⇑y ⊆ M.E

instance Matroid.Rep.cocycleSpace_finiteDimensional {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.Finite] (v : M.Rep 𝔽 W) : FiniteDimensional 𝔽 ↥v.cocycleSpace