IsLiftable — Mathlib

English

The property IsLiftable defines when a map f: B → G respects the Coxeter relations M, i.e., (f(i) f(j))^{M(i,j)} = 1 for all i,j.

Русский

Свойство IsLiftable задаёт, когда отображение f: B → G соблюдает отношения Коксетера, т.е. (f(i) f(j))^{M(i,j)} = 1 для всех i,j.

LaTeX

$$$\mathrm{IsLiftable}(M,f) :\equiv \forall i,i', (f(i) f(i'))^{M(i,i')} = 1$$$

Lean4

/-- The proposition that the values of the function `f : B → G` satisfy the Coxeter relations
corresponding to the matrix `M`. -/
def _root_.CoxeterMatrix.IsLiftable {G : Type*} [Monoid G] (M : CoxeterMatrix B) (f : B → G) : Prop :=
  ∀ i i', (f i * f i') ^ M i i' = 1

Похожие утверждения