OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections
OpenThe theorem, which is admitted in the source with a placeholder proof, states the following for a Coxeter matrix M on a finite, linearly ordered index set S, with Artin(M) the Artin group presented on generators S by the braid relations: the word of alternating generators s,t,s,... of length M(s,t) equals the alternating word beginning with t, for each pair s,t. For any two subsets X and Y of S and any two elements g and h of Artin(M), there exist a subset Z of S and an element k of Artin(M) such that the intersection of the two conjugate subgroups g P_X g⁻¹ and h P_Y h⁻¹ equals k P_Z k⁻¹. Here P_T is the standard parabolic subgroup generated by the images of the generators in T, and conjugation by g is the subgroup whose members x satisfy g⁻¹xg in P. There is no spherical-type or other restriction on M, so the intersection of two conjugates of standard parabolic subgroups is itself a conjugate of a standard parabolic subgroup.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/ArtinParabolicIntersections.lean; bytes 3753..4081
-- 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)
/-- The intersection of two conjugates of standard parabolics is parabolic. -/
theorem unconditional_parabolic_intersections
(X Y : Set S) (g h : Artin M) :
∃ (Z : Set S) (k : Artin M),
conjugate g (artinParabolic M X) ⊓ conjugate h (artinParabolic M Y) =
conjugate k (artinParabolic M Z) := by
sorry
end HarmonicArtin.ParabolicIntersections
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.