English
Let X and Y be quadratic module objects over a commutative ring R, and let f be a morphism from X to Y in the category of quadratic modules. The underlying module homomorphism obtained by forgetting the quadratic structure coincides with the linear map coming from f’s isometry component; equivalently, the forgetful functor to module objects sends f to ModuleCat.ofHom applied to the linear part of f.
Русский
Пусть X и Y — квадратичные модули над кольцом R, и пусть f: X → Y — морфизм в категории квадратичных модулей. Подмодульная карта, полученная при забывании квадратичной структуры, совпадает с линейным отображением, полученным из изометрной части f; эквивалентно, забывающий функтор отправляет f в модульную морфизм через соответствующую линейную карту.
LaTeX
$$$\\big(\\mathrm{forget}_2 (\\mathrm{QuadraticModuleCat}\\ R\\, ) (\\mathrm{ModuleCat}\\ R)\\big).\\mathrm{map} \\, f \;=\; \\mathrm{ModuleCat.ofHom}(f^{\\mathrm{toIsometry}}.toLinearMap)$$$
Lean4
@[simp]
theorem forget₂_map (X Y : QuadraticModuleCat R) (f : X ⟶ Y) :
(forget₂ (QuadraticModuleCat R) (ModuleCat R)).map f = ModuleCat.ofHom f.toIsometry.toLinearMap :=
rfl
