Convex flags

This file formalizes Definitions 3.1, 3.4, 3.5, and 3.6 of the paper. Nodes form a finite nonempty upper semilattice. Fibre coordinates are real, and each fibre carries its own affine lattice. Transitions preserve both the polytope and the chosen lattice.

The base of a point is retained as data. This is intentional: points with the same coordinate at an upper node but different domains are distinct (the 0 versus 0' phenomenon in the examples following Proposition 3.11).

structure EGZ.ConvexFlag : Type (u + 1)

A convex flag in affine-lattice coordinates.

The transition attached to x ≤ y goes from the fibre at x to the fibre at y; it is the paper's map ψ_{y,x}.

• Node : Type u

  Finite ordered set indexing the flag.

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

  Coordinate dimension at each flag node.

• polytope (x : self.Node) : RationalPolytope (self.rank x)

  Rational polytope at each flag node.

• lattice (x : self.Node) : AffineLattice (self.rank x)

  Affine lattice at each flag node.

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

  Integral affine transition along an order relation between flag nodes.

• transition_mem {x y : self.Node} (h : x ≤ y) {q : RealCoord (self.rank x)} : q ∈ (self.polytope x).carrier → (self.transition h).real q ∈ (self.polytope y).carrier
• transition_lattice {x y : self.Node} (h : x ≤ y) {q : RealCoord (self.rank x)} : q ∈ self.lattice x → (self.transition h).real q ∈ self.lattice 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)

structure EGZ.ConvexFlag.Point (F : ConvexFlag) : Type u_1

The points of a flag are dependent pairs of a base and a point of that base polytope.

• base : F.Node

  Flag node carrying this point.

• val : RealCoord (F.rank self.base)

  Real coordinates of the point at its base node.

• val_mem : self.val ∈ (F.polytope self.base).carrier

def EGZ.ConvexFlag.Point.domain {F : ConvexFlag} (q : F.Point) : Set F.Node

The upper-set domain of a flag point.

Equations

• q.domain = {x : F.Node | q.base ≤ x}

@[simp]

theorem EGZ.ConvexFlag.Point.mem_domain {F : ConvexFlag} (q : F.Point) (x : F.Node) : x ∈ q.domain ↔ q.base ≤ x

def EGZ.ConvexFlag.Point.coord {F : ConvexFlag} (q : F.Point) {x : F.Node} (h : q.base ≤ x) : RealCoord (F.rank x)

Coordinate of a point at a node in its domain.

Equations

• q.coord h = (F.transition h).real q.val

theorem EGZ.ConvexFlag.Point.coord_mem {F : ConvexFlag} (q : F.Point) {x : F.Node} (h : q.base ≤ x) : q.coord h ∈ (F.polytope x).carrier

@[simp]

theorem EGZ.ConvexFlag.Point.coord_base {F : ConvexFlag} (q : F.Point) : q.coord ⋯ = q.val

def EGZ.ConvexFlag.Point.IsIntegral {F : ConvexFlag} (q : F.Point) : Prop

A point is integral if its coordinate at its base is in that fibre's distinguished affine lattice.

Equations

• q.IsIntegral = (q.val ∈ F.lattice q.base)

theorem EGZ.ConvexFlag.Point.isIntegral_coord {F : ConvexFlag} {q : F.Point} (hq : q.IsIntegral) {x : F.Node} (h : q.base ≤ x) : q.coord h ∈ F.lattice x

def EGZ.ConvexFlag.Point.IsProjectionOf {F : ConvexFlag} (q q' : F.Point) : Prop

q is a projection of q' when q' has the larger domain and they agree on the domain of q. By the cocycle law it is enough to compare at q.base.

Equations

• q.IsProjectionOf q' = ∃ (h : q'.base ≤ q.base), q.val = q'.coord h

theorem EGZ.ConvexFlag.Point.domain_subset_of_projection {F : ConvexFlag} {q q' : F.Point} (h : q.IsProjectionOf q') : q.domain ⊆ q'.domain

theorem EGZ.ConvexFlag.Point.coord_eq_of_projection {F : ConvexFlag} {q q' : F.Point} (hbase : q'.base ≤ q.base) (hval : q.val = q'.coord hbase) {x : F.Node} (hx : q.base ≤ x) : q.coord hx = q'.coord ⋯

structure EGZ.ConvexFlag.LinearFunction (F : ConvexFlag) : Type u_1

A "linear function" in the paper: an affine functional based at one node, with constant terms allowed.

• base : F.Node

  Flag node on which the affine functional is defined.

• toAffine : RealCoord (F.rank self.base) →ᵃ[ℝ] ℝ

  Affine functional in the coordinates of its base node.

def EGZ.ConvexFlag.LinearFunction.domain {F : ConvexFlag} (xi : F.LinearFunction) : Set F.Node

The lower-set domain of a flag linear function.

Equations

• xi.domain = {x : F.Node | x ≤ xi.base}

@[simp]

theorem EGZ.ConvexFlag.LinearFunction.mem_domain {F : ConvexFlag} (xi : F.LinearFunction) (x : F.Node) : x ∈ xi.domain ↔ x ≤ xi.base

def EGZ.ConvexFlag.LinearFunction.EvaluableAt {F : ConvexFlag} (xi : F.LinearFunction) (q : F.Point) : Prop

A function can be evaluated at a point exactly when their domains meet.

Equations

• xi.EvaluableAt q = (q.base ≤ xi.base)

theorem EGZ.ConvexFlag.LinearFunction.evaluableAt_iff_domains_inter {F : ConvexFlag} (xi : F.LinearFunction) (q : F.Point) : xi.EvaluableAt q ↔ (xi.domain ∩ q.domain).Nonempty

def EGZ.ConvexFlag.LinearFunction.eval {F : ConvexFlag} (xi : F.LinearFunction) (q : F.Point) (h : xi.EvaluableAt q) : ℝ

Evaluation, using the function's base.

Equations

• xi.eval q h = xi.toAffine (q.coord h)

structure EGZ.ConvexFlag.ConvexCombination {F : ConvexFlag} {I : Type u_1} [Fintype I] (points : I → F.Point) (weight : I → ℝ) (result : F.Point) : Prop

Data witnessing one finite convex combination of flag points. Only strictly positive coefficients constrain the result's base; this is crucial in Proposition 7.1 and avoids zero coefficients shrinking the domain.

• nonnegative (i : I) : 0 ≤ weight i
• sum_eq_one : ∑ i : I, weight i = 1
• base_isLUB : IsLeast {x : F.Node | ∀ (i : I), 0 < weight i → (points i).base ≤ x} result.base
• val_eq : result.val = ∑ i : { i : I // 0 < weight i }, weight ↑i • (points ↑i).coord ⋯

theorem EGZ.ConvexFlag.ConvexCombination.sum_active {F : ConvexFlag} {I : Type u_1} [Fintype I] {points : I → F.Point} {weight : I → ℝ} {result : F.Point} (c : ConvexCombination points weight result) : ∑ i : { i : I // 0 < weight i }, weight ↑i = 1

The weights on the strictly positive support still sum to one.

theorem EGZ.ConvexFlag.ConvexCombination.coord_eq {F : ConvexFlag} {I : Type u_1} [Fintype I] {points : I → F.Point} {weight : I → ℝ} {result : F.Point} (c : ConvexCombination points weight result) {y : F.Node} (hy : result.base ≤ y) : result.coord hy = ∑ i : { i : I // 0 < weight i }, weight ↑i • (points ↑i).coord ⋯

Equation convc at an arbitrary upper node. This is the API form used as equation comb2 in Proposition 7.1.

theorem EGZ.ConvexFlag.exists_convexCombination {F : ConvexFlag} {I : Type u_1} [Fintype I] (points : I → F.Point) (weight : I → ℝ) (hnonneg : ∀ (i : I), 0 ≤ weight i) (hsum : ∑ i : I, weight i = 1) : ∃ (result : F.Point), ConvexCombination points weight result

Convex combinations exist. This theorem is the implementation-level counterpart of equation convc: the base is the supremum of the positive support and convexity of the target fibre supplies membership.

def EGZ.ConvexFlag.convexHull (F : ConvexFlag) (S : Set F.Point) : Set F.Point

The flag-convex hull from Definition 3.5.

Equations

• F.convexHull S = {result : F.Point | ∃ (n : ℕ) (points : Fin n → F.Point) (weight : Fin n → ℝ), (∀ (i : Fin n), points i ∈ S) ∧ EGZ.ConvexFlag.ConvexCombination points weight result}

structure EGZ.ConvexFlag.ProperPointSet (F : ConvexFlag) : Type u_1

A designated set of proper points: it is closed under flag convex combinations.

• carrier : Set F.Point

  Underlying set of flag points, closed under the flag convex hull.

• convex_closed : F.convexHull self.carrier ⊆ self.carrier

@[instance_reducible]

instance EGZ.ConvexFlag.ProperPointSet.instMembershipPoint {F : ConvexFlag} : Membership F.Point F.ProperPointSet

Equations

• EGZ.ConvexFlag.ProperPointSet.instMembershipPoint = { mem := fun (Ω : F.ProperPointSet) (q : F.Point) => q ∈ Ω.carrier }