Commit 2024-04-22 10:39 24e020ad

refactor(GroupTheory/Coxeter/Basic): Coxeter groups (#11836)

• Remove the definition def Matrix.IsCoxeter : Prop. Replace it with a type CoxeterMatrix B, which is the type of all Coxeter matrices indexed by B.
• Simplify the definitions of Coxeter matrices Aₙ (n : ℕ), Bₙ (n : ℕ), Dₙ (n : ℕ), I₂ₘ (m : ℕ), E₆, E₇, E₈, F₄, G₂, H₃, and H₄.
• All definitions involving a matrix (including the definition of a Coxeter group, Coxeter relation, and Coxeter system) now require the matrix to be a Coxeter matrix.
• Update docstrings of GroupTheory.Coxeter.Basic and GroupTheory.Coxeter.Matrix.
  • The terms "Coxeter matrix", "Coxeter group", and "Coxeter system" are now defined in the header docstring.
  • It is now clearer that the rank of a Coxeter system can be infinite.
  • There is now a note in the implementation details of GroupTheory.Coxeter.Matrix about what happens when an entry of the Coxeter matrix is zero.
  • There is now a note in the implementation details of GroupTheory.Coxeter.Basic about how we try to state our results in terms of the type B that indexes the simple reflections, rather than the set $S$ of simple reflections.
• Rename these definitions, structures, and theorems. Previously, there were six namespaces to keep track of: Matrix, Matrix.IsCoxeter, CoxeterMatrix, CoxeterGroup, CoxeterGroup.Relations, and CoxeterSystem. It was difficult to guess the fully qualified name of many theorems, and the names were not designed for use with field notation. Instead, we put everything into two namespaces: CoxeterMatrix and CoxeterSystem.
  • Rename CoxeterGroup.Relations.ofMatrix to CoxeterMatrix.relation. Also, change its type to B → B → FreeGroup B (from B × B → FreeGroup B).
  • Rename CoxeterGroup.Relations.toSet to CoxeterMatrix.relationsSet.
  • Rename Matrix.CoxeterGroup to CoxeterMatrix.group.
  • Rename CoxeterGroup.of to CoxeterMatrix.simple.
  • Remove CoxeterSystem.funLike. Rename CoxeterSystem.funLike.coe to CoxeterSystem.simple, because "simple reflection" (or "simple" for short) is the name used in the literature for this concept, and it is unintuitive to think of a Coxeter system as a function.
  • Rename CoxeterSystem.funLike.coe_injective' and CoxeterSystem.ext', which are exactly the same theorem, to CoxeterSystem.simple_determines_coxeterSystem. (This theorem is forthcoming in #11406.)
  • Rename CoxeterSystem.ofCoxeterGroup to CoxeterMatrix.toCoxeterSystem. CoxeterSystem.ofCoxeterGroup is a confusing name because the input to the definition is an CoxeterMatrix, not a Coxeter group.
  • Rename CoxeterSystem.ofCoxeterGroup_apply to CoxeterMatrix.toCoxeterSystem_simple and remove @[simp]. The theorem doesn't have a Coxeter system as input and it does have a CoxeterMatrix as input, so it makes more sense for it to be in the CoxeterMatrix namespace.
  • Rename CoxeterSystem.map_relations_eq_reindex_relations to CoxeterMatrix.reindex_relationsSet and switch the two sides of the equality. The theorem doesn't mention Coxeter systems anywhere, so it shouldn't be in the CoxeterSystem namespace. Also, the new name better indicates what is on the left-hand side of the equality.
  • Rename CoxeterSystem.equivCoxeterGroup to CoxeterMatrix.reindexGroupEquiv and switch the two sides of the equivalence. The definition doesn't mention Coxeter systems anywhere, so it shouldn't be in the CoxeterSystem namespace. Also, the new name conveys that the definition is about the Coxeter group associated to a reindexed matrix, rather than merely conveying that it is about an isomorphism of Coxeter groups.
  • Rename CoxeterSystem.equivCoxeterGroup_apply_of to CoxeterMatrix.reindexGroupEquiv_apply_simple.
  • Rename CoxeterSystem.equivCoxeterGroup_symm_apply_of CoxeterMatrix.reindexGroupEquiv_symm_apply_simple.
  • Rename CoxeterSystem.reindex_apply to CoxeterSystem.reindex_simple.
  • Rename CoxeterSystem.map_apply to CoxeterSystem.map_simple.
• Simplify several of the proofs.