Isometric linear maps #
Main definitions #
Q₁ →qᵢ Q₂ is notation for
- toFun : M₁ → M₂
The quadratic form agrees across the map.
An isometry between two quadratic spaces
M₁, Q₁ and
M₂, Q₂ over a ring
is a linear map between
M₂ that commutes with the quadratic forms.
The composition of two isometries between quadratic forms.
There is a zero map from any module with the zero form.
There is a zero map from the trivial module.
Maps into the zero module are trivial