Coordinates adapted to an affine projection

The coordinate change used in the final expansion argument is proved here. An affine surjection from an affine subspace becomes first-coordinate projection after choosing coordinates on its kernel.

structure EGZ.Expansion.AffineModel {p d r : ℕ} (V : AffineSubspace (ZMod p) (FpCoord p d)) (φ : FpCoord p d →ᵃ[ZMod p] FpCoord p r) (c : FpCoord p r) (t : ℕ) : Type

Coordinates on an affine subspace in which φ is first-coordinate projection followed by translation by c.

• chart : FpCoord p (r + t) →ᵃ[ZMod p] FpCoord p d

  The injective affine chart from model coordinates onto the ambient affine set.

• injective : Function.Injective ⇑self.chart
• range_chart : Set.range ⇑self.chart = ↑V
• projection (q : FpCoord p (r + t)) : φ (self.chart q) = (Coord.first r t) q + c

theorem EGZ.Expansion.exists_affineModel {p d r : ℕ} [Fact (Nat.Prime p)] (V : AffineSubspace (ZMod p) (FpCoord p d)) (φ : FpCoord p d →ᵃ[ZMod p] FpCoord p r) (hφ : Set.SurjOn (⇑φ) (↑V) Set.univ) (c : FpCoord p r) : ∃ (t : ℕ), r + t ≤ d ∧ Nonempty (AffineModel V φ c t)

def EGZ.Expansion.IsThickRelativeOn {p d r : ℕ} [NeZero p] (w : FpCoord p d → ℕ) (V : Set (FpCoord p d)) (φ : FpCoord p d → FpCoord p r) (T : ℕ) (δ : ℝ) : Prop

Relative thickness restricted to the affine space carrying the weight.

Equations

• One or more equations did not get rendered due to their size.

theorem EGZ.Expansion.AffineModel.chart_mem {p d r t : ℕ} [Fact (Nat.Prime p)] {V : AffineSubspace (ZMod p) (FpCoord p d)} {φ : FpCoord p d →ᵃ[ZMod p] FpCoord p r} {c : FpCoord p r} (M : AffineModel V φ c t) (q : FpCoord p (r + t)) : M.chart q ∈ V

theorem EGZ.Expansion.AffineModel.pushWeight_weight {p d r t : ℕ} [NeZero p] [Fact (Nat.Prime p)] {V : AffineSubspace (ZMod p) (FpCoord p d)} {φ : FpCoord p d →ᵃ[ZMod p] FpCoord p r} {c : FpCoord p r} (M : AffineModel V φ c t) (w : FpCoord p d → ℕ) (hw : ∀ (v : FpCoord p d), w v ≠ 0 → v ∈ V) : pushWeight (⇑M.chart) (w ∘ ⇑M.chart) = w

theorem EGZ.Expansion.AffineModel.fibreWeight {p d r t : ℕ} [NeZero p] [Fact (Nat.Prime p)] {V : AffineSubspace (ZMod p) (FpCoord p d)} {φ : FpCoord p d →ᵃ[ZMod p] FpCoord p r} {c : FpCoord p r} (M : AffineModel V φ c t) (w : FpCoord p d → ℕ) (hw : ∀ (v : FpCoord p d), w v ≠ 0 → v ∈ V) (q : FpCoord p r) : pushWeight (⇑(Coord.first r t)) (w ∘ ⇑M.chart) (q - c) = pushWeight (⇑φ) w q

theorem EGZ.Expansion.AffineModel.thickRelative {p d r t : ℕ} [NeZero p] [Fact (Nat.Prime p)] {V : AffineSubspace (ZMod p) (FpCoord p d)} {φ : FpCoord p d →ᵃ[ZMod p] FpCoord p r} {c : FpCoord p r} (M : AffineModel V φ c t) (w : FpCoord p d → ℕ) (hw : ∀ (v : FpCoord p d), w v ≠ 0 → v ∈ V) {T : ℕ} {δ : ℝ} (h : IsThickRelativeOn w (↑V) (⇑φ) T δ) : IsThickRelative (w ∘ ⇑M.chart) (⇑(Coord.first r t)) T δ

theorem EGZ.Expansion.AffineModel.hasZeroSumMultiplicity_of_coordinates {p d r t : ℕ} [NeZero p] [Fact (Nat.Prime p)] {V : AffineSubspace (ZMod p) (FpCoord p d)} {φ : FpCoord p d →ᵃ[ZMod p] FpCoord p r} {c : FpCoord p r} (M : AffineModel V φ c t) (w : FpCoord p d → ℕ) (hw : ∀ (v : FpCoord p d), w v ≠ 0 → v ∈ V) (h : HasZeroSumMultiplicity (w ∘ ⇑M.chart)) : HasZeroSumMultiplicity w