Coordinate and mass maps for the elementary constructions

noncomputable def EGZ.FlagDecomposition.reducedStableNodeMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : (Φ.reduced hp).flag.Node) : Φ.StableNodeMap (Φ.reduced hp) (↑x) x

The stable node map identifying a node of the reduced decomposition with its original node.

Equations

• Φ.reducedStableNodeMap hp x = { coord := EGZ.IntegralAffineMap.id ((Φ.reduced hp).flag.rank x), polytope_mem := ⋯, cumulative_le := ⋯, map_eq := ⋯, mass_loss_le := ⋯ }

noncomputable def EGZ.FlagDecomposition.PrunedWeights.rebuiltStableNodeMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.rebuilt hp).flag.Node) : Φ.StableNodeMap (D.rebuilt hp) (↑x) x

The stable node map from an original node to its rebuilt pruned counterpart.

Equations

• D.rebuiltStableNodeMap hp x = { coord := EGZ.IntegralAffineMap.id ((D.rebuilt hp).flag.rank x), polytope_mem := ⋯, cumulative_le := ⋯, map_eq := ⋯, mass_loss_le := ⋯ }

noncomputable def EGZ.FlagDecomposition.PrunedWeights.cleanedStableNodeMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.cleaned hp).flag.Node) : Φ.StableNodeMap (D.cleaned hp) (↑↑x) x

The stable node map obtained by rebuilding pruned weights and then reducing the result.

Equations

• D.cleanedStableNodeMap hp x = (D.rebuiltStableNodeMap hp ↑x).comp ((D.rebuilt hp).reducedStableNodeMap hp x)

noncomputable def EGZ.FlagDecomposition.Rechart.stableNodeMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) [Fact (Nat.Prime p)] (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) : Φ.StableNodeMap (decomposition Φ C hp hinj hcenter) x x

The stable node map induced by the chosen change of integral affine coordinates.

Equations

• EGZ.FlagDecomposition.Rechart.stableNodeMap Φ C hp hinj hcenter x = { coord := EGZ.FlagDecomposition.Rechart.chart Φ C x, polytope_mem := ⋯, cumulative_le := ⋯, map_eq := ⋯, mass_loss_le := ⋯ }

noncomputable def EGZ.FlagDecomposition.FaceRefinement.upperStableNodeMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) : Φ.StableNodeMap (decomposition Φ anchor selected hp) x (upper Φ anchor selected hp x)

The stable node map from an original node to its upper copy in the face refinement.

Equations

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

noncomputable def EGZ.FlagDecomposition.LowerTransfer.stableNodeMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (x : (decomposition Φ anchor hp).flag.Node) : Φ.StableNodeMap (decomposition Φ anchor hp) (↑↑x).1 x

The stable node map from the original node underlying a node of the lower transfer.

Equations

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

noncomputable def EGZ.FlagDecomposition.Augmented.stableNodeMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) (he : Antitone e) (C : (x : (diagram Φ e ξ hp he).Node) → IntegerLatticeChart ((diagram Φ e ξ hp he).support x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : (diagram Φ e ξ hp he).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : (diagram Φ e ξ hp he).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : Φ.StableNodeMap (decomposition Φ e ξ hp he C hmod hcenter) x x

The stable node map for augmentation, using the coordinate map that forgets the added directions.

Equations

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