DirectionSpaces.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KaplanskyCounterexample.FiniteGeometry.curve line 12
lemma OAI.KaplanskyCounterexample.FiniteGeometry.curve_relation line 14
lemma OAI.KaplanskyCounterexample.FiniteGeometry.curve_linearIndependent line 22
def OAI.KaplanskyCounterexample.FiniteGeometry.curveMap line 30
Source documentation
The one-dimensional extension-field line, viewed over the ground field.
```
def curveMap {Q : Type u_4} {F : Type u_5} [Field Q] [Field F] [Algebra Q F]
    (m : ℕ) (ξ : F) : F →ₗ[Q] (Fin m → F) where
…
```
lemma OAI.KaplanskyCounterexample.FiniteGeometry.curveMap_injective line 38
lemma OAI.KaplanskyCounterexample.FiniteGeometry.curveMap_direct line 46
Source documentation
Any at most m of the extension-field lines have direct sum over Q. Each chosen Q-subspace can subsequently be taken inside its own line.
```
lemma curveMap_direct {Q : Type u_8} {F : Type u_9} [Field Q] [Field F] [Algebra Q F]
    {k m : ℕ} (hk : k ≤ m) {ξ : Fin k → F} (hξ : Function.Injective ξ)
    (x : Fin k → (Fin m → F))
    (hx : ∀ i, x i ∈ (curveMap (Q := Q) m (ξ i)).range)
…
```
Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.curveMap

lemma OAI.KaplanskyCounterexample.FiniteGeometry.exists_subspace_in_curve line 59

Source documentation

Select any required ground-field dimension inside a curve line.

lemma exists_subspace_in_curve {Q : Type u_10} {F : Type u_11} [Field Q] [Field F] [Algebra Q F]
    [FiniteDimensional Q F] {m : ℕ} (hm : 0 < m) (ξ : F)
    (d : ℕ) (hd : d ≤ finrank Q F) :
    ∃ P : Submodule Q (Fin m → F), finrank Q P = d ∧
      P ≤ (curveMap (Q := Q) m ξ).range := by
…

Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.curveMap

def OAI.KaplanskyCounterexample.FiniteGeometry.ShortDirect line 75

Source documentation

Direct sum for distinct selections of at most m members of a family.

def ShortDirect {Q : Type u_12} {A : Type u_13} {ι : Type u_14} [Field Q] [AddCommGroup A] [Module Q A]
    (m : ℕ) (P : ι → Submodule Q A) : Prop :=
…

theorem OAI.KaplanskyCounterexample.FiniteGeometry.exists_shortDirect_subspaces line 81

Source documentation

The Vandermonde construction of all the required direction spaces.

theorem exists_shortDirect_subspaces {Q : Type u_15} {F : Type u_16} {ι : Type u_17} [Field Q] [Field F] [Algebra Q F]
    [FiniteDimensional Q F] [Fintype F] [Fintype ι]
    {m : ℕ} (hm : 0 < m) (d : ι → ℕ) (hd : ∀ i, d i ≤ finrank Q F)
    (hcard : Fintype.card ι ≤ Fintype.card F) :
    ∃ P : ι → Submodule Q (Fin m → F),
      (∀ i, finrank Q (P i) = d i) ∧ ShortDirect m P := by
…

Mentions: OAI.KaplanskyCounterexample.FiniteGeometry.ShortDirect