# Isometric linear maps #

## Main definitions #

• QuadraticForm.Isometry: LinearMaps which map between two different quadratic forms

## Notation #

Q₁ →qᵢ Q₂ is notation for Q₁.Isometry Q₂.

structure QuadraticForm.Isometry {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] (Q₁ : ) (Q₂ : ) extends :
Type (max u_4 u_5)

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_add' : ∀ (x y : M₁), self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' : ∀ (m : R) (x : M₁), self.toFun (m x) = () m self.toFun x
• map_app' : ∀ (m : M₁), Q₂ (self.toFun m) = Q₁ m

The quadratic form agrees across the map.

Instances For
theorem QuadraticForm.Isometry.map_app' {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (self : Q₁ →qᵢ Q₂) (m : M₁) :
Q₂ (self.toFun m) = Q₁ m

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
instance QuadraticForm.Isometry.instFunLike {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } :
FunLike (Q₁ →qᵢ Q₂) M₁ M₂
Equations
• QuadraticForm.Isometry.instFunLike = { coe := fun (f : Q₁ →qᵢ Q₂) => f.toLinearMap, coe_injective' := }
instance QuadraticForm.Isometry.instLinearMapClass {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } :
LinearMapClass (Q₁ →qᵢ Q₂) R M₁ M₂
Equations
• =
theorem QuadraticForm.Isometry.toLinearMap_injective {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } :
theorem QuadraticForm.Isometry.ext {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } ⦃f : Q₁ →qᵢ Q₂ ⦃g : Q₁ →qᵢ Q₂ (h : ∀ (x : M₁), f x = g x) :
f = g
def QuadraticForm.Isometry.Simps.apply {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) :
M₁M₂

See Note [custom simps projection].

Equations
Instances For
@[simp]
theorem QuadraticForm.Isometry.map_app {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) (m : M₁) :
Q₂ (f m) = Q₁ m
@[simp]
theorem QuadraticForm.Isometry.coe_toLinearMap {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) :
f.toLinearMap = f
@[simp]
theorem QuadraticForm.Isometry.id_apply {R : Type u_2} {M : Type u_3} [] [] [Module R M] (Q : ) (a : M) :
= a
def QuadraticForm.Isometry.id {R : Type u_2} {M : Type u_3} [] [] [Module R M] (Q : ) :

The identity isometry from a quadratic form to itself.

Equations
• = let __spread.0 := LinearMap.id; { toLinearMap := __spread.0, map_app' := }
Instances For
@[simp]
theorem QuadraticForm.Isometry.ofEq_apply {R : Type u_2} {M₁ : Type u_4} [] [] [Module R M₁] {Q₁ : } {Q₂ : } (h : Q₁ = Q₂) (a : M₁) :
= a
def QuadraticForm.Isometry.ofEq {R : Type u_2} {M₁ : Type u_4} [] [] [Module R M₁] {Q₁ : } {Q₂ : } (h : Q₁ = Q₂) :
Q₁ →qᵢ Q₂

The identity isometry between equal quadratic forms.

Equations
• = let __spread.0 := LinearMap.id; { toLinearMap := __spread.0, map_app' := }
Instances For
@[simp]
theorem QuadraticForm.Isometry.ofEq_rfl {R : Type u_2} {M₁ : Type u_4} [] [] [Module R M₁] {Q : } :
@[simp]
theorem QuadraticForm.Isometry.comp_apply {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : } {Q₂ : } {Q₃ : } (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) (x : M₁) :
(g.comp f) x = g (f x)
def QuadraticForm.Isometry.comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : } {Q₂ : } {Q₃ : } (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
Q₁ →qᵢ Q₃

The composition of two isometries between quadratic forms.

Equations
• g.comp f = let __spread.0 := g.toLinearMap ∘ₗ f.toLinearMap; { toFun := fun (x : M₁) => g (f x), map_add' := , map_smul' := , map_app' := }
Instances For
@[simp]
theorem QuadraticForm.Isometry.toLinearMap_comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : } {Q₂ : } {Q₃ : } (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
(g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
@[simp]
theorem QuadraticForm.Isometry.id_comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) :
.comp f = f
@[simp]
theorem QuadraticForm.Isometry.comp_id {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } (f : Q₁ →qᵢ Q₂) :
f.comp = f
theorem QuadraticForm.Isometry.comp_assoc {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} {M₄ : Type u_7} [] [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] {Q₁ : } {Q₂ : } {Q₃ : } {Q₄ : } (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
(h.comp g).comp f = h.comp (g.comp f)
instance QuadraticForm.Isometry.instZeroOfNat {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₂ : } :
Zero (0 →qᵢ Q₂)

There is a zero map from any module with the zero form.

Equations
• QuadraticForm.Isometry.instZeroOfNat = { zero := let __src := 0; { toLinearMap := __src, map_app' := } }
instance QuadraticForm.Isometry.hasZeroOfSubsingleton {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } [] :
Zero (Q₁ →qᵢ Q₂)

There is a zero map from the trivial module.

Equations
• QuadraticForm.Isometry.hasZeroOfSubsingleton = { zero := let __src := 0; { toLinearMap := __src, map_app' := } }
instance QuadraticForm.Isometry.instSubsingleton {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [] [] [] [Module R M₁] [Module R M₂] {Q₁ : } {Q₂ : } [] :
Subsingleton (Q₁ →qᵢ Q₂)

Maps into the zero module are trivial

Equations
• =