Levels after complete-element refinement

Forgetting augmented coordinates factors the old represented map, so levels never decrease. If at least one direction was added, its independence from the old fibre-constant functionals forces every lower level above the old anchor. In particular this applies to the reduced complete representative.

theorem EGZ.FlagDecomposition.CompletePreparation.refined_space_le_original {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (hmod : ∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.split hp hδ hsmall).flag.Node) : (D.refined hp hδ hsmall C hmod hcenter).representation.space x ≤ Φ.representation.space ↑(↑↑x).1

theorem EGZ.FlagDecomposition.CompletePreparation.refined_forget_map {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (hmod : ∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.split hp hδ hsmall).flag.Node) (v : FpCoord p d) (hv : v ∈ (D.refined hp hδ hsmall C hmod hcenter).representation.space x) : ((Augmented.forget (D.split hp hδ hsmall) (D.extra hp hδ hsmall) D.chain.direction hp ⋯ C x).modp p) (((D.refined hp hδ hsmall C hmod hcenter).representation.map x) v) = (Φ.representation.map ↑(↑↑x).1) v

theorem EGZ.FlagDecomposition.CompletePreparation.refined_level_le {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (hmod : ∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.split hp hδ hsmall).flag.Node) : Φ.level ↑(↑↑x).1 ≤ (D.refined hp hδ hsmall C hmod hcenter).level x

Every output node has level at least that of its original base.

noncomputable def EGZ.FlagDecomposition.CompletePreparation.addedCoordinate {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (x : (D.split hp hδ hsmall).flag.Node) (i : Fin (D.extra hp hδ hsmall x)) : FpCoord p (C x).rank →ᵃ[ZMod p] ZMod p

Read one added functional from the new chart coordinates.

Equations

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

theorem EGZ.FlagDecomposition.CompletePreparation.addedCoordinate_map {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (hmod : ∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : (D.split hp hδ hsmall).flag.Node) (i : Fin (D.extra hp hδ hsmall x)) (v : FpCoord p d) (hv : v ∈ (D.refined hp hδ hsmall C hmod hcenter).representation.space x) : (D.addedCoordinate hp hδ hsmall C x i) (((D.refined hp hδ hsmall C hmod hcenter).representation.map x) v) = (D.chain.direction ↑i) v

theorem EGZ.FlagDecomposition.CompletePreparation.first_direction_nonconstant {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hcount : 0 < D.count) : Φ.representation.NonconstantOnFibers anchor (D.chain.direction 0)

theorem EGZ.FlagDecomposition.CompletePreparation.lower_refined_level_lt {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (hmod : ∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (hcount : 0 < D.count) (x : (D.split hp hδ hsmall).flag.Node) (hx : (↑↑x).2 = 0) : Φ.level anchor < (D.refined hp hδ hsmall C hmod hcenter).level x

Each surviving lower node has strictly greater level than the old anchor as soon as at least one thin direction was selected.

theorem EGZ.FlagDecomposition.CompletePreparation.completeNode_level_lt {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (hmod : ∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (hcount : 0 < D.count) : Φ.level anchor < (D.refined hp hδ hsmall C hmod hcenter).level (D.completeNode hp hδ hsmall C hmod hcenter)

theorem EGZ.FlagDecomposition.CompletePreparation.completeNode_level_lt_of_not_complete {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {anchor : Φ.flag.Node} {t : ℕ → ℕ} {δ : ℝ} (D : Φ.CompletePreparation anchor t δ) (hp : Odd p) (hδ : 0 ≤ δ) (hsmall : 3 ^ (d + 1) * δ < 1) (C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x)) (hmod : ∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (T : ℕ) (hwidth : T ≤ t 1) (hnot : ¬Φ.IsCompleteElement anchor T δ) : Φ.level anchor < (D.refined hp hδ hsmall C hmod hcenter).level (D.completeNode hp hδ hsmall C hmod hcenter)

Failure of completeness at the trigger width yields the strict level increase required by the iteration.