theorem Function.ExtendByZero.linearMap_injective (R : Type u_7) {ι : Type u_8} {η : Type u_9} [Semiring R] {s : ι → η} (hs : Injective s) : Injective ⇑(linearMap R R s)

theorem Matroid.Rep.span_spanning_eq {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {S : Set α} (hS : M.Spanning S) : Submodule.span 𝔽 (⇑v '' S) = Submodule.span 𝔽 (Set.range ⇑v)

theorem Matroid.Rep.spanning_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) {S : Set α} (hSE : S ⊆ M.E := by aesop_mat) : M.Spanning S ↔ Submodule.span 𝔽 (⇑v '' S) = Submodule.span 𝔽 (Set.range ⇑v)

def Matroid.Rep.FullRank {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : Prop

A representation is FullRank if its vectors span the space

Equations

• v.FullRank = (⊤ ≤ Submodule.span 𝔽 (Set.range ⇑v))

def Matroid.Rep.restrictSpan {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : M.Rep 𝔽 ↥(Submodule.span 𝔽 (Set.range ⇑v))

Restrict a representation to the submodule spanned by its image

Equations

• v.restrictSpan = { to_fun := Set.codRestrict ⇑v ↑(Submodule.span 𝔽 (Set.range ⇑v)) ⋯, indep_iff' := ⋯ }

@[simp]

theorem Matroid.Rep.restrictSpan_to_fun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (a✝ : α) : v.restrictSpan.to_fun a✝ = Set.codRestrict ⇑v ↑(Submodule.span 𝔽 (Set.range ⇑v)) ⋯ a✝

@[simp]

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

theorem Matroid.Rep.restrictSpan_comp {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : v.restrictSpan.comp' (Submodule.span 𝔽 (Set.range ⇑v)).subtype ⋯ = v

theorem Matroid.Rep.FullRank.span_range {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : M.Rep 𝔽 W} (h : v.FullRank) : Submodule.span 𝔽 (Set.range ⇑v) = ⊤

theorem Matroid.Rep.FullRank.span_spanning {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : M.Rep 𝔽 W} (h : v.FullRank) {S : Set α} (hS : M.Spanning S) : Submodule.span 𝔽 (⇑v '' S) = ⊤

theorem Matroid.Rep.FullRank.spanning_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (h : v.FullRank) {S : Set α} (hSE : S ⊆ M.E := by aesop_mat) : M.Spanning S ↔ Submodule.span 𝔽 (⇑v '' S) = ⊤

theorem Matroid.Rep.fullRank_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : M.Rep 𝔽 W} : v.FullRank ↔ Submodule.span 𝔽 (Set.range ⇑v) = ⊤

theorem Matroid.Rep.restrictSpan_eq_inclusion {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : ⇑v.restrictSpan = Set.inclusion ⋯ ∘ Set.rangeFactorization ⇑v

@[simp]

theorem Matroid.Rep.restrict_span_apply {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (e : α) : v.restrictSpan e = Set.inclusion ⋯ (Set.rangeFactorization (⇑v) e)

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

noncomputable def Matroid.Rep.FullRank.basis_of_isBase {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {B : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : M.Rep 𝔽 W} (h : v.FullRank) (hB : M.IsBase B) : Module.Basis (↑B) 𝔽 W

A base of M gives a linear basis in a full-rank representation

Equations

• h.basis_of_isBase hB = Basis.mkImage ⋯ ⋯

theorem Matroid.Rep.FullRank.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} (h : v.FullRank) (ψ : W ≃ₗ[𝔽] W') : (v.compEquiv ψ).FullRank

noncomputable def Matroid.Rep.isBasis_of_isBase {α : 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) : Module.Basis (↑B) 𝔽 ↥(Submodule.span 𝔽 (Set.range ⇑v))

A base of M gives a (linear) basis for the span of the range of a representation

Equations

• v.isBasis_of_isBase hB = (Basis.spanImage ⋯).map (LinearEquiv.ofEq (Submodule.span 𝔽 (⇑v '' B)) (Submodule.span 𝔽 (Set.range ⇑v)) ⋯)

noncomputable def Matroid.Rep.standardRep' {α : 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) : M.Rep 𝔽 (↑B →₀ 𝔽)

The natural representation with rows indexed by a base with Finsupp

Equations

• v.standardRep' hB = v.restrictSpan.compEquiv (⋯.basis_of_isBase hB).repr

@[simp]

theorem Matroid.Rep.standardRep_eq_one' {α : 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) (e : ↑B) : ((v.standardRep' hB) ↑e) e = 1

theorem Matroid.Rep.standardRep_eq_zero' {α : 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) (e f : ↑B) (hef : e ≠ f) : ((v.standardRep' hB) ↑e) f = 0

theorem Matroid.Rep.standardRep_fullRank' {α : 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).FullRank

noncomputable def Matroid.Rep.standardRep {α : 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) : M.Rep 𝔽 (↑B → 𝔽)

The natural representation of a matroid with rows indexed by a base

Equations

• v.standardRep hB = (v.standardRep' hB).comp Finsupp.lcoeFun ⋯

theorem Matroid.Rep.standardRep_eq_one {α : 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) (e : ↑B) : (v.standardRep hB) (↑e) e = 1

theorem Matroid.Rep.standardRep_eq_zero {α : 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) (e f : ↑B) (hef : e ≠ f) : (v.standardRep hB) (↑e) f = 0

theorem Matroid.Rep.standardRep_eq_mapEquiv {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {B : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.RankFinite] (v : M.Rep 𝔽 W) (hB : M.IsBase B) : v.standardRep hB = (v.standardRep' hB).compEquiv (Finsupp.linearEquivFunOnFinite 𝔽 𝔽 ↑B)

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

theorem Matroid.exists_eq_comp_standardRep' {α : 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) : ∃ (φ : (↑B →₀ 𝔽) →ₗ[𝔽] W) (hφ : φ.ker = ⊥), v = (v.standardRep' hB).comp' φ hφ

def Matroid.loopyRep {α : Type u_1} (E : Set α) (𝔽 : Type u_7) [DivisionRing 𝔽] : (loopyOn E).Rep 𝔽 𝔽

Equations

• Matroid.loopyRep E 𝔽 = { to_fun := 0, indep_iff' := ⋯ }

def Matroid.emptyRep (α : Type u_7) (𝔽 : Type u_8) [DivisionRing 𝔽] : (emptyOn α).Rep 𝔽 𝔽

Equations

• Matroid.emptyRep α 𝔽 = { to_fun := 0, indep_iff' := ⋯ }

noncomputable def Matroid.freeRep {α : Type u_1} (E : Set α) [DecidablePred fun (x : α) => x ∈ E] (𝔽 : Type u_7) [DivisionRing 𝔽] : (freeOn E).Rep 𝔽 (↑E →₀ 𝔽)

Equations

• Matroid.freeRep E 𝔽 = { to_fun := fun (x : α) => if hx : x ∈ E then Finsupp.single ⟨x, hx⟩ 1 else 0, indep_iff' := ⋯ }

noncomputable def Matroid.ofBaseCobaseFun {α : Type u_1} {𝔽 : Type u_5} [DivisionRing 𝔽] (B E : Set α) [DecidablePred fun (x : α) => x ∈ B] [DecidablePred fun (x : α) => x ∈ E] (v : ↑(E \ B) → ↑B →₀ 𝔽) : Matroid α

Equations

• Matroid.ofBaseCobaseFun B E v = Matroid.ofFun 𝔽 E fun (e : α) => if heB : e ∈ B then Finsupp.single ⟨e, heB⟩ 1 else if heE : e ∈ E then v ⟨e, ⋯⟩ else 0

structure Matroid.Rep.FunStandard {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] (v : M.Rep 𝔽 (β → 𝔽)) (i : β → α) : Prop

Given an injection i from the rows to the columns of a matrix representation v of M, Rep.FunStandard v i means that the range of i indexes an identity submatrix.

• apply_eq (b : β) : v (i b) b = 1
• apply_ne ⦃b b' : β⦄ : b ≠ b' → v (i b) b' = 0

theorem Matroid.Rep.FunStandard.injective {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {i : β → α} {v : M.Rep 𝔽 (β → 𝔽)} (hv : v.FunStandard i) : Function.Injective i

theorem Matroid.Rep.FunStandard.subset_ground {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {i : β → α} {v : M.Rep 𝔽 (β → 𝔽)} (hv : v.FunStandard i) : Set.range i ⊆ M.E

theorem Matroid.Rep.FunStandard.apply_eq_single {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {i : β → α} {v : M.Rep 𝔽 (β → 𝔽)} [DecidableEq β] (hv : v.FunStandard i) (b : β) : v (i b) = Pi.single b 1

theorem Matroid.Rep.FunStandard.IsBase {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {i : β → α} {v : M.Rep 𝔽 (β → 𝔽)} [M.RankFinite] (hv : v.FunStandard i) : M.IsBase (Set.range i)

structure Matroid.Rep.IsStandard {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {γ : Type u_7} {B : Set α} [FunLike γ (↑B) 𝔽] [AddCommGroup γ] [Module 𝔽 γ] (v : M.Rep 𝔽 γ) : Prop

A representation over B → 𝔽 or B →₀ 𝔽 IsStandard if it is the identity on B. The definition is agnostic as to whether the representation is Finsupp or Function, and is phrased without Function.Pi to avoid decidability assumptions.

In the Finsupp case, this implies that B is a base - see Matroid.Rep.IsStandard.isBase.

In the Function case, we really need a FiniteRank assumption for this to be sensible, since, if I is an infinite identity matrix and 1 means the all-ones vector, then [I | 1] represents a free matroid in which I doesn't correspond to a base.

• apply_eq (x : ↑B) : (v ↑x) x = 1
• apply_ne ⦃x y : ↑B⦄ : x ≠ y → (v ↑x) y = 0

theorem Matroid.Rep.isStandard_iff {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {γ : Type u_7} {B : Set α} [FunLike γ (↑B) 𝔽] [AddCommGroup γ] [Module 𝔽 γ] (v : M.Rep 𝔽 γ) : v.IsStandard ↔ (∀ (x : ↑B), (v ↑x) x = 1) ∧ ∀ ⦃x y : ↑B⦄, x ≠ y → (v ↑x) y = 0

structure Matroid.Rep.IsStandard' {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} (v : M.Rep 𝔽 (↑B → 𝔽)) : Prop

• apply_eq (x : ↑B) : v (↑x) x = 1
• apply_ne ⦃x y : ↑B⦄ : x ≠ y → v (↑x) y = 0

theorem Matroid.Rep.isStandard'_iff {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} (v : M.Rep 𝔽 (↑B → 𝔽)) : v.IsStandard' ↔ (∀ (x : ↑B), v (↑x) x = 1) ∧ ∀ ⦃x y : ↑B⦄, x ≠ y → v (↑x) y = 0

theorem Matroid.Rep.IsStandard.apply_mem_eq {α : Type u_1} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] {γ : Type u_7} {B : Set α} [FunLike γ (↑B) 𝔽] [AddCommGroup γ] [Module 𝔽 γ] {v : M.Rep 𝔽 γ} (hv : v.IsStandard) (he : e ∈ B) : (v e) ⟨e, he⟩ = 1

theorem Matroid.Rep.IsStandard.apply_mem_ne {α : Type u_1} {𝔽 : Type u_5} {e f : α} {M : Matroid α} [DivisionRing 𝔽] {γ : Type u_7} {B : Set α} [FunLike γ (↑B) 𝔽] [AddCommGroup γ] [Module 𝔽 γ] {v : M.Rep 𝔽 γ} (hv : v.IsStandard) (he : e ∈ B) (hf : f ∈ B) (hef : e ≠ f) : (v e) ⟨f, hf⟩ = 0

theorem Matroid.Rep.IsStandard'.apply_eq_single {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} [DecidableEq ↑B] {v : M.Rep 𝔽 (↑B → 𝔽)} (hv : v.IsStandard') (x : ↑B) : v ↑x = Pi.single x 1

theorem Matroid.Rep.IsStandard.injOn {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {γ : Type u_7} {B : Set α} [FunLike γ (↑B) 𝔽] [AddCommGroup γ] [Module 𝔽 γ] {v : M.Rep 𝔽 γ} (hv : v.IsStandard) : Set.InjOn (⇑v) B

theorem Matroid.Rep.IsStandard.image_coe_support_subset {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {γ : Type u_7} {B : Set α} [FunLike γ (↑B) 𝔽] [AddCommGroup γ] [Module 𝔽 γ] {v : M.Rep 𝔽 γ} : v.IsStandard → ∀ {e : α}, Subtype.val '' Function.support ⇑(v e) ⊆ B

theorem Matroid.Rep.IsStandard.apply_finsupp {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) (e : ↑B) : v ↑e = Finsupp.single e 1

theorem Matroid.isStandard_finsupp_iff {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} : v.IsStandard ↔ ∀ (e : ↑B), v ↑e = Finsupp.single e 1

theorem Matroid.Rep.IsStandard.apply_finsupp_mem {α : Type u_1} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) (he : e ∈ B) : v e = Finsupp.single ⟨e, he⟩ 1

theorem Matroid.Rep.IsStandard.isBase {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) : M.IsBase B

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

theorem Matroid.Rep.IsStandard.image_eq {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) (I : Set ↑B) : ⇑v '' Subtype.val '' I = ⇑Finsupp.basisSingleOne '' I

theorem Matroid.Rep.IsStandard.image_subset_eq {α : Type u_1} {𝔽 : Type u_5} {I : Set α} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) (hIB : I ⊆ B) : ⇑v '' I = ⇑Finsupp.basisSingleOne '' Subtype.val ⁻¹' I

theorem Matroid.Rep.IsStandard.mem_closure_iff {α : Type u_1} {𝔽 : Type u_5} {e : α} {I : Set α} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) (hIB : I ⊆ B) (heE : e ∈ M.E) : e ∈ M.closure I ↔ ↑(v e).support ⊆ Subtype.val ⁻¹' I

theorem Matroid.Rep.IsStandard.isCircuit_insert_support {α : Type u_1} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) (heB : e ∉ B) (heE : e ∈ M.E) : M.IsCircuit (insert e (Subtype.val '' ↑(v e).support))

For every column e of M.E \ B, the support of v e as a subset of B, together with e itself, make a circuit of M.

theorem Matroid.Rep.IsStandard.image_val_support_eq {α : Type u_1} {𝔽 : Type u_5} {e : α} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) (he : e ∉ B) : Subtype.val '' ↑(v e).support = M.fundCircuit e B ∩ B

theorem Matroid.Rep.IsStandard.isCocircuit_insert_support {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {B : Set α} {v : M.Rep 𝔽 (↑B →₀ 𝔽)} (hv : v.IsStandard) (e : ↑B) : M.IsCocircuit (Function.support fun (x : α) => (v x) e)

For every e ∈ B, the support of the row of v corresponding to e is a cocircuit of M.

def Matroid.Representable {α : Type u_1} (M : Matroid α) (𝔽 : Type u_7) [Semiring 𝔽] : Prop

A Representable matroid is one that has a representation over 𝔽. To avoid quantifying over types, we require that the representation is over the module α → 𝔽. Rep.Representable, which is defined later, makes this definition useful.

Equations

• M.Representable 𝔽 = Nonempty (M.Rep 𝔽 (α → 𝔽))

theorem Matroid.Rep.representable {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) : M.Representable 𝔽

Any representation makes a matroid representable.

@[simp]

theorem Matroid.loopyOn_representable {α : Type u_1} (E : Set α) (𝔽 : Type u_7) [DivisionRing 𝔽] : (loopyOn E).Representable 𝔽

@[simp]

theorem Matroid.emptyOn_representable (α : Type u_7) (𝔽 : Type u_8) [DivisionRing 𝔽] : (emptyOn α).Representable 𝔽

theorem Matroid.Representable.map {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] (hM : M.Representable 𝔽) {f : α → β} (hf : Set.InjOn f M.E) : (M.map f hf).Representable 𝔽

theorem Matroid.Representable.iso {α : Type u_1} {β : Type u_2} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {N : Matroid β} (hM : M.Representable 𝔽) (i : M ≂ N) : N.Representable 𝔽

theorem Matroid.Representable.exists_fullRank_rep {α : Type u_1} {𝔽 : Type u_5} {B : Set α} {M : Matroid α} [DivisionRing 𝔽] (hM : M.Representable 𝔽) (hB : M.IsBase B) : ∃ (v : M.Rep 𝔽 (↑B →₀ 𝔽)), v.FullRank

theorem Matroid.Representable.exists_isStandard_rep {α : Type u_1} {𝔽 : Type u_5} {B : Set α} {M : Matroid α} [DivisionRing 𝔽] (hM : M.Representable 𝔽) (hB : M.IsBase B) : ∃ (v : M.Rep 𝔽 (↑B →₀ 𝔽)), v.IsStandard

theorem Matroid.Representable.exists_fin_rep {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [M.RankFinite] (hM : M.Representable 𝔽) : ∃ (v : M.Rep 𝔽 (Fin M.rank → 𝔽)), v.FullRank

theorem Matroid.Representable.exists_fin_rep_of_eq {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] {n : ℕ} [M.RankFinite] (hM : M.Representable 𝔽) (hr : M.rank = n) : ∃ (v : M.Rep 𝔽 (Fin n → 𝔽)), v.FullRank