Isometric linear maps #
Main definitions #
QuadraticMap.Isometry
:LinearMap
s which map between two different quadratic forms
Notation #
Q₁ →qᵢ Q₂
is notation for Q₁.Isometry Q₂
.
An isometry between two quadratic spaces M₁, Q₁
and M₂, Q₂
over a ring R
,
is a linear map between M₁
and M₂
that commutes with the quadratic forms.
- toFun : M₁ → M₂
- map_smul' : ∀ (m : R) (x : M₁), self.toFun (m • x) = (RingHom.id R) m • self.toFun x
- map_app' : ∀ (m : M₁), Q₂ (self.toFun m) = Q₁ m
The quadratic form agrees across the map.
Instances For
The quadratic form agrees across the map.
An isometry between two quadratic spaces M₁, Q₁
and M₂, Q₂
over a ring R
,
is a linear map between M₁
and M₂
that commutes with the quadratic forms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
See Note [custom simps projection].
Equations
Instances For
The identity isometry from a quadratic form to itself.
Equations
- QuadraticMap.Isometry.id Q = { toLinearMap := LinearMap.id, map_app' := ⋯ }
Instances For
The identity isometry between equal quadratic forms.
Equations
- QuadraticMap.Isometry.ofEq h = { toLinearMap := LinearMap.id, map_app' := ⋯ }
Instances For
The composition of two isometries between quadratic forms.
Equations
- g.comp f = { toFun := fun (x : M₁) => g (f x), map_add' := ⋯, map_smul' := ⋯, map_app' := ⋯ }
Instances For
There is a zero map from any module with the zero form.
Equations
- QuadraticMap.Isometry.instZeroOfNat = { zero := let __src := 0; { toLinearMap := __src, map_app' := ⋯ } }
There is a zero map from the trivial module.
Equations
- QuadraticMap.Isometry.hasZeroOfSubsingleton = { zero := let __src := 0; { toLinearMap := __src, map_app' := ⋯ } }
Maps into the zero module are trivial
Equations
- ⋯ = ⋯