Convex flags from finite lattice-support diagrams

Finite nonempty integer supports and compatible support-preserving integral transitions already determine a convex flag. No finite-field representation is required. Choosing the support-generated lattice charts gives a new diagram and a convex flag in minimal integer lattice coordinates.

structure EGZ.LatticeSupportDiagram : Type (u + 1)

The discrete data needed to construct a flag of finite support hulls.

• Node : Type u

  The finite ordered indexing type of the lattice support diagram.

• nodeFintype : Fintype self.Node
• nodeSemilatticeSup : SemilatticeSup self.Node
• nodeOrderTop : OrderTop self.Node
• rank : self.Node → ℕ

  The number of integral coordinates attached to each node.

• support (x : self.Node) : Finset (IntCoord (self.rank x))

  The nonempty finite lattice support attached to each node.

• support_nonempty (x : self.Node) : (self.support x).Nonempty
• transition {x y : self.Node} : x ≤ y → IntegralAffineMap (self.rank x) (self.rank y)

  The integral affine map transporting coordinates along an order relation between nodes.

• transition_support {x y : self.Node} (h : x ≤ y) {q : IntCoord (self.rank x)} : q ∈ self.support x → (self.transition h).integer q ∈ self.support y
• transition_refl (x : self.Node) : self.transition ⋯ = IntegralAffineMap.id (self.rank x)
• transition_trans {x y z : self.Node} (hxy : x ≤ y) (hyz : y ≤ z) : self.transition ⋯ = (self.transition hyz).comp (self.transition hxy)

noncomputable def EGZ.LatticeSupportDiagram.polytope (D : LatticeSupportDiagram) (x : D.Node) : RationalPolytope (D.rank x)

The rational hull of the integer support at one node.

Equations

• D.polytope x = EGZ.RationalPolytope.ofFinsetConvexHull (Finset.image EGZ.IntCoord.real (D.support x)) ⋯ ⋯

@[simp]

theorem EGZ.LatticeSupportDiagram.polytope_carrier (D : LatticeSupportDiagram) (x : D.Node) : (D.polytope x).carrier = (convexHull ℝ) (IntCoord.real '' ↑(D.support x))

theorem EGZ.LatticeSupportDiagram.transition_mem (D : LatticeSupportDiagram) {x y : D.Node} (h : x ≤ y) {q : RealCoord (D.rank x)} (hq : q ∈ (D.polytope x).carrier) : (D.transition h).real q ∈ (D.polytope y).carrier

@[reducible, inline]

noncomputable abbrev EGZ.LatticeSupportDiagram.toConvexFlag (D : LatticeSupportDiagram) : ConvexFlag

A support diagram always defines a convex flag with standard lattices.

Equations

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

noncomputable def EGZ.LatticeSupportDiagram.chart (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (x : D.Node) : IntegralAffineMap (C x).rank (D.rank x)

Real, integer, and modular realizations of the chosen lattice chart.

Equations

• D.chart C x = EGZ.IntegralAffineMap.ofIntAffineMap (C x).map

theorem EGZ.LatticeSupportDiagram.chart_real_injective (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (x : D.Node) : Function.Injective ⇑(D.chart C x).real

theorem EGZ.LatticeSupportDiagram.transition_affineSpan (D : LatticeSupportDiagram) {x y : D.Node} (h : x ≤ y) (z : IntCoord (D.rank x)) : z ∈ D.support x → (D.transition h).toIntAffineMap z ∈ affineSpan ℤ ↑(D.support y)

noncomputable def EGZ.LatticeSupportDiagram.chartedTransition (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) {x y : D.Node} (h : x ≤ y) : IntegralAffineMap (C x).rank (C y).rank

Express the diagram transitions in the support-generated lattice charts.

Equations

• D.chartedTransition C h = EGZ.IntegralAffineMap.ofIntAffineMap ((C x).transition (C y) (D.transition h).toIntAffineMap ⋯)

theorem EGZ.LatticeSupportDiagram.chart_comp_transition (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) {x y : D.Node} (h : x ≤ y) : (D.chart C y).comp (D.chartedTransition C h) = (D.transition h).comp (D.chart C x)

theorem EGZ.LatticeSupportDiagram.chart_transition_real (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) {x y : D.Node} (h : x ≤ y) (q : RealCoord (C x).rank) : (D.chart C y).real ((D.chartedTransition C h).real q) = (D.transition h).real ((D.chart C x).real q)

theorem EGZ.LatticeSupportDiagram.chart_transition_modp (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) {x y : D.Node} (h : x ≤ y) (p : ℕ) (q : FpCoord p (C x).rank) : ((D.chart C y).modp p) (((D.chartedTransition C h).modp p) q) = ((D.transition h).modp p) (((D.chart C x).modp p) q)

theorem EGZ.LatticeSupportDiagram.chartedTransition_support (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) {x y : D.Node} (h : x ≤ y) {q : IntCoord (C x).rank} (hq : q ∈ (C x).coordinateSupport) : (D.chartedTransition C h).integer q ∈ (C y).coordinateSupport

theorem EGZ.LatticeSupportDiagram.chartedTransition_refl (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (x : D.Node) : D.chartedTransition C ⋯ = IntegralAffineMap.id (C x).rank

theorem EGZ.LatticeSupportDiagram.chartedTransition_trans (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) {x y z : D.Node} (hxy : x ≤ y) (hyz : y ≤ z) : D.chartedTransition C ⋯ = (D.chartedTransition C hyz).comp (D.chartedTransition C hxy)

@[reducible, inline]

noncomputable abbrev EGZ.LatticeSupportDiagram.rechart (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) : LatticeSupportDiagram

The same support diagram in the new lattice coordinates.

Equations

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

@[reducible, inline]

noncomputable abbrev EGZ.LatticeSupportDiagram.chartedFlag (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) : ConvexFlag

An actual convex flag in support-generated lattice coordinates.

Equations

• D.chartedFlag C = (D.rechart C).toConvexFlag

theorem EGZ.LatticeSupportDiagram.chartedSupport_affineIntSpans (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (x : D.Node) : FlagDecomposition.AffineIntSpans ((D.rechart C).support x)

theorem EGZ.LatticeSupportDiagram.chart_image_polytope (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (x : D.Node) : ⇑(D.chart C x).real '' ((D.rechart C).polytope x).carrier = (D.polytope x).carrier

Every chart maps the new support hull onto the original support hull.

theorem EGZ.LatticeSupportDiagram.chart_mem_polytope_iff (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (x : D.Node) (q : RealCoord (C x).rank) : (D.chart C x).real q ∈ (D.polytope x).carrier ↔ q ∈ ((D.rechart C).polytope x).carrier

theorem EGZ.LatticeSupportDiagram.charted_polytope_bound (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) {K B : D.Node → ℕ} (hD : ∀ (x : D.Node) (z : IntCoord (D.rank x)), z.real ∈ (D.polytope x).carrier → latticeSupNorm z ≤ K x) (hC : ∀ (x : D.Node) (q : IntCoord (C x).rank), latticeSupNorm ((C x).map q) ≤ K x → latticeSupNorm q ≤ B x) (x : D.Node) (q : IntCoord (C x).rank) : q.real ∈ ((D.rechart C).polytope x).carrier → latticeSupNorm q ≤ B x

Chart box bounds transfer integer-point bounds on the original support hulls to integer-point bounds on the new hulls.