Rebuilding a flag after deleting local mass

Nonzero cumulative supports are closed under transition. Keeping the active nodes and replacing their polytopes by these support hulls reconstructs a flag decomposition, including visibility of every face.

structure EGZ.FlagDecompositionRaw.RebuildData {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (f : FpCoord p d → ℕ) : Prop

The algebraic conditions needed to rebuild the support polytopes.

• odd : Odd p
• nonzero : ∃ (x : F.Node) (v : FpCoord p d), pieces x v ≠ 0
• local_supported (x : F.Node) (v : FpCoord p d) : pieces x v ≠ 0 → v ∈ R.space x
• retained_le (v : FpCoord p d) : retainedWeight pieces v ≤ f v
• transition_hat_nonzero {x y : F.Node} (h : x ≤ y) (z : IntCoord (F.rank x)) : hat R pieces x z ≠ 0 → hat R pieces y ((F.transition h).integer z) ≠ 0
• hat_exists_local (x : F.Node) (z : IntCoord (F.rank x)) : hat R pieces x z ≠ 0 → ∃ (y : F.Node) (h : y ≤ x) (w : IntCoord (F.rank y)), localLift R pieces y w ≠ 0 ∧ (F.transition h).integer w = z

def EGZ.FlagDecompositionRaw.RebuildData.Active {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (_D : RebuildData R pieces f) (x : F.Node) : Prop

A node is active when it has a nonzero local contribution below it.

Equations

• _D.Active x = ∃ y ≤ x, ∃ (v : EGZ.FpCoord p d), pieces y v ≠ 0

theorem EGZ.FlagDecompositionRaw.RebuildData.active_mono {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) {x y : F.Node} (h : x ≤ y) (hx : D.Active x) : D.Active y

theorem EGZ.FlagDecompositionRaw.RebuildData.active_top {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : D.Active ⊤

@[reducible, inline]

abbrev EGZ.FlagDecompositionRaw.RebuildData.ActiveNode {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : Type u_1

The subtype of nodes whose cumulative lifted support survives rebuilding.

Equations

• D.ActiveNode = { x : F.Node // D.Active x }

@[instance_reducible]

noncomputable instance EGZ.FlagDecompositionRaw.RebuildData.instFintypeActiveNode {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : Fintype D.ActiveNode

Equations

• D.instFintypeActiveNode = Subtype.fintype D.Active

@[instance_reducible]

instance EGZ.FlagDecompositionRaw.RebuildData.instSemilatticeSupActiveNode {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : SemilatticeSup D.ActiveNode

Equations

• D.instSemilatticeSupActiveNode = Subtype.semilatticeSup ⋯

@[instance_reducible]

instance EGZ.FlagDecompositionRaw.RebuildData.instOrderTopActiveNode {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : OrderTop D.ActiveNode

Equations

• D.instOrderTopActiveNode = { top := ⟨⊤, ⋯⟩, le_top := ⋯ }

theorem EGZ.FlagDecompositionRaw.RebuildData.pieces_eq_zero_of_not_active {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) {x : F.Node} (hx : ¬D.Active x) (v : FpCoord p d) : pieces x v = 0

theorem EGZ.FlagDecompositionRaw.RebuildData.cumulative_pos_of_active {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) {x : F.Node} (hx : D.Active x) : ∃ (v : FpCoord p d), cumulativeWeight pieces x v ≠ 0

theorem EGZ.FlagDecompositionRaw.RebuildData.hatSupport_nonempty {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) {x : F.Node} (hx : D.Active x) : (hatSupport R pieces x).Nonempty

theorem EGZ.FlagDecompositionRaw.RebuildData.active_of_localLift_ne_zero {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) {x : F.Node} {z : IntCoord (F.rank x)} (hz : localLift R pieces x z ≠ 0) : D.Active x

theorem EGZ.FlagDecompositionRaw.RebuildData.localLift_le_hat {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} (x : F.Node) (z : IntCoord (F.rank x)) : localLift R pieces x z ≤ hat R pieces x z

noncomputable def EGZ.FlagDecompositionRaw.RebuildData.polytope {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (x : D.ActiveNode) : RationalPolytope (F.rank ↑x)

The new polytope has exactly the surviving cumulative support as generators.

Equations

• D.polytope x = EGZ.RationalPolytope.ofFinsetConvexHull (Finset.image EGZ.IntCoord.real (EGZ.FlagDecompositionRaw.hatSupport R pieces ↑x)) ⋯ ⋯

@[simp]

theorem EGZ.FlagDecompositionRaw.RebuildData.polytope_carrier {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (x : D.ActiveNode) : (D.polytope x).carrier = (convexHull ℝ) (IntCoord.real '' ↑(hatSupport R pieces ↑x))

theorem EGZ.FlagDecompositionRaw.RebuildData.mem_polytope_of_localLift_ne_zero {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (x : D.ActiveNode) (z : IntCoord (F.rank ↑x)) (hz : localLift R pieces (↑x) z ≠ 0) : z.real ∈ (D.polytope x).carrier

theorem EGZ.FlagDecompositionRaw.RebuildData.transition_mem {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) {x y : D.ActiveNode} (h : x ≤ y) {q : RealCoord (F.rank ↑x)} (hq : q ∈ (D.polytope x).carrier) : (F.transition h).real q ∈ (D.polytope y).carrier

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecompositionRaw.RebuildData.flag {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : ConvexFlag

Retain active nodes and rebuild each support hull.

Equations

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

noncomputable def EGZ.FlagDecompositionRaw.RebuildData.representation {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : FpRepresentation p d D.flag

The finite-field representation restricted to the active nodes of the rebuilt flag.

Equations

• D.representation = { space := fun (x : D.flag.Node) => R.space ↑x, map := fun (x : D.flag.Node) => R.map ↑x, space_mono := ⋯, map_surjective := ⋯, compatible := ⋯, lattice_eq_standard := ⋯ }

theorem EGZ.FlagDecompositionRaw.RebuildData.sum_activeNode_eq {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (v : FpCoord p d) : ∑ x : D.ActiveNode, pieces (↑x) v = ∑ x : F.Node, pieces x v

theorem EGZ.FlagDecompositionRaw.RebuildData.cumulativeWeight_activeNode {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (x : D.ActiveNode) (v : FpCoord p d) : cumulativeWeight (fun (y : D.flag.Node) => pieces ↑y) x v = cumulativeWeight pieces (↑x) v

theorem EGZ.FlagDecompositionRaw.RebuildData.hat_activeNode {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (x : D.ActiveNode) (z : IntCoord (F.rank ↑x)) : hat D.representation (fun (y : D.flag.Node) => pieces ↑y) x z = hat R pieces (↑x) z

theorem EGZ.FlagDecompositionRaw.RebuildData.faces_visible {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (x : D.ActiveNode) (Γ : (D.polytope x).Face) : VisibleFace D.representation (fun (y : D.flag.Node) => pieces ↑y) x Γ

Every face of a rebuilt support hull contains a projection of a surviving local generator, so it remains visible to the proper-point set.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecompositionRaw.RebuildData.decomposition {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : FlagDecomposition p d f

Rebuild a decomposition with precisely the surviving mass at active nodes. The constructor proves all flag and visibility invariants.

Equations

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

@[simp]

theorem EGZ.FlagDecompositionRaw.RebuildData.decomposition_cumulativeWeight {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (x : D.ActiveNode) : D.decomposition.cumulativeWeight x = cumulativeWeight pieces ↑x

@[simp]

theorem EGZ.FlagDecompositionRaw.RebuildData.decomposition_hat {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) (x : D.ActiveNode) : D.decomposition.hat x = hat R pieces ↑x

@[simp]

theorem EGZ.FlagDecompositionRaw.RebuildData.decomposition_retainedWeight {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : D.decomposition.retainedWeight = retainedWeight pieces

theorem EGZ.FlagDecompositionRaw.RebuildData.card_decomposition_le {p d : ℕ} [NeZero p] {F : ConvexFlag} {R : FpRepresentation p d F} {pieces : F.Node → FpCoord p d → ℕ} {f : FpCoord p d → ℕ} (D : RebuildData R pieces f) : Fintype.card D.decomposition.flag.Node ≤ Fintype.card F.Node