toIsometry — Mathlib

English

The morphism from QuadraticModuleCat toIsometry associates to a morphism its underlying isometry.

Русский

Морфизм из QuadraticModuleCat в Isometry сопоставляет морфизму его базовую изометрию.

LaTeX

$$$ \text{Hom.toIsometry} : \text{QuadraticModuleCat.Hom} \to \text{QuadraticMap.Isometry}$$$

Lean4

/-- Turn a morphism in `QuadraticModuleCat` back into a `Isometry`. -/
abbrev toIsometry {X Y : QuadraticModuleCat R} (f : Hom X Y) :=
  ConcreteCategory.hom (C := QuadraticModuleCat R) f

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