toIsometry_whiskerLeft — Mathlib

English

Let L, M, N be quadratic modules over a commutative ring R with 2 invertible. For any morphism f: M → N, the isometry associated to the left whiskering (L ⫽ f) is the tensor product of the identity on L with the isometry of f: (L ⫽ f).toIsometry = id_L ⊗ f.toIsometry.

Русский

Пусть L, M, N — квадратичные модули над кольцом R с инвертируемым 2. Для любого морфизма f: M → N изометрия, соответствующая левому завитку (L ◁ f), равна тензорному произведению единицы на L с изометрией f: (L ◁ f).toIsometry = id_L ⊗ f.toIsometry.

LaTeX

$$$ (L \triangleleft f).toIsometry = \mathrm{tmul}(\mathrm{id}_L, f.toIsometry) $$$

Lean4

theorem toIsometry_whiskerLeft (L : QuadraticModuleCat.{u} R) {M N : QuadraticModuleCat.{u} R} (f : M ⟶ N) :
    (L ◁ f).toIsometry = .tmul (.id _) f.toIsometry :=
  rfl

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