English
For any monoid G, there is a correspondence between lifts f: B → G satisfying Coxeter relations and monoid homomorphisms W →* G.
Русский
Для любого моноида G существует соответствие между подъемами f: B → G, удовлетворяющими отношениям Коксетера, и моноид-гомоморфизма W →* G.
LaTeX
$$Equiv { f : B → G // IsLiftable M f } (W →* G)$$
Lean4
/-- The universal mapping property of Coxeter systems. For any monoid `G`,
functions `f : B → G` whose values satisfy the Coxeter relations are equivalent to
monoid homomorphisms `f' : W → G`. -/
def lift {G : Type*} [Monoid G] : { f : B → G // IsLiftable M f } ≃ (W →* G)
where
toFun
f :=
MonoidHom.comp (Units.coeHom G)
(cs.groupLift
(show ∀ i i', ((restrictUnit f.property) i * (restrictUnit f.property) i') ^ M i i' = 1 from fun i i' ↦
Units.ext (f.property i i')))
invFun
ι :=
⟨ι ∘ cs.simple, fun i i' ↦ by rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]⟩
left_inv
f := by
ext i
simp only [MonoidHom.comp_apply, comp_apply, groupLift, simple]
rw [← MonoidHom.toFun_eq_coe, toMonoidHom_apply_symm_apply, PresentedGroup.toGroup.of, OneHom.toFun_eq_coe,
MonoidHom.toOneHom_coe, Units.coeHom_apply, restrictUnit]
right_inv
ι := by
apply cs.ext_simple
intro i
dsimp only
rw [groupLift, simple, MonoidHom.comp_apply, MonoidHom.comp_apply, toMonoidHom_apply_symm_apply,
PresentedGroup.toGroup.of, CoxeterSystem.restrictUnit, Units.coeHom_apply]
simp only [comp_apply, simple]
