Thickness on fibres of augmented representations

Two points in the same augmented fibre agree on the old representation and on every added direction. They therefore agree on the whole enlarged space of fibre-constant affine functionals. A functional distinguishing them lies outside that space, where maximality supplies thickness after slab pruning.

def EGZ.affineFunctionalEqualizer {p d : ℕ} [Fact (Nat.Prime p)] (v w : FpCoord p d) : Submodule (ZMod p) (FpCoord p d →ᵃ[ZMod p] ZMod p)

Affine functionals taking the same value at two specified points.

Equations

• EGZ.affineFunctionalEqualizer v w = { carrier := {ξ : EGZ.FpCoord p d →ᵃ[ZMod p] ZMod p | ξ v = ξ w}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem EGZ.DirectionChain.eq_on_augmented_fibre {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) {k : ℕ} {P : ℕ → (FpCoord p d →ᵃ[ZMod p] ZMod p) → Prop} (D : DirectionChain (R.fiberConstantSubmodule x) P k) {v w : FpCoord p d} (hv : v ∈ R.space x) (hw : w ∈ R.space x) (hmap : (R.map x) v = (R.map x) w) (hdir : ∀ i < k, (D.direction i) v = (D.direction i) w) {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} (hξ : ξ ∈ D.space k) : ξ v = ξ w

Equality on the old fibre and every added direction implies equality on the final span.

theorem EGZ.DirectionChain.not_mem_of_augmented_fibre_witness {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) {k : ℕ} {P : ℕ → (FpCoord p d →ᵃ[ZMod p] ZMod p) → Prop} (D : DirectionChain (R.fiberConstantSubmodule x) P k) {v w : FpCoord p d} (hv : v ∈ R.space x) (hw : w ∈ R.space x) (hmap : (R.map x) v = (R.map x) w) (hdir : ∀ i < k, (D.direction i) v = (D.direction i) w) {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} (hξ : ξ v ≠ ξ w) : ξ ∉ D.space k

theorem EGZ.DirectionChain.thick_slabIntersection_of_augmented_fibre {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) {k : ℕ} {weight : FpCoord p d → ℕ} {t : ℕ → ℕ} {δ : ℝ} (D : DirectionChain (R.fiberConstantSubmodule x) (fun (i : ℕ) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) => IsThinAlong weight ξ (t (i + 1)) (3 ^ (i + 1) * δ)) k) (hδ : 0 ≤ δ) (hmax : ∀ ξ ∉ D.space k, IsThickAlong weight ξ (t (k + 1)) (3 ^ (k + 1) * δ)) {v w : FpCoord p d} (hv : v ∈ R.space x) (hw : w ∈ R.space x) (hmap : (R.map x) v = (R.map x) w) (hdir : ∀ i < k, (D.direction i) v = (D.direction i) w) {ξ : FpCoord p d →ᵃ[ZMod p] ZMod p} (hξ : ξ v ≠ ξ w) : IsThickAlong (restrictWeight weight (slabIntersection k D.direction t)) ξ (t (k + 1)) δ

The selected weight is thick in every functional that distinguishes a pair in an augmented fibre. This is the completeness input for the new node.