Level comparison for mass-transport maps #
For a minimal output decomposition, compatibility on cumulative support extends to its whole represented affine space. Thus a node mass map already contains all data needed for level monotonicity and equal-level coordinate injectivity; no extra transport fields are required.
theorem
EGZ.FlagDecomposition.NodeMassMap.space_le
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ Ψ : FlagDecomposition p d f}
{x : Φ.flag.Node}
{y : Ψ.flag.Node}
(M : Φ.NodeMassMap Ψ x y)
(hΨ : Ψ.IsMinimal)
:
theorem
EGZ.FlagDecomposition.NodeMassMap.map_eq_on_space
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ Ψ : FlagDecomposition p d f}
{x : Φ.flag.Node}
{y : Ψ.flag.Node}
(M : Φ.NodeMassMap Ψ x y)
(hΨ : Ψ.IsMinimal)
(v : FpCoord p d)
(hv : v ∈ Ψ.representation.space y)
:
Compatibility extends from the support to its full affine span.
theorem
EGZ.FlagDecomposition.NodeMassMap.modp_injective_of_level_eq
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ Ψ : FlagDecomposition p d f}
{x : Φ.flag.Node}
{y : Ψ.flag.Node}
(M : Φ.NodeMassMap Ψ x y)
(hΨ : Ψ.IsMinimal)
(hlevel : Φ.level x = Ψ.level y)
:
Function.Injective ⇑(M.coord.modp p)