HarmonicArtin
DefinitionFor a type S of generators and a Coxeter matrix M on S, alternating(s,t,n) is the word in the free group on S of length n that alternates s,t,s,... starting with s. The braid relators are the elements alternating(s,t,m) times the inverse of alternating(t,s,m), where m = M(s,t), over all pairs (s,t). Artin(M) is the group presented by the free group on S modulo these relators, the Artin group of M, with generator(s) the image of s. For a subset T of S, coxeterParabolic(M,T) is the subgroup of the Coxeter group generated by the simple reflections indexed by T, and T is spherical when this parabolic subgroup is finite. SphericalType(M) is the type of spherical subsets, and a lifted cell is a pair consisting of an Artin group element and a spherical subset. For a list w of generators, wordArtin and wordCoxeter give its product in the Artin group and in the Coxeter group. LiftedFace(a,b) holds when the spherical set of a is contained in that of b and there is a word w using only generators from b's set, reduced in the Coxeter system (its length equals the length of w), of minimal length in its coset with respect to right multiplication by the parabolic subgroup of a's set, such that the Artin element of a equals that of b times wordArtin(w). LiftedCell is made a preorder by taking the reflexive-transitive closure of LiftedFace. SalvettiCover(M) is the topological space obtained as the geometric realization of the nerve of this preorder, viewed as a category.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/HarmonicArtin.lean; bytes 16..1778
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
namespace OAI
namespace HarmonicArtin
universe u
variable {S : Type u}
def alternating (s t : S) : ℕ → FreeGroup S
| 0 => 1
| n + 1 => FreeGroup.of s * alternating t s n
def braidRelators (M : CoxeterMatrix S) : Set (FreeGroup S) :=
Set.range fun st : S × S =>
alternating st.1 st.2 (M st.1 st.2) *
(alternating st.2 st.1 (M st.1 st.2))⁻¹
abbrev Artin (M : CoxeterMatrix S) := PresentedGroup (braidRelators M)
def generator (M : CoxeterMatrix S) (s : S) : Artin M := PresentedGroup.of s
def coxeterParabolic (M : CoxeterMatrix S) (T : Set S) : Subgroup M.Group :=
Subgroup.closure (M.simple '' T)
def IsSpherical (M : CoxeterMatrix S) (T : Set S) : Prop :=
Finite (coxeterParabolic M T)
abbrev SphericalType (M : CoxeterMatrix S) := {T : Set S // IsSpherical M T}
abbrev LiftedCell (M : CoxeterMatrix S) := Artin M × SphericalType M
def wordArtin (M : CoxeterMatrix S) (w : List S) : Artin M :=
(w.map (generator M)).prod
def wordCoxeter (M : CoxeterMatrix S) (w : List S) : M.Group :=
(w.map M.simple).prod
def LiftedFace (M : CoxeterMatrix S) (a b : LiftedCell M) : Prop :=
a.2.1 ⊆ b.2.1 ∧ ∃ w : List S,
(∀ s ∈ w, s ∈ b.2.1) ∧
M.toCoxeterSystem.length (wordCoxeter M w) = w.length ∧
(∀ v : coxeterParabolic M a.2.1,
M.toCoxeterSystem.length (wordCoxeter M w) ≤
M.toCoxeterSystem.length (wordCoxeter M w * v)) ∧
a.1 = b.1 * wordArtin M w
instance (M : CoxeterMatrix S) : Preorder (LiftedCell M) where
le := Relation.ReflTransGen (LiftedFace M)
le_refl _ := Relation.ReflTransGen.refl
le_trans _ _ _ := Relation.ReflTransGen.trans
noncomputable def SalvettiCover (M : CoxeterMatrix S) : TopCat :=
SSet.toTop.obj (CategoryTheory.nerve (LiftedCell M))
end HarmonicArtin
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.