Finite-field coordinates for minimal representations

An injective affine chart has an affine left inverse on the whole ambient vector space. Its retraction identity extends from the support to its affine span. Integer affine generation also implies affine generation modulo p.

noncomputable def EGZ.affineLeftInverse {k : Type u_1} [Field k] {m n : ℕ} (A : (Fin m → k) →ᵃ[k] Fin n → k) : (Fin n → k) →ᵃ[k] Fin m → k

An affine retraction that is a left inverse when the original affine map is injective.

Equations

• EGZ.affineLeftInverse A = A.linear.leftInverse.toAffineMap.comp (AffineMap.id k (Fin n → k) - AffineMap.const k (Fin n → k) (A 0))

theorem EGZ.affineLeftInverse_apply {k : Type u_1} [Field k] {m n : ℕ} (A : (Fin m → k) →ᵃ[k] Fin n → k) (hA : Function.Injective ⇑A) (q : Fin m → k) : (affineLeftInverse A) (A q) = q

theorem EGZ.affineLeftInverse_retract {k : Type u_1} [Field k] {m n : ℕ} (A : (Fin m → k) →ᵃ[k] Fin n → k) (hA : Function.Injective ⇑A) {q : Fin n → k} (hq : q ∈ Set.range ⇑A) : A ((affineLeftInverse A) q) = q

theorem EGZ.affineLeftInverse_retract_affineSpan {k : Type u_1} [Field k] {l m n : ℕ} (A : (Fin m → k) →ᵃ[k] Fin n → k) (hA : Function.Injective ⇑A) (φ : (Fin l → k) →ᵃ[k] Fin n → k) (S : Set (Fin l → k)) (hS : ∀ v ∈ S, φ v ∈ Set.range ⇑A) {v : Fin l → k} (hv : v ∈ affineSpan k S) : A ((affineLeftInverse A) (φ v)) = φ v

Retraction through the chart is the identity on the entire affine span once it is the identity on the support.

theorem EGZ.surjOn_affineSpan_of_image_span_eq_top {k : Type u_1} [Field k] {m n : ℕ} (φ : (Fin m → k) →ᵃ[k] Fin n → k) (S : Set (Fin m → k)) (hS : affineSpan k (⇑φ '' S) = ⊤) : Set.SurjOn (⇑φ) (↑(affineSpan k S)) Set.univ

theorem EGZ.FlagDecomposition.AffineIntSpans.affineSpan_mod_eq_top {p n : ℕ} [Fact (Nat.Prime p)] {S : Finset (IntCoord n)} (hS : AffineIntSpans S) : affineSpan (ZMod p) (IntCoord.mod p '' ↑S) = ⊤

Integer affine generators generate the full finite-field affine space after reduction modulo a prime.