toIsometryEquiv — Mathlib

English

From an isomorphism i in QuadraticModuleCat between X and Y, one obtains a corresponding isometry equivalence between their forms X.form and Y.form.

Русский

Изоморфизм i между модулями X и Y порождает изометрическое эквивалентное отображение между формами X.form и Y.form.

LaTeX

$$$\\text{toIsometryEquiv}(i) : X.\\mathrm{form} \\IsometryEquiv Y.\\mathrm{form}$$$

Lean4

/-- Build a `QuadraticForm.IsometryEquiv` from an isomorphism in the category
`QuadraticModuleCat R`. -/
@[simps]
def toIsometryEquiv (i : X ≅ Y) : X.form.IsometryEquiv Y.form
    where
  toFun := i.hom.toIsometry
  invFun := i.inv.toIsometry
  left_inv
    x := by
    change (i.hom ≫ i.inv).toIsometry x = x
    simp
  right_inv
    x := by
    change (i.inv ≫ i.hom).toIsometry x = x
    simp
  map_add' := map_add _
  map_smul' := map_smul _
  map_app' := QuadraticMap.Isometry.map_app _

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