Selecting local atoms over a face

The face refinement splits every local summand below its anchor using the same predicate on ambient points. Compatibility of centered lifts identifies the selected cumulative support with the inverse image of the target face.

def EGZ.FlagDecomposition.faceSelector {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) (v : FpCoord p d) : Prop

Ambient atoms whose centered coordinate at the anchor lies on its face.

Equations

• Φ.faceSelector x Γ v = (((Φ.representation.map x) v).centeredLift.real ∈ Γ.carrier)

theorem EGZ.FlagDecomposition.transition_centeredLift {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) {y x : Φ.flag.Node} (h : y ≤ x) (v : FpCoord p d) (hv : Φ.cumulativeWeight y v ≠ 0) : (Φ.flag.transition h).integer ((Φ.representation.map y) v).centeredLift = ((Φ.representation.map x) v).centeredLift

On supported atoms, taking centered representatives commutes with every transition of the old decomposition.

theorem EGZ.FlagDecomposition.faceSelector_iff {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) {y x : Φ.flag.Node} (h : y ≤ x) (Γ : (Φ.flag.polytope x).Face) (q : IntCoord (Φ.flag.rank y)) (hc : IsCenteredLift p q) (v : FpCoord p d) (hmap : (Φ.representation.map y) v = IntCoord.mod p q) (hv : Φ.cumulativeWeight y v ≠ 0) : Φ.faceSelector x Γ v ↔ (Φ.flag.transition h).real q.real ∈ Γ.carrier

theorem EGZ.FlagDecomposition.centeredFibreMass_faceSelector {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) {y x : Φ.flag.Node} (h : y ≤ x) (Γ : (Φ.flag.polytope x).Face) (q : IntCoord (Φ.flag.rank y)) : FlagDecompositionRaw.centeredFibreMass (fun (v : FpCoord p d) => if Φ.faceSelector x Γ v then Φ.cumulativeWeight y v else 0) (⇑(Φ.representation.map y)) q = if (Φ.flag.transition h).real q.real ∈ Γ.carrier then Φ.hat y q else 0

Selecting a face does not split any nonzero cumulative fibre below the anchor: the entire fibre is retained or the entire fibre is removed.

theorem EGZ.FlagDecomposition.centeredFibreMass_faceSelector_self {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (Γ : (Φ.flag.polytope x).Face) (q : IntCoord (Φ.flag.rank x)) : FlagDecompositionRaw.centeredFibreMass (fun (v : FpCoord p d) => if Φ.faceSelector x Γ v then Φ.cumulativeWeight x v else 0) (⇑(Φ.representation.map x)) q = if q.real ∈ Γ.carrier then Φ.hat x q else 0

The selected support at the anchor is precisely its old support on the chosen face.