Preservation of realized faces

A subdivision map sends the nodes of a smaller decomposition to the old nodes, preserves their finite joins, and commutes with the affine transition maps. Its fibres map into the old polytopes and its proper points remain proper. Under these concrete conditions every old realized face restricts to a realized face whenever its pullback is nonempty. The key order inequality compares the new face index with the old one.

def EGZ.ConvexFlag.Point.map {F : ConvexFlag} {G : ConvexFlag} (q : F.Point) (node : SupHom F.Node G.Node) (fibre : (x : F.Node) → RealCoord (F.rank x) →ᵃ[ℝ] RealCoord (G.rank (node x))) (hpolytope : ∀ (x : F.Node), Set.MapsTo (⇑(fibre x)) (F.polytope x).carrier (G.polytope (node x)).carrier) : G.Point

Map a flag point using a map on nodes and compatible affine fibre maps.

Equations

• q.map node fibre hpolytope = { base := node q.base, val := (fibre q.base) q.val, val_mem := ⋯ }

theorem EGZ.ConvexFlag.ConvexCombination.map_on_polytope {F : ConvexFlag} {G : ConvexFlag} (node : SupHom F.Node G.Node) (fibre : (x : F.Node) → RealCoord (F.rank x) →ᵃ[ℝ] RealCoord (G.rank (node x))) (hpolytope : ∀ (x : F.Node), Set.MapsTo (⇑(fibre x)) (F.polytope x).carrier (G.polytope (node x)).carrier) (hcomm : ∀ {x y : F.Node} (h : x ≤ y), ∀ q ∈ (F.polytope x).carrier, (fibre y) ((F.transition h).real q) = (G.transition ⋯).real ((fibre x) q)) {I : Type u_1} [Fintype I] {points : I → F.Point} {weight : I → ℝ} {result : F.Point} (c : ConvexCombination points weight result) : ConvexCombination (fun (i : I) => (points i).map node fibre hpolytope) weight (result.map node fibre hpolytope)

Affine maps commuting with transitions preserve flag convex combinations when the node map preserves joins. The least-upper-bound condition is proved from the finite join of the strictly positive support.

theorem EGZ.ConvexFlag.ConvexCombination.map {F : ConvexFlag} {G : ConvexFlag} (node : SupHom F.Node G.Node) (fibre : (x : F.Node) → RealCoord (F.rank x) →ᵃ[ℝ] RealCoord (G.rank (node x))) (hpolytope : ∀ (x : F.Node), Set.MapsTo (⇑(fibre x)) (F.polytope x).carrier (G.polytope (node x)).carrier) (hcomm : ∀ {x y : F.Node} (h : x ≤ y) (q : RealCoord (F.rank x)), (fibre y) ((F.transition h).real q) = (G.transition ⋯).real ((fibre x) q)) {I : Type u_1} [Fintype I] {points : I → F.Point} {weight : I → ℝ} {result : F.Point} (c : ConvexCombination points weight result) : ConvexCombination (fun (i : I) => (points i).map node fibre hpolytope) weight (result.map node fibre hpolytope)

Global commutation is a sufficient special case of commutation on the source polytopes.

def EGZ.RationalPolytope.Face.preimage {m n : ℕ} {P : RationalPolytope m} {Q : RationalPolytope n} (Γ : P.Face) (A : RealCoord n →ᵃ[ℝ] RealCoord m) (hA : Set.MapsTo (⇑A) Q.carrier P.carrier) (hne : (Q.carrier ∩ ⇑A ⁻¹' Γ.carrier).Nonempty) : Q.Face

Pull back an exposed face along an affine map taking one polytope into another. The pullback includes the source polytope constraint.

Equations

• Γ.preimage A hA hne = { carrier := Q.carrier ∩ ⇑A ⁻¹' Γ.carrier, is_exposed := ⋯, nonempty := hne }

@[simp]

theorem EGZ.RationalPolytope.Face.preimage_carrier {m n : ℕ} {P : RationalPolytope m} {Q : RationalPolytope n} (Γ : P.Face) (A : RealCoord n →ᵃ[ℝ] RealCoord m) (hA : Set.MapsTo (⇑A) Q.carrier P.carrier) (hne : (Q.carrier ∩ ⇑A ⁻¹' Γ.carrier).Nonempty) : (Γ.preimage A hA hne).carrier = Q.carrier ∩ ⇑A ⁻¹' Γ.carrier

structure EGZ.FlagDecomposition.SubdivisionMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ Ψ : FlagDecomposition p d f) : Type

Affine data comparing a smaller decomposition Ψ with Φ. Preserving joins, transitions, and proper points suffices to preserve realized faces; neither injectivity nor equal coordinate ranks are required.

• node : SupHom Ψ.flag.Node Φ.flag.Node

  Supremum-preserving map from refined nodes to original nodes.

• fibre (x : Ψ.flag.Node) : RealCoord (Ψ.flag.rank x) →ᵃ[ℝ] RealCoord (Φ.flag.rank (self.node x))

  Affine map from each refined polytope to its original-node coordinates.

• polytope_mem (x : Ψ.flag.Node) : Set.MapsTo (⇑(self.fibre x)) (Ψ.flag.polytope x).carrier (Φ.flag.polytope (self.node x)).carrier
• transition_comm {x y : Ψ.flag.Node} (h : x ≤ y) (q : RealCoord (Ψ.flag.rank x)) : (self.fibre y) ((Ψ.flag.transition h).real q) = (Φ.flag.transition ⋯).real ((self.fibre x) q)
• proper (q : Ψ.flag.Point) : q ∈ Ψ.omega → { base := self.node q.base, val := (self.fibre q.base) q.val, val_mem := ⋯ } ∈ Φ.omega

def EGZ.FlagDecomposition.SubdivisionMap.ofLocalGenerators {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (node : SupHom Ψ.flag.Node Φ.flag.Node) (fibre : (x : Ψ.flag.Node) → RealCoord (Ψ.flag.rank x) →ᵃ[ℝ] RealCoord (Φ.flag.rank (node x))) (polytope_mem : ∀ (x : Ψ.flag.Node), Set.MapsTo (⇑(fibre x)) (Ψ.flag.polytope x).carrier (Φ.flag.polytope (node x)).carrier) (transition_comm : ∀ {x y : Ψ.flag.Node} (h : x ≤ y) (q : RealCoord (Ψ.flag.rank x)), (fibre y) ((Ψ.flag.transition h).real q) = (Φ.flag.transition ⋯).real ((fibre x) q)) (hgenerators : ∀ q ∈ Ψ.omegaZero, q.map node fibre polytope_mem ∈ Φ.omegaZero) : Φ.SubdivisionMap Ψ

To construct a subdivision map it suffices to send local generators to old local generators. Convex-combination preservation then gives inclusion of the entire proper-point sets.

Equations

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

def EGZ.FlagDecomposition.SubdivisionMap.point {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) (q : Ψ.flag.Point) : Φ.flag.Point

The induced map on flag points.

Equations

• M.point q = { base := M.node q.base, val := (M.fibre q.base) q.val, val_mem := ⋯ }

@[simp]

theorem EGZ.FlagDecomposition.SubdivisionMap.point_base {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) (q : Ψ.flag.Point) : (M.point q).base = M.node q.base

theorem EGZ.FlagDecomposition.SubdivisionMap.point_coord {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) (q : Ψ.flag.Point) {x : Ψ.flag.Node} (h : q.base ≤ x) : (M.point q).coord ⋯ = (M.fibre x) (q.coord h)

theorem EGZ.FlagDecomposition.SubdivisionMap.point_proper {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) {q : Ψ.flag.Point} (hq : q ∈ Ψ.omega) : M.point q ∈ Φ.omega

def EGZ.FlagDecomposition.SubdivisionMap.comp {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) {Θ : FlagDecomposition p d f} (N : Ψ.SubdivisionMap Θ) : Φ.SubdivisionMap Θ

Compose successive subdivisions, including their proper-point maps.

Equations

• M.comp N = { node := M.node.comp N.node, fibre := fun (x : Θ.flag.Node) => (M.fibre (N.node x)).comp (N.fibre x), polytope_mem := ⋯, transition_comm := ⋯, proper := ⋯ }

@[simp]

theorem EGZ.FlagDecomposition.SubdivisionMap.comp_point {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) {Θ : FlagDecomposition p d f} (N : Ψ.SubdivisionMap Θ) (q : Θ.flag.Point) : (M.comp N).point q = M.point (N.point q)

def EGZ.FlagDecomposition.SubdivisionMap.face {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) (x : Ψ.flag.Node) (Γ : (Φ.flag.polytope (M.node x)).Face) (hne : ((Ψ.flag.polytope x).carrier ∩ ⇑(M.fibre x) ⁻¹' Γ.carrier).Nonempty) : (Ψ.flag.polytope x).Face

The part of an old face lying in the new fibre.

Equations

• M.face x Γ hne = Γ.preimage (M.fibre x) ⋯ hne

@[simp]

theorem EGZ.FlagDecomposition.SubdivisionMap.face_carrier {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) (x : Ψ.flag.Node) (Γ : (Φ.flag.polytope (M.node x)).Face) (hne : ((Ψ.flag.polytope x).carrier ∩ ⇑(M.fibre x) ⁻¹' Γ.carrier).Nonempty) : (M.face x Γ hne).carrier = (Ψ.flag.polytope x).carrier ∩ ⇑(M.fibre x) ⁻¹' Γ.carrier

theorem EGZ.FlagDecomposition.SubdivisionMap.point_mem_pointsOnFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) {x : Ψ.flag.Node} {Γ : (Φ.flag.polytope (M.node x)).Face} {hne : ((Ψ.flag.polytope x).carrier ∩ ⇑(M.fibre x) ⁻¹' Γ.carrier).Nonempty} {q : Ψ.flag.Point} (hq : q ∈ Ψ.pointsOnFace x (M.face x Γ hne)) : M.point q ∈ Φ.pointsOnFace (M.node x) Γ

theorem EGZ.FlagDecomposition.SubdivisionMap.faceIndex_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) (x : Ψ.flag.Node) (Γ : (Φ.flag.polytope (M.node x)).Face) (hne : ((Ψ.flag.polytope x).carrier ∩ ⇑(M.fibre x) ⁻¹' Γ.carrier).Nonempty) : M.node (Ψ.faceIndex x (M.face x Γ hne)) ≤ Φ.faceIndex (M.node x) Γ

Every new proper-point base over the restricted face lies below the old face index. Join preservation gives the same inequality for their supremum.

theorem EGZ.FlagDecomposition.SubdivisionMap.isRealizedFace {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) (x : Ψ.flag.Node) (Γ : (Φ.flag.polytope (M.node x)).Face) (hne : ((Ψ.flag.polytope x).carrier ∩ ⇑(M.fibre x) ⁻¹' Γ.carrier).Nonempty) (hΓ : Φ.IsRealizedFace (M.node x) Γ) : Ψ.IsRealizedFace x (M.face x Γ hne)

Realization survives restriction of the polytopes and proper-point set. The new face index may move downwards; its old image still maps into the old face index, whose whole polytope maps into the realized face.

noncomputable def EGZ.FlagDecomposition.reducedSubdivisionMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) : Φ.SubdivisionMap (Φ.reduced hp)

The inclusion of reduced nodes is a subdivision map. Its fibre maps are identities and every original proper point survives the restriction.

Equations

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