A decomposition in support-generated lattice coordinates

The recharted flag and finite-field representation form an actual flag decomposition. Every face contains a new support generator; lifting its old chart image to an old local generator produces a new proper point over that face. All weights and lifted masses are preserved, and the new decomposition has minimal ambient affine spaces and integer lattices.

theorem EGZ.FlagDecomposition.Rechart.raw_hat {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (q : IntCoord (C x).rank) : FlagDecompositionRaw.hat (representation Φ C hp hinj) Φ.localWeight x q = Φ.hat x ((C x).map q)

theorem EGZ.FlagDecomposition.Rechart.raw_localLift {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (q : IntCoord (C x).rank) : FlagDecompositionRaw.localLift (representation Φ C hp hinj) Φ.localWeight x q = Φ.localLift x ((C x).map q)

theorem EGZ.FlagDecomposition.Rechart.faces_visible {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (Γ : (polytope Φ C x).Face) : FlagDecompositionRaw.VisibleFace (representation Φ C hp hinj) Φ.localWeight x Γ

Every new face is visible to a local generator transported from the old decomposition. This proves the visibility field of the new decomposition.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.Rechart.decomposition {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : FlagDecomposition p d f

Replace every fibre by its support-generated integer lattice coordinates and every ambient affine space by its cumulative support span.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.Rechart.decomposition_localWeight {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : (decomposition Φ C hp hinj hcenter).localWeight x = Φ.localWeight x

@[simp]

theorem EGZ.FlagDecomposition.Rechart.decomposition_cumulativeWeight {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : (decomposition Φ C hp hinj hcenter).cumulativeWeight x = Φ.cumulativeWeight x

@[simp]

theorem EGZ.FlagDecomposition.Rechart.decomposition_retainedWeight {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (decomposition Φ C hp hinj hcenter).retainedWeight = Φ.retainedWeight

@[simp]

theorem EGZ.FlagDecomposition.Rechart.decomposition_retainedMass {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (decomposition Φ C hp hinj hcenter).retainedMass = Φ.retainedMass

@[simp]

theorem EGZ.FlagDecomposition.Rechart.decomposition_liftedSupport {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : (decomposition Φ C hp hinj hcenter).liftedSupport x = (C x).coordinateSupport

@[simp]

theorem EGZ.FlagDecomposition.Rechart.decomposition_hat {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (q : IntCoord (C x).rank) : (decomposition Φ C hp hinj hcenter).hat x q = Φ.hat x ((C x).map q)

@[simp]

theorem EGZ.FlagDecomposition.Rechart.decomposition_localLift {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (q : IntCoord (C x).rank) : (decomposition Φ C hp hinj hcenter).localLift x q = Φ.localLift x ((C x).map q)

theorem EGZ.FlagDecomposition.Rechart.decomposition_isMinimal {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (decomposition Φ C hp hinj hcenter).IsMinimal

The new ambient spaces and integer coordinate supports satisfy both minimality conditions.

theorem EGZ.FlagDecomposition.Rechart.decomposition_isKBounded {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) {K B : Φ.flag.Node → ℕ} (hΦ : Φ.IsKBounded K) (hC : ∀ (x : Φ.flag.Node) (q : IntCoord (C x).rank), latticeSupNorm ((C x).map q) ≤ K x → latticeSupNorm q ≤ B x) : (decomposition Φ C hp hinj hcenter).IsKBounded B

theorem EGZ.FlagDecomposition.Rechart.decomposition_gap {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : (decomposition Φ C hp hinj hcenter).gap x = Φ.gap x

Recharting preserves the complete finite set of positive lifted masses, so in particular it preserves their minimum.