English
From a QuadraticForm.IsometryEquiv between Q1 and Q2 one obtains an isomorphism in the category QuadraticModuleCat between the corresponding objects, via the construction of ofIso.
Русский
Из квадратичной формы между Q1 и Q2 существует изоморфизм в категории QuadraticModuleCat между соответствующими объектами, получаемый посредством построения ofIso.
LaTeX
$$$\\exists \\; \\text{iso} : \\mathrm{QuadraticModuleCat}.\\mathrm{of}\\ Q_1 \\;\\cong\\; \\mathrm{QuadraticModuleCat}.\\mathrm{of}\\ Q_2$ от соответствующего изометрического эквивалента $Q_1.IsometryEquiv Q_2$$$
Lean4
/-- Build an isomorphism in the category `QuadraticModuleCat R` from a
`QuadraticForm.IsometryEquiv`. -/
@[simps]
def ofIso (e : Q₁.IsometryEquiv Q₂) : QuadraticModuleCat.of Q₁ ≅ QuadraticModuleCat.of Q₂
where
hom := ofHom e.toIsometry
inv := ofHom e.symm.toIsometry
hom_inv_id := Hom.ext <| DFunLike.ext _ _ e.left_inv
inv_hom_id := Hom.ext <| DFunLike.ext _ _ e.right_inv
