Recharting supported fibre masses without a representation #
Exact centered-mass transport uses only a support-generated lattice chart, modular injectivity, and containment of the supported centered lifts in the old support. The original finite-field affine map need not be surjective.
theorem
EGZ.FlagDecompositionRaw.centeredFibreMass_ne_zero_iff
{p d n : ℕ}
[NeZero p]
(w : FpCoord p d → ℕ)
(φ : FpCoord p d → FpCoord p n)
(q : IntCoord n)
:
centeredFibreMass w φ q ≠ 0 ↔ IsCenteredLift p q ∧ ∃ (v : FpCoord p d), φ v = IntCoord.mod p q ∧ w v ≠ 0
theorem
EGZ.IntegerLatticeChart.rechartMap_eq_coordinates_mod_of_mem
{p d n : ℕ}
[Fact (Nat.Prime p)]
{S : Finset (IntCoord n)}
(C : IntegerLatticeChart S)
(φ : FpCoord p d →ᵃ[ZMod p] FpCoord p n)
(hmod : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap C.map).modp p))
{v : FpCoord p d}
(hv : (φ v).centeredLift ∈ S)
:
theorem
EGZ.IntegerLatticeChart.rechart_centered_fibre_iff
{p d n : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{S : Finset (IntCoord n)}
(C : IntegerLatticeChart S)
(φ : FpCoord p d →ᵃ[ZMod p] FpCoord p n)
(hmod : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap C.map).modp p))
(hp : Odd p)
(hcenter : ∀ q ∈ C.coordinateSupport, IsCenteredLift p q)
{v : FpCoord p d}
(hv : (φ v).centeredLift ∈ S)
(q : IntCoord C.rank)
:
IsCenteredLift p q ∧ (C.rechartMap φ) v = IntCoord.mod p q ↔ IsCenteredLift p (C.map q) ∧ φ v = IntCoord.mod p (C.map q)
theorem
EGZ.IntegerLatticeChart.centeredFibreMass_rechart
{p d n : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{S : Finset (IntCoord n)}
(C : IntegerLatticeChart S)
(φ : FpCoord p d →ᵃ[ZMod p] FpCoord p n)
(hmod : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap C.map).modp p))
(hp : Odd p)
(hcenter : ∀ q ∈ C.coordinateSupport, IsCenteredLift p q)
(w : FpCoord p d → ℕ)
(hwS : ∀ (v : FpCoord p d), w v ≠ 0 → (φ v).centeredLift ∈ S)
(q : IntCoord C.rank)
:
FlagDecompositionRaw.centeredFibreMass w (⇑(C.rechartMap φ)) q = FlagDecompositionRaw.centeredFibreMass w (⇑φ) (C.map q)
Exact mass transport for arbitrary supported weights and an affine map which is not required to be surjective.
theorem
EGZ.IntegerLatticeChart.coordinateSupport_spec_rechart
{p d n : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{S : Finset (IntCoord n)}
(C : IntegerLatticeChart S)
(φ : FpCoord p d →ᵃ[ZMod p] FpCoord p n)
(hmod : Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap C.map).modp p))
(hp : Odd p)
(hcenter : ∀ q ∈ C.coordinateSupport, IsCenteredLift p q)
(w : FpCoord p d → ℕ)
(hS : ∀ (z : IntCoord n), z ∈ S ↔ FlagDecompositionRaw.centeredFibreMass w (⇑φ) z ≠ 0)
(q : IntCoord C.rank)
:
If the old support is exactly the nonzero centered fibre support, its chart-coordinate support is exactly the new nonzero centered fibre support.