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