The convex flag in minimal lattice coordinates

Choose a support-generated integer lattice chart at every node. Rebuilding the support polytopes and factoring the old transitions through these charts gives a convex flag on the same node poset with standard coordinate lattices.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.originalWeights {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Φ.PrunedWeights

The original local weights as a collection of surviving weights.

Equations

• Φ.originalWeights = { weight := Φ.localWeight, weight_le := ⋯, nonzero := ⋯ }

theorem EGZ.FlagDecomposition.transition_mem_liftedSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {x y : Φ.flag.Node} (h : x ≤ y) {q : IntCoord (Φ.flag.rank x)} (hq : q ∈ Φ.liftedSupport x) : (Φ.flag.transition h).integer q ∈ Φ.liftedSupport y

Original transitions carry each lifted support into the upper lifted support, with no additional prime or coordinate-bound hypothesis.

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

The coordinate chart at a node, with real and modular realizations.

Equations

• EGZ.FlagDecomposition.Rechart.chart Φ C x = EGZ.IntegralAffineMap.ofIntAffineMap (C x).map

theorem EGZ.FlagDecomposition.Rechart.chart_real_injective {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) : Function.Injective ⇑(chart Φ C x).real

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

The new node polytope is the hull of its support in the new coordinates.

Equations

• EGZ.FlagDecomposition.Rechart.polytope Φ C x = EGZ.RationalPolytope.ofFinsetConvexHull (Finset.image EGZ.IntCoord.real (C x).coordinateSupport) ⋯ ⋯

@[simp]

theorem EGZ.FlagDecomposition.Rechart.polytope_carrier {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) : (polytope Φ C x).carrier = (convexHull ℝ) (IntCoord.real '' ↑(C x).coordinateSupport)

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

The chart maps the new polytope onto the original one.

@[simp]

theorem EGZ.FlagDecomposition.Rechart.chart_mem_polytope_iff {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) : (chart Φ C x).real q ∈ (Φ.flag.polytope x).carrier ↔ q ∈ (polytope Φ C x).carrier

theorem EGZ.FlagDecomposition.Rechart.polytope_bound {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) {K B : Φ.flag.Node → ℕ} (hΦ : Φ.IsKBounded K) (hC : ∀ (x : Φ.flag.Node) (q : IntCoord (C x).rank), latticeSupNorm ((C x).map q) ≤ K x → latticeSupNorm q ≤ B x) (x : Φ.flag.Node) (q : IntCoord (C x).rank) : q.real ∈ (polytope Φ C x).carrier → latticeSupNorm q ≤ B x

The uniform chart box bounds transfer boundedness of the original decomposition to every lattice point of each new polytope.

theorem EGZ.FlagDecomposition.Rechart.transition_support {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {x y : Φ.flag.Node} (h : x ≤ y) (z : IntCoord (Φ.flag.rank x)) : z ∈ Φ.liftedSupport x → (Φ.flag.transition h).toIntAffineMap z ∈ affineSpan ℤ ↑(Φ.liftedSupport y)

Support membership supplies the target-lattice condition for factoring the original transition through the chosen charts.

noncomputable def EGZ.FlagDecomposition.Rechart.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) : IntegralAffineMap (C x).rank (C y).rank

Original transitions expressed in the chosen lattice charts.

Equations

• EGZ.FlagDecomposition.Rechart.transition Φ C h = EGZ.IntegralAffineMap.ofIntAffineMap ((C x).transition (C y) (Φ.flag.transition h).toIntAffineMap ⋯)

theorem EGZ.FlagDecomposition.Rechart.chart_comp_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) : (chart Φ C y).comp (transition Φ C h) = (Φ.flag.transition h).comp (chart Φ C x)

Chart maps intertwine new and old transitions as integral-affine maps.

theorem EGZ.FlagDecomposition.Rechart.chart_transition_real {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 (C x).rank) : (chart Φ C y).real ((transition Φ C h).real q) = (Φ.flag.transition h).real ((chart Φ C x).real q)

theorem EGZ.FlagDecomposition.Rechart.chart_transition_modp {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) (r : ℕ) (q : FpCoord r (C x).rank) : ((chart Φ C y).modp r) (((transition Φ C h).modp r) q) = ((Φ.flag.transition h).modp r) (((chart Φ C x).modp r) q)

theorem EGZ.FlagDecomposition.Rechart.transition_mem {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 (C x).rank} (hq : q ∈ (polytope Φ C x).carrier) : (transition Φ C h).real q ∈ (polytope Φ C y).carrier

theorem EGZ.FlagDecomposition.Rechart.transition_refl {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) : transition Φ C ⋯ = IntegralAffineMap.id (C x).rank

theorem EGZ.FlagDecomposition.Rechart.transition_trans {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) {x y z : Φ.flag.Node} (hxy : x ≤ y) (hyz : y ≤ z) : transition Φ C ⋯ = (transition Φ C hyz).comp (transition Φ C hxy)

@[reducible, inline]

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

The convex flag obtained by replacing every fibre with its support-generated lattice coordinates.

Equations

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