OAI.HarmonicArtin.salvetti_cover_contractible
OpenThe theorem states that, for every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/HarmonicArtin.lean; bytes 1778..2033
-- 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_HarmonicArtin
namespace OAI
namespace HarmonicArtin
universe u
variable {S : Type u}
/-- The full lifted spherical-cell realization is contractible for every
Coxeter matrix with finitely many standard generators. -/
theorem salvetti_cover_contractible [Finite S] (M : CoxeterMatrix S) :
ContractibleSpace (SalvettiCover M) := by
sorry
end HarmonicArtin
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.