Algebraic matroids

StructureAlgebraic representation of a matroid#✓fully proved

Let \(K\) be a field and \(M\) a matroid on a type \(E\). An algebraic representation of \(M\) over \(K\) consists of a field extension \(L\) of \(K\) and a map \(\varphi \colon E \to L\) such that \(L\) is generated over \(K\) by the image under \(\varphi\) of the ground set of \(M\), and a set \(I\) is independent in \(M\) exactly when \(I\) is contained in the ground set of \(M\), \(\varphi\) is injective on \(I\), and \(\varphi(I)\) is algebraically independent over \(K\).

Matroid.AlgebraicRepresentation · 16 lines

structure AlgebraicRepresentation (K : Type u) [Field K] {E : Type v}
    (M : Matroid E) where
  /-- Ambient extension field holding the realization. -/
  L : Type w
  /-- Field structure on the ambient extension. -/
  [field : Field L]
  /-- `K`-algebra structure on the ambient extension. -/
  [algebra : Algebra K L]
  /-- Faithfulness of the scalar action of `K` on `L`. -/
  [faithful : FaithfulSMul K L]
  /-- Map sending each ground-set element to `L`. -/
  realize : E → L
  /-- The realized ground set generates `L` over `K`. -/
  generates : IntermediateField.adjoin K (realize '' M.E) = ⊤
  /-- Independence in `M` matches algebraic independence in `L`. -/
  matroid_eq : M = (AlgebraicIndependent.matroid K L).comapOn M.E realize

Used by 2

Used byAlgebraic matroid over a field · Algebraic representations witness algebraicity over a field

DefinitionAlgebraic matroid over a field#✓fully proved

Let \(K\) be a field. A matroid \(M\) on a type \(E\) is algebraic over \(K\) if it has an algebraic representation over \(K\) whose extension field lies in the larger of the universes of \(K\) and \(E\).

Universe encoding: Lean fixes universes, so the witness extension is required to live in a universe holding both \(K\) and \(E\).

def IsAlgebraicOver (K : Type u) [Field K] {E : Type v}
    (M : Matroid E) : Prop :=
  Nonempty (AlgebraicRepresentation.{u, v, max u v} K M)

Uses 1 · Used by 1

Statement usesAlgebraic representation of a matroid

Used byAlgebraic representations witness algebraicity over a field

StructureAlgebraic representation of a matroid over some field#✓fully proved

Let \(M\) be a matroid on a type \(E\). An algebraic representation of \(M\) over some field consists of a field \(K\), a field extension \(L\) of \(K\) and a map \(\varphi \colon E \to L\) such that \(L\) is generated over \(K\) by the image under \(\varphi\) of the ground set of \(M\), and a set \(I\) is independent in \(M\) exactly when \(I\) is contained in the ground set of \(M\), \(\varphi\) is injective on \(I\), and \(\varphi(I)\) is algebraically independent over \(K\).

Universe encoding: both \(K\) and \(L\) lie in the same universe as \(E\), so matroids on \(E\) need no larger universes.

Matroid.AlgebraicRepresentationSomeField · 20 lines

structure AlgebraicRepresentationSomeField {E : Type v}
    (M : Matroid E) where
  /-- Base field of the realization, in the same universe as `E`. -/
  K : Type v
  /-- Field structure on the base field. -/
  [fieldK : Field K]
  /-- Extension field holding the realization. -/
  L : Type v
  /-- Field structure on the extension. -/
  [fieldL : Field L]
  /-- `K`-algebra structure on the extension. -/
  [algebra : Algebra K L]
  /-- Faithfulness of the scalar action of `K` on `L`. -/
  [faithful : FaithfulSMul K L]
  /-- Map sending each ground-set element to `L`. -/
  realize : E → L
  /-- The realized ground set generates `L` over `K`. -/
  generates : IntermediateField.adjoin K (realize '' M.E) = ⊤
  /-- Independence in `M` matches algebraic independence in `L`. -/
  matroid_eq : M = (AlgebraicIndependent.matroid K L).comapOn M.E realize

Used by 2

Used byAlgebraic matroid · Representations over some field witness algebraicity

DefinitionAlgebraic matroid#✓fully proved

A matroid \(M\) on a type \(E\) is algebraic if it has an algebraic representation over some field whose base field and extension field lie in the same universe as \(E\).

Universe encoding: this is the universe-local form of algebraicity for matroids on \(E\).

def IsAlgebraic {E : Type v} (M : Matroid E) : Prop :=
  Nonempty (AlgebraicRepresentationSomeField M)

Uses 1 · Used by 1

Statement usesAlgebraic representation of a matroid over some field

Used byRepresentations over some field witness algebraicity

TheoremAlgebraic representations witness algebraicity over a field#✓fully proved

Let \(K\) be a field and \(M\) a matroid on a type \(E\). If \(M\) has an algebraic representation over \(K\) whose extension field lies in the larger of the universes of \(K\) and \(E\), then \(M\) is algebraic over \(K\).

theorem AlgebraicRepresentation.toIsAlgebraicOver {K : Type u} [Field K]
    {E : Type v} {M : Matroid E}
    (self : AlgebraicRepresentation.{u, v, max u v} K M) :
    IsAlgebraicOver K M

Uses 2

Statement usesAlgebraic representation of a matroid · Algebraic matroid over a field

TheoremRepresentations over some field witness algebraicity#✓fully proved

If a matroid \(M\) on a type \(E\) has an algebraic representation over some field whose base field and extension field lie in the same universe as \(E\), then \(M\) is algebraic.

theorem AlgebraicRepresentationSomeField.toIsAlgebraic {E : Type v}
    {M : Matroid E} (self : AlgebraicRepresentationSomeField M) :
    IsAlgebraic M

Uses 2

Statement usesAlgebraic representation of a matroid over some field · Algebraic matroid

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.