Levels and coordinate injectivity of normalized operations #
Reduced restriction leaves the level calculations intact. These wrappers state the comparisons using the actual normalized subdivision maps, ready for tracking persistent nodes through an iteration.
theorem
EGZ.FlagDecomposition.FaceRefinement.normalized_level_le
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(anchor : Φ.flag.Node)
(Γ : (Φ.flag.polytope anchor).Face)
(hp : Odd p)
(C :
(x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) →
IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x))
(hmod :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p))
(hcenter :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(x : (normalized Φ anchor Γ hp C hmod hcenter).flag.Node)
:
Φ.level ((normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).node x) ≤ (normalized Φ anchor Γ hp C hmod hcenter).level x
theorem
EGZ.FlagDecomposition.FaceRefinement.normalized_lower_level_lt
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(anchor : Φ.flag.Node)
(Γ : (Φ.flag.polytope anchor).Face)
(hp : Odd p)
(C :
(x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) →
IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x))
(hmod :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p))
(hcenter :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(hΓ : Γ.carrier ⊂ (Φ.flag.polytope anchor).carrier)
(x : (normalized Φ anchor Γ hp C hmod hcenter).flag.Node)
(hx : (↑↑↑x).2 = 0)
:
theorem
EGZ.FlagDecomposition.FaceRefinement.normalizedTargetNode_level_eq
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(anchor : Φ.flag.Node)
(Γ : (Φ.flag.polytope anchor).Face)
(hp : Odd p)
(C :
(x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) →
IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x))
(hmod :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p))
(hcenter :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(hΦ : Φ.IsMinimal)
(hΓ : Γ ≠ ⊤)
(hred : Φ.IsReducedElement anchor)
:
(normalized Φ anchor Γ hp C hmod hcenter).level (normalizedTargetNode Φ anchor Γ hp C hmod hcenter hΓ hred) = Φ.level anchor
theorem
EGZ.FlagDecomposition.FaceRefinement.normalizedSubdivisionMap_fibre_injective
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(anchor : Φ.flag.Node)
(Γ : (Φ.flag.polytope anchor).Face)
(hp : Odd p)
(C :
(x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) →
IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x))
(hmod :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p))
(hcenter :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(x : (normalized Φ anchor Γ hp C hmod hcenter).flag.Node)
:
Function.Injective ⇑((normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).fibre x)
Face refinement uses injective charts at every surviving node.
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_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.normalized hp hδ hsmall C hmod hcenter).flag.Node)
:
Φ.level ((D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).node x) ≤ (D.normalized hp hδ hsmall C hmod hcenter).level x
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_lower_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.normalized hp hδ hsmall C hmod hcenter).flag.Node)
(hx : (↑↑↑x).2 = 0)
:
theorem
EGZ.FlagDecomposition.CompletePreparation.normalizedCompleteNode_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.normalized hp hδ hsmall C hmod hcenter).level (D.normalizedCompleteNode hp hδ hsmall C hmod hcenter)
theorem
EGZ.FlagDecomposition.CompletePreparation.normalizedSubdivisionMap_fibre_injective_of_level_eq
{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.normalized hp hδ hsmall C hmod hcenter).flag.Node)
(hlevel :
Φ.level ((D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).node x) = (D.normalized hp hδ hsmall C hmod hcenter).level x)
:
Function.Injective ⇑((D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).fibre x)
At a persistent level, forgetting added coordinates is injective on the whole real coordinate space of the surviving normalized node.