Lifted mass in new lattice coordinates

An injective modular chart and centered new support coordinates identify the old and new centered fibres on every ambient atom carrying cumulative mass. Summing that pointwise identification proves exact transport for every weight bounded by the cumulative weight, including the local summand.

noncomputable def EGZ.FlagDecompositionRaw.centeredFibreMass {p d n : ℕ} [NeZero p] (w : FpCoord p d → ℕ) (φ : FpCoord p d → FpCoord p n) (q : IntCoord n) : ℕ

The centered lift of a weight through one coordinate map.

Equations

• EGZ.FlagDecompositionRaw.centeredFibreMass w φ q = if EGZ.IsCenteredLift p q then EGZ.FlagDecompositionRaw.affineFibreMass w φ (EGZ.IntCoord.mod p q) else 0

theorem EGZ.FlagDecompositionRaw.centeredFibreMass_eq_sum {p d n : ℕ} [NeZero p] (w : FpCoord p d → ℕ) (φ : FpCoord p d → FpCoord p n) (q : IntCoord n) : centeredFibreMass w φ q = ∑ v : FpCoord p d, if IsCenteredLift p q ∧ φ v = IntCoord.mod p q then w v else 0

noncomputable def EGZ.IntegerLatticeChart.rechartMap {p d n : ℕ} [Fact (Nat.Prime p)] {S : Finset (IntCoord n)} (C : IntegerLatticeChart S) (φ : FpCoord p d →ᵃ[ZMod p] FpCoord p n) : FpCoord p d →ᵃ[ZMod p] FpCoord p C.rank

Express a finite-field representation map in the chart coordinates.

Equations

• C.rechartMap φ = (EGZ.affineLeftInverse ((EGZ.IntegralAffineMap.ofIntAffineMap C.map).modp p)).comp φ

theorem EGZ.FlagDecomposition.centeredLift_mem_liftedSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) {v : FpCoord p d} (hv : Φ.cumulativeWeight x v ≠ 0) : ((Φ.representation.map x) v).centeredLift ∈ Φ.liftedSupport x

Every ambient atom carrying cumulative mass lifts into the stored support.

theorem EGZ.FlagDecomposition.rechartMap_eq_coordinates_mod {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (C : IntegerLatticeChart (Φ.liftedSupport x)) (hmod : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap C.map).modp p)) {v : FpCoord p d} (hv : Φ.cumulativeWeight x v ≠ 0) : (C.rechartMap (Φ.representation.map x)) v = IntCoord.mod p (C.coordinates ((Φ.representation.map x) v).centeredLift)

On a supported atom the new finite-field coordinate is the reduction of the inverse chart coordinate of its old centered lift.

theorem EGZ.FlagDecomposition.rechart_centered_fibre_iff {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (C : IntegerLatticeChart (Φ.liftedSupport x)) (hmod : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap C.map).modp p)) (hcenter : ∀ q ∈ C.coordinateSupport, IsCenteredLift p q) {v : FpCoord p d} (hv : Φ.cumulativeWeight x v ≠ 0) (q : IntCoord C.rank) : IsCenteredLift p q ∧ (C.rechartMap (Φ.representation.map x)) v = IntCoord.mod p q ↔ IsCenteredLift p (C.map q) ∧ (Φ.representation.map x) v = IntCoord.mod p (C.map q)

Centered old and new fibre conditions agree on every supported atom, including when the displayed test coordinate is outside a centered box.

theorem EGZ.FlagDecomposition.centeredFibreMass_rechart {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (C : IntegerLatticeChart (Φ.liftedSupport x)) (hmod : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap C.map).modp p)) (hcenter : ∀ q ∈ C.coordinateSupport, IsCenteredLift p q) (w : FpCoord p d → ℕ) (hw : w ≤ Φ.cumulativeWeight x) (q : IntCoord C.rank) : FlagDecompositionRaw.centeredFibreMass w (⇑(C.rechartMap (Φ.representation.map x))) q = FlagDecompositionRaw.centeredFibreMass w (⇑(Φ.representation.map x)) (C.map q)

Exact transport of any centered lifted weight dominated by the old cumulative weight. The equality holds at every integer coordinate.

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

Cumulative lifted mass is unchanged after expressing the support in its own integer lattice coordinates.

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

The same exact transport holds for the local lift defining proper-point generators, not just for cumulative mass.

theorem EGZ.FlagDecomposition.coordinateSupport_spec_rechart {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (C : IntegerLatticeChart (Φ.liftedSupport x)) (hmod : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap C.map).modp p)) (hcenter : ∀ q ∈ C.coordinateSupport, IsCenteredLift p q) (q : IntCoord C.rank) : q ∈ C.coordinateSupport ↔ FlagDecompositionRaw.centeredFibreMass (Φ.cumulativeWeight x) (⇑(C.rechartMap (Φ.representation.map x))) q ≠ 0

The support transported by the chart is exactly the nonzero support of the recharted cumulative lift.