Properties preserved by changing lattice coordinates

The chart and its affine left inverse identify the node polytopes and their proper points. These maps preserve reducedness, realized faces, and completeness of individual elements.

noncomputable def EGZ.FlagDecomposition.Rechart.inverseChart {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) : RealCoord (Φ.flag.rank x) →ᵃ[ℝ] RealCoord (C x).rank

An affine inverse of the real chart, extended to the old ambient space.

Equations

• EGZ.FlagDecomposition.Rechart.inverseChart Φ C x = EGZ.affineLeftInverse (EGZ.FlagDecomposition.Rechart.chart Φ C x).real

@[simp]

theorem EGZ.FlagDecomposition.Rechart.inverseChart_chart {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) (q : RealCoord (C x).rank) : (inverseChart Φ C x) ((chart Φ C x).real q) = q

theorem EGZ.FlagDecomposition.Rechart.chart_inverseChart {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) (q : RealCoord (Φ.flag.rank x)) (hq : q ∈ (Φ.flag.polytope x).carrier) : (chart Φ C x).real ((inverseChart Φ C x) q) = q

theorem EGZ.FlagDecomposition.Rechart.inverseChart_mem_polytope {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) : Set.MapsTo (⇑(inverseChart Φ C x)) (Φ.flag.polytope x).carrier (polytope Φ C x).carrier

theorem EGZ.FlagDecomposition.Rechart.chart_mem_polytope {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) : Set.MapsTo (⇑(chart Φ C x).real) (polytope Φ C x).carrier (Φ.flag.polytope x).carrier

theorem EGZ.FlagDecomposition.Rechart.inverseChart_transition {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) {x y : Φ.flag.Node} (h : x ≤ y) (q : RealCoord (Φ.flag.rank x)) (hq : q ∈ (Φ.flag.polytope x).carrier) : (inverseChart Φ C y) ((Φ.flag.transition h).real q) = (transition Φ C h).real ((inverseChart Φ C x) q)

Inverse charts commute with transitions on the old source polytope.

noncomputable def EGZ.FlagDecomposition.Rechart.forwardPoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (q : (flag Φ C).Point) : Φ.flag.Point

Map a point in the new coordinates to its original flag point.

Equations

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

noncomputable def EGZ.FlagDecomposition.Rechart.inversePoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (q : Φ.flag.Point) : (flag Φ C).Point

Express an original flag point in the new coordinates.

Equations

• EGZ.FlagDecomposition.Rechart.inversePoint Φ C q = q.map (SupHom.id Φ.flag.Node) (EGZ.FlagDecomposition.Rechart.inverseChart Φ C) ⋯

@[simp]

theorem EGZ.FlagDecomposition.Rechart.inversePoint_forwardPoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (q : (flag Φ C).Point) : inversePoint Φ C (forwardPoint Φ C q) = q

@[simp]

theorem EGZ.FlagDecomposition.Rechart.forwardPoint_inversePoint {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (q : Φ.flag.Point) : forwardPoint Φ C (inversePoint Φ C q) = q

theorem EGZ.FlagDecomposition.Rechart.forwardPoint_mem_omegaZero {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) {q : (flag Φ C).Point} (hq : q ∈ (decomposition Φ C hp hinj hcenter).omegaZero) : forwardPoint Φ C q ∈ Φ.omegaZero

theorem EGZ.FlagDecomposition.Rechart.inversePoint_mem_omegaZero {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) {q : Φ.flag.Point} (hq : q ∈ Φ.omegaZero) : inversePoint Φ C q ∈ (decomposition Φ C hp hinj hcenter).omegaZero

theorem EGZ.FlagDecomposition.Rechart.forwardPoint_mem_omega {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) {q : (flag Φ C).Point} (hq : q ∈ (decomposition Φ C hp hinj hcenter).omega) : forwardPoint Φ C q ∈ Φ.omega

Forward charts preserve the full proper-point set.

theorem EGZ.FlagDecomposition.Rechart.inversePoint_mem_omega {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) {q : Φ.flag.Point} (hq : q ∈ Φ.omega) : inversePoint Φ C q ∈ (decomposition Φ C hp hinj hcenter).omega

The inverse charts preserve proper points even though their transition commutation is only required on the polytopes.

noncomputable def EGZ.FlagDecomposition.Rechart.subdivisionMap {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) : Φ.SubdivisionMap (decomposition Φ C hp hinj hcenter)

The new decomposition is a subdivision of the old one through its coordinate charts.

Equations

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

theorem EGZ.FlagDecomposition.Rechart.decomposition_isReduced {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) (hΦ : Φ.IsReduced) : (decomposition Φ C hp hinj hcenter).IsReduced

Recharting preserves every base occurring among the proper points.

theorem EGZ.FlagDecomposition.Rechart.decomposition_isReduced_iff {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) : (decomposition Φ C hp hinj hcenter).IsReduced ↔ Φ.IsReduced

theorem EGZ.FlagDecomposition.Rechart.face_preimage_nonempty {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) : ((polytope Φ C x).carrier ∩ ⇑(chart Φ C x).real ⁻¹' Γ.carrier).Nonempty

Every old face has a nonempty pullback under a chart.

theorem EGZ.FlagDecomposition.Rechart.decomposition_isRealizedFace {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) (Γ : (Φ.flag.polytope x).Face) (hΓ : Φ.IsRealizedFace x Γ) : (decomposition Φ C hp hinj hcenter).IsRealizedFace x ((subdivisionMap Φ C hp hinj hcenter).face x Γ ⋯)

Every previously realized face is still realized in the new coordinates.

theorem EGZ.FlagDecomposition.Rechart.nonconstantOnFibers_original {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)) (x : Φ.flag.Node) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (hξ : (representation Φ C hp hinj).NonconstantOnFibers x ξ) : Φ.representation.NonconstantOnFibers x ξ

A functional varying on new representation fibres already varies on old representation fibres.

theorem EGZ.FlagDecomposition.Rechart.decomposition_isCompleteElement {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) (t : ℕ) (δ : ℝ) (hcomplete : Φ.IsCompleteElement x t δ) : (decomposition Φ C hp hinj hcenter).IsCompleteElement x t δ

Element completeness is preserved with exactly the same thresholds.