Decompositions with additional affine coordinates

Appending a common prefix of slab coordinates and then choosing the generated integer lattice charts yields an actual minimal decomposition on the same nodes and with the same local weights. Forgetting the additional coordinates maps its proper points to the original decomposition.

theorem EGZ.FlagDecomposition.isReducedElement_iff_sup'_localWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) : Φ.IsReducedElement x ↔ ∃ (s : Finset Φ.flag.Node) (hs : s.Nonempty), (∀ y ∈ s, ∃ (v : FpCoord p d), Φ.localWeight y v ≠ 0) ∧ s.sup' hs id = x

Reduced nodes depend only on the bases carrying nonzero local weight, and are unchanged when the coordinate maps or polytopes are replaced.

theorem EGZ.FlagDecomposition.Augmented.lift_eq_centeredLift {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) (x : Φ.flag.Node) (v : FpCoord p d) : lift Φ e ξ x v = ((map Φ e ξ x) v).centeredLift

theorem EGZ.FlagDecomposition.Augmented.support_spec_centeredFibreMass {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) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x + e x)) : q ∈ support Φ e ξ x ↔ FlagDecompositionRaw.centeredFibreMass (Φ.cumulativeWeight x) (⇑(map Φ e ξ x)) q ≠ 0

The augmented supports are exactly the nonzero centered cumulative fibres, even though the augmented affine maps need not be surjective.

theorem EGZ.FlagDecomposition.Augmented.centeredLift_map_mem_support {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) (x : Φ.flag.Node) (v : FpCoord p d) (hv : Φ.cumulativeWeight x v ≠ 0) : ((map Φ e ξ x) v).centeredLift ∈ support Φ e ξ x

theorem EGZ.FlagDecomposition.Augmented.localLift_first_ne_zero {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) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x + e x)) (hq : FlagDecompositionRaw.centeredFibreMass (Φ.localWeight x) (⇑(map Φ e ξ x)) q ≠ 0) : Φ.localLift x ((Coord.first (Φ.flag.rank x) (e x)) q) ≠ 0

Forgetting the additional coordinates sends a nonzero augmented local fibre to a nonzero original local fibre.

noncomputable def EGZ.FlagDecomposition.Augmented.forget {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) (x : Φ.flag.Node) : IntegralAffineMap (C x).rank (Φ.flag.rank x)

The map from charted augmented coordinates to the original coordinates.

Equations

• EGZ.FlagDecomposition.Augmented.forget Φ e ξ hp he C x = (EGZ.IntegralAffineMap.first (Φ.flag.rank x) (e x)).comp ((EGZ.FlagDecomposition.Augmented.diagram Φ e ξ hp he).chart C x)

theorem EGZ.FlagDecomposition.Augmented.forget_image_polytope {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) (x : Φ.flag.Node) : ⇑(forget Φ e ξ hp he C x).real '' (((diagram Φ e ξ hp he).chartedFlag C).polytope x).carrier = (Φ.flag.polytope x).carrier

theorem EGZ.FlagDecomposition.Augmented.forget_mem_polytope {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) (x : Φ.flag.Node) : Set.MapsTo (⇑(forget Φ e ξ hp he C x).real) (((diagram Φ e ξ hp he).chartedFlag C).polytope x).carrier (Φ.flag.polytope x).carrier

theorem EGZ.FlagDecomposition.Augmented.forget_transition {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) {x y : Φ.flag.Node} (h : x ≤ y) (q : RealCoord (C x).rank) : (forget Φ e ξ hp he C y).real ((((diagram Φ e ξ hp he).chartedFlag C).transition h).real q) = (Φ.flag.transition h).real ((forget Φ e ξ hp he C x).real q)

theorem EGZ.FlagDecomposition.Augmented.representation_space_le_original {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (x : Φ.flag.Node) : (representation Φ e ξ hp he C hmod).space x ≤ Φ.representation.space x

The new represented space is the cumulative support span and is contained in the old represented space.

theorem EGZ.FlagDecomposition.Augmented.chart_representation_map {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (x : Φ.flag.Node) (v : FpCoord p d) (hv : v ∈ (representation Φ e ξ hp he C hmod).space x) : (((diagram Φ e ξ hp he).chart C x).modp p) (((representation Φ e ξ hp he C hmod).map x) v) = (map Φ e ξ x) v

The modular chart retracts to the augmented affine map on the full represented affine space, not only on its nonzero cumulative atoms.

theorem EGZ.FlagDecomposition.Augmented.representation_map_eq_iff {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (x : Φ.flag.Node) (v w : FpCoord p d) (hv : v ∈ (representation Φ e ξ hp he C hmod).space x) (hw : w ∈ (representation Φ e ξ hp he C hmod).space x) : ((representation Φ e ξ hp he C hmod).map x) v = ((representation Φ e ξ hp he C hmod).map x) w ↔ (map Φ e ξ x) v = (map Φ e ξ x) w

theorem EGZ.FlagDecomposition.Augmented.forget_representation_map {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (x : Φ.flag.Node) (v : FpCoord p d) (hv : v ∈ (representation Φ e ξ hp he C hmod).space x) : ((forget Φ e ξ hp he C x).modp p) (((representation Φ e ξ hp he C hmod).map x) v) = (Φ.representation.map x) v

The forgotten new coordinate is exactly the original coordinate on the new represented affine space.

noncomputable def EGZ.FlagDecomposition.Augmented.supportData {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : FlagDecompositionRaw.SupportData (representation Φ e ξ hp he C hmod) Φ.localWeight

The charted augmented flag has the exact cumulative support required by the decomposition constructor.

Equations

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

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.Augmented.decomposition {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : FlagDecomposition p d f

The actual augmented and minimalized decomposition, with unchanged nodes and unchanged local weights.

Equations

• EGZ.FlagDecomposition.Augmented.decomposition Φ e ξ hp he C hmod hcenter = (EGZ.FlagDecomposition.Augmented.supportData Φ e ξ hp he C hmod hcenter).decomposition hp f ⋯

theorem EGZ.FlagDecomposition.Augmented.decomposition_isMinimal {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (decomposition Φ e ξ hp he C hmod hcenter).IsMinimal

@[simp]

theorem EGZ.FlagDecomposition.Augmented.decomposition_retainedWeight {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (decomposition Φ e ξ hp he C hmod hcenter).retainedWeight = Φ.retainedWeight

@[simp]

theorem EGZ.FlagDecomposition.Augmented.decomposition_retainedMass {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (decomposition Φ e ξ hp he C hmod hcenter).retainedMass = Φ.retainedMass

@[simp]

theorem EGZ.FlagDecomposition.Augmented.decomposition_cumulativeWeight {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : (decomposition Φ e ξ hp he C hmod hcenter).cumulativeWeight x = Φ.cumulativeWeight x

@[simp]

theorem EGZ.FlagDecomposition.Augmented.decomposition_localWeight {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : (decomposition Φ e ξ hp he C hmod hcenter).localWeight x = Φ.localWeight x

@[simp]

theorem EGZ.FlagDecomposition.Augmented.card_decomposition {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : Fintype.card (decomposition Φ e ξ hp he C hmod hcenter).flag.Node = Fintype.card Φ.flag.Node

theorem EGZ.FlagDecomposition.Augmented.decomposition_hat {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (q : IntCoord (C x).rank) : (decomposition Φ e ξ hp he C hmod hcenter).hat x q = FlagDecompositionRaw.centeredFibreMass (Φ.cumulativeWeight x) (⇑(map Φ e ξ x)) ((C x).map q)

The new centered cumulative mass is the old augmented centered mass at the image under the integer chart.

theorem EGZ.FlagDecomposition.Augmented.decomposition_localLift {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (q : IntCoord (C x).rank) : (decomposition Φ e ξ hp he C hmod hcenter).localLift x q = FlagDecompositionRaw.centeredFibreMass (Φ.localWeight x) (⇑(map Φ e ξ x)) ((C x).map q)

theorem EGZ.FlagDecomposition.Augmented.decomposition_isReducedElement_iff {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : (decomposition Φ e ξ hp he C hmod hcenter).IsReducedElement x ↔ Φ.IsReducedElement x

Changing coordinates leaves the set of reduced nodes exactly unchanged.

theorem EGZ.FlagDecomposition.Augmented.decomposition_isReduced_iff {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : (decomposition Φ e ξ hp he C hmod hcenter).IsReduced ↔ Φ.IsReduced

theorem EGZ.FlagDecomposition.Augmented.decomposition_isCompleteElement {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (t : ℕ) (δ : ℝ) (hcomplete : Φ.IsCompleteElement x t δ) : (decomposition Φ e ξ hp he C hmod hcenter).IsCompleteElement x t δ

Completeness of an old element persists when the coordinate fibres are refined by the additional affine directions.

theorem EGZ.FlagDecomposition.Augmented.decomposition_isKBounded {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) {K L B : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) (hL : ∀ (x : Φ.flag.Node) (v : FpCoord p d), Φ.cumulativeWeight x v ≠ 0 → latticeSupNorm (slabCoordinates (e x) ξ v) ≤ L x) (hC : ∀ (x : Φ.flag.Node) (q : IntCoord (C x).rank), latticeSupNorm ((C x).map q) ≤ max (K x) (L x) → latticeSupNorm q ≤ B x) : (decomposition Φ e ξ hp he C hmod hcenter).IsKBounded B

Bounds for the slab block and the chart inverse bound every integer point of the new polytope.

noncomputable def EGZ.FlagDecomposition.Augmented.forwardPoint {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (q : (decomposition Φ e ξ hp he C hmod hcenter).flag.Point) : Φ.flag.Point

Project a new flag point by forgetting the augmented coordinate block.

Equations

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

theorem EGZ.FlagDecomposition.Augmented.forwardPoint_mem_omegaZero {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) {q : (decomposition Φ e ξ hp he C hmod hcenter).flag.Point} (hq : q ∈ (decomposition Φ e ξ hp he C hmod hcenter).omegaZero) : forwardPoint Φ e ξ hp he C hmod hcenter q ∈ Φ.omegaZero

noncomputable def EGZ.FlagDecomposition.Augmented.subdivisionMap {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) : Φ.SubdivisionMap (decomposition Φ e ξ hp he C hmod hcenter)

Forgetting the slab block is a subdivision map to the original flag.

Equations

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

theorem EGZ.FlagDecomposition.Augmented.face_preimage_nonempty {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : ((((diagram Φ e ξ hp he).chartedFlag C).polytope x).carrier ∩ ⇑(forget Φ e ξ hp he C x).real ⁻¹' Γ.carrier).Nonempty

theorem EGZ.FlagDecomposition.Augmented.decomposition_isRealizedFace {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 : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x)) [Fact (Nat.Prime p)] (hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) (hΓ : Φ.IsRealizedFace x Γ) : (decomposition Φ e ξ hp he C hmod hcenter).IsRealizedFace x ((subdivisionMap Φ e ξ hp he C hmod hcenter).face x Γ ⋯)

Previously realized faces remain realized after pulling back along the old-coordinate projection.