OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_closure
OpenThe theorem states that, for a Coxeter matrix M on a finite linearly ordered generating set S, with Artin(M) the Artin group presented by the braid relations determined by M (alternating words of length M(s,t) in s and t are equal), every subset E of Artin(M) lies in a unique smallest parabolic subgroup. Here a subgroup P is parabolic if it is a conjugate g·Artin_parabolic(T)·g⁻¹ of the standard subgroup generated by the images of the generators in some subset T of S, for some g in Artin(M), with no spherical-type restriction. Precisely, there exists exactly one subgroup P of Artin(M) that is parabolic, contains E, and is contained in every parabolic subgroup Q that contains E. The statement holds unconditionally, for arbitrary M and arbitrary E, and its proof is admitted in the source rather than established.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/ArtinParabolicIntersections.lean; bytes 4522..4810
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
import Definitions.Def_ArtinParabolicIntersections
namespace OAI
namespace HarmonicArtin.ParabolicIntersections
variable {S : Type} [Fintype S] [LinearOrder S] (M : CoxeterMatrix S)
/-- Every subset is contained in a unique smallest parabolic subgroup. -/
theorem unconditional_parabolic_closure (E : Set (Artin M)) :
∃! P : Subgroup (Artin M), IsParabolic M P ∧ E ⊆ P ∧
∀ Q : Subgroup (Artin M), IsParabolic M Q → E ⊆ Q → P ≤ Q := by
sorry
end HarmonicArtin.ParabolicIntersections
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.