OAI.HarmonicArtin.ParabolicIntersections.unconditional_arbitrary_intersections
OpenThe theorem states that, for a finite linearly ordered generating set S and a Coxeter matrix M on S, with Artin(M) the Artin group defined as the free group on S modulo the braid relations (alternating words of length M(s,t) in s,t being equal in either order), the following hold for every set F of subgroups of Artin(M) all of whose members are parabolic, meaning each is a conjugate g P g⁻¹ of a standard subgroup generated by the images of some subset X of S, with no spherical-type restriction. First, there is a finite subfamily F₀ contained in F with at most |S| members (the cardinality of S) such that the intersection of all of F equals the intersection of the members of F₀. Second, the intersection of all of F is itself a parabolic subgroup.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/ArtinParabolicIntersections.lean; bytes 4083..4520
-- 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)
/-- An arbitrary parabolic intersection is obtained from at most the rank many members. -/
theorem unconditional_arbitrary_intersections
(F : Set (Subgroup (Artin M))) (hF : ∀ P ∈ F, IsParabolic M P) :
(∃ F₀ : Finset (Subgroup (Artin M)),
(↑F₀ : Set (Subgroup (Artin M))) ⊆ F ∧ F₀.card ≤ Nat.card S ∧
sInf F = sInf (↑F₀ : Set (Subgroup (Artin M)))) ∧ IsParabolic M (sInf F) := by
sorry
end HarmonicArtin.ParabolicIntersections
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.