The canonical filtration subgroups are convex (Proposition 8)
DisprovedPCB.convex_towerThe canonical filtration subgroups are convex for the lexicographic bi-ordering. An element outside a filtration subgroup has a nontrivial normal-form component above the given index, so it lies either above every element of the subgroup or below every element of the subgroup, and no element outside the subgroup can lie strictly between two of its elements. This is Proposition 8 of the paper.
import Mathlib import Definitions.Def_PCB_alg import Definitions.Def_PCB_tor
namespace PCB
/-! Milestone 6 (Proposition 8): the canonical subgroups of the
filtration are convex with respect to the lexicographic bi-ordering. An
element outside the subgroup G_j has a nontrivial component above j, so
it lies either above every element of G_j or below every element of G_j
in the order, and no element outside G_j can lie strictly between two of
its elements. -/
theorem convex_tower {k : ℕ} {G : Type*} [Group G] {F : Fin k → Type*} [∀ j, Group (F j)]
(W : AlmostDirectProductWorld k G F) :
∀ j : Fin k, ConvexSubgroup (lexCone W) (W.tower j) := by sorry
end PCB
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in an almost-direct product world, every subgroup of the canonical filtration is convex with respect to the lexicographic cone: every element lying strictly between two elements of the subgroup, in the ordering determined by the cone, belongs to the subgroup. Hypotheses: the world is given; no further hypotheses appear.