toIsometry_whiskerRight — Mathlib

English

Let L, M be quadratic modules over R and N an R-quadratic module. For a morphism f: L → M, the isometry of the right whiskering (f ▷ N) is the tensor product of f’s isometry with the identity on N: (f ▷ N).toIsometry = f.toIsometry ⊗ id_N.

Русский

Пусть L, M — квадратичные модули над R, N — квадратичный модуль. Морфизм f: L → M. Изометрия правого завитка (f ▷ N) равна тензорному произведению изометрии f на тождественную на N: (f ▷ N).toIsometry = f.toIsometry ⊗ id_N.

LaTeX

$$$ (f \triangleright N).toIsometry = \mathrm{tmul}(f.toIsometry, \mathrm{id} _ ) $$$

Lean4

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

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