@[reducible, inline]

abbrev Matroid.Rep.projFun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.OnUniv] [M.Loopless] (v : M.Rep 𝔽 W) (e : α) : Projectivization 𝔽 W

Equations

• v.projFun e = Projectivization.mk 𝔽 (v e) ⋯

theorem Matroid.Rep.projFun_apply {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.OnUniv] [M.Loopless] (v : M.Rep 𝔽 W) (e : α) : v.projFun e = Projectivization.mk 𝔽 (v e) ⋯

theorem Matroid.Rep.projFun_eq {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.OnUniv] [M.Loopless] (v : M.Rep 𝔽 W) : v.projFun = fun (e : α) => Projectivization.mk 𝔽 (v e) ⋯

theorem Matroid.Rep.projFun_injective {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.OnUniv] [M.Loopless] [M.Simple] (v : M.Rep 𝔽 W) : Function.Injective v.projFun

theorem Matroid.Rep.indep_iff_projFun {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {I : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.OnUniv] [M.Loopless] (v : M.Rep 𝔽 W) : M.Indep I ↔ Projectivization.Independent fun (x : ↑I) => v.projFun ↑x

@[simp]

theorem Matroid.Rep.independent_image_projFun_iff {α : Type u_1} {W : Type u_3} {𝔽 : Type u_5} {I : Set α} {M : Matroid α} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [M.OnUniv] [M.Loopless] [M.Simple] (v : M.Rep 𝔽 W) : (Projectivization.Independent fun (x : ↑(v.projFun '' I)) => ↑x) ↔ M.Indep I

theorem Matroid.span_image_projFun_eq {α : Type u_1} {M : Matroid α} [M.OnUniv] [M.Loopless] {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (X : Set α) : Projectivization.Subspace.span (v.projFun '' X) = (Submodule.span 𝔽 (⇑v '' X)).toProjSubspace

theorem Matroid.Rep.closure_eq_span_image_projFun {α : Type u_1} {M : Matroid α} [M.OnUniv] [M.Loopless] {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (X : Set α) : M.closure X = v.projFun ⁻¹' ↑(Projectivization.Subspace.span (v.projFun '' X))

theorem Matroid.Rep.FullRank.spanning_iff_projFun {α : Type u_1} {M : Matroid α} [M.OnUniv] [M.Loopless] {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] (v : M.Rep 𝔽 W) (hv : v.FullRank) (S : Set α) : M.Spanning S ↔ Projectivization.Subspace.span (v.projFun '' S) = ⊤

theorem Matroid.Rep.isBase_iff_proj {α : Type u_1} {M : Matroid α} [M.OnUniv] [M.Loopless] {𝔽 : Type u_7} {W : Type u_8} [Field 𝔽] [AddCommGroup W] [Module 𝔽 W] {v : M.Rep 𝔽 W} (hv : v.FullRank) (B : Set α) : M.IsBase B ↔ (Projectivization.Independent fun (x : ↑B) => v.projFun ↑x) ∧ Projectivization.Subspace.span (v.projFun '' B) = ⊤

noncomputable def Projectivization.matroid (𝔽 : Type u_7) (W : Type u_8) [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : Matroid (Projectivization 𝔽 W)

The natural 𝔽-representable matroid whose ground set is a projective geometry over 𝔽.

Equations

• Projectivization.matroid 𝔽 W = (Module.matroid 𝔽 W).comap Projectivization.rep

@[simp]

theorem Projectivization.matroid_E (𝔽 : Type u_7) (W : Type u_8) [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : (Projectivization.matroid 𝔽 W).E = Projectivization.rep ⁻¹' (Module.matroid 𝔽 W).E

noncomputable def Projectivization.matroidRep {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : (Projectivization.matroid 𝔽 W).Rep 𝔽 W

Equations

• Projectivization.matroidRep = (Module.matroidRep 𝔽 W).comap Projectivization.rep

instance Projectivization.matroid_onUniv {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : (Projectivization.matroid 𝔽 W).OnUniv

@[simp]

theorem Projectivization.projectiveGeometry_eq_empty {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] [Subsingleton W] : Projectivization.matroid 𝔽 W = Matroid.emptyOn (Projectivization 𝔽 W)

@[simp]

theorem Projectivization.matroidRep_apply_eq {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] (e : Projectivization 𝔽 W) : matroidRep e = e.rep

theorem Projectivization.matroidRep_fullRank {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : matroidRep.FullRank

instance Projectivization.instLooplessMatroid {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : (Projectivization.matroid 𝔽 W).Loopless

@[simp]

theorem Projectivization.matroidRep_indep_iff {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] {I : Set (Projectivization 𝔽 W)} : (Projectivization.matroid 𝔽 W).Indep I ↔ Independent fun (x : ↑I) => ↑x

instance Projectivization.matroid_simple {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : (Projectivization.matroid 𝔽 W).Simple

instance Projectivization.matroid_finitary {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : (Projectivization.matroid 𝔽 W).Finitary

noncomputable def Projectivization.PG (n p t : ℕ) [Fact (Nat.Prime p)] : Matroid (Projectivization (GaloisField p t) (Fin (n + 1) → GaloisField p t))

The projective geometry of rank n+1 over GF(p^t).

Equations

• Projectivization.PG n p t = Projectivization.matroid (GaloisField p t) (Fin (n + 1) → GaloisField p t)

@[simp]

theorem Projectivization.matroid_cRank {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : (Projectivization.matroid 𝔽 W).cRank = Module.rank 𝔽 W

TODO: Generalize this to arbitrary fullrank representations

@[simp]

theorem Projectivization.projectiveGeometry_rank {W : Type u_3} {𝔽 : Type u_5} [DivisionRing 𝔽] [AddCommGroup W] [Module 𝔽 W] : (Projectivization.matroid 𝔽 W).rank = Module.finrank 𝔽 W

noncomputable def Projectivization.matroid_congr {𝔽 : Type u_7} {W : Type u_8} {W' : Type u_9} [Field 𝔽] [AddCommGroup W] [AddCommGroup W'] [Module 𝔽 W] [Module 𝔽 W'] (i : W ≃ₗ[𝔽] W') : Projectivization.matroid 𝔽 W ≂ Projectivization.matroid 𝔽 W'

Isomorphic vector spaces give isomorphic projective geometries.

Equations

• Projectivization.matroid_congr i = ((Projectivization.matroid 𝔽 W).isoMapEquiv (Projectivization.mapEquiv i)).trans (Matroid.Iso.ofEq ⋯)

@[simp]

theorem Projectivization.PG_rank (n p t : ℕ) [Fact (Nat.Prime p)] : (PG n p t).rank = n + 1

theorem Matroid.Representable.exists_isoRestr_projectiveGeometry {α : Type u_1} {B : Set α} {M : Matroid α} {𝔽 : Type u_7} [Field 𝔽] [M.Simple] (h : M.Representable 𝔽) (hB : M.IsBase B) : ∃ (i : IsoRestr M (Projectivization.matroid 𝔽 (↑B →₀ 𝔽))), i.Spanning

Every simple 𝔽-representable matroid is isomorphic to a spanning restriction of a projective geometry over 𝔽.

theorem Matroid.Representable.encard_le_of_simple {α : Type u_1} {M : Matroid α} {𝔽 : Type u_7} [Field 𝔽] [M.RankFinite] [M.Simple] (h : M.Representable 𝔽) : M.E.encard ≤ ∑ i ∈ Finset.range M.rank, ENat.card 𝔽 ^ i

A simple rank-r F-representable matroid has at most 1 + |𝔽| + |𝔽|^2 + ... + |𝔽|^(r-1) elements. Also true for infinite 𝔽.