Isometric linear maps #
Main definitions #
QuadraticMap.Isometry:LinearMaps which map between two different quadratic forms
Notation #
Q₁ →qᵢ Q₂ is notation for Q₁.Isometry Q₂.
structure
QuadraticMap.Isometry
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
(Q₁ : QuadraticMap R M₁ N)
(Q₂ : QuadraticMap R M₂ N)
extends M₁ →ₗ[R] M₂ :
Type (max u_3 u_4)
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
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
QuadraticMap.Isometry.instFunLike
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
:
instance
QuadraticMap.Isometry.instLinearMapClass
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
:
LinearMapClass (Q₁ →qᵢ Q₂) R M₁ M₂
Equations
- ⋯ = ⋯
theorem
QuadraticMap.Isometry.toLinearMap_injective
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
:
Function.Injective QuadraticMap.Isometry.toLinearMap
theorem
QuadraticMap.Isometry.ext
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
⦃f g : Q₁ →qᵢ Q₂⦄
(h : ∀ (x : M₁), f x = g x)
:
f = g
def
QuadraticMap.Isometry.Simps.apply
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
(f : Q₁ →qᵢ Q₂)
:
M₁ → M₂
See Note [custom simps projection].
Equations
Instances For
@[simp]
theorem
QuadraticMap.Isometry.map_app
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
(f : Q₁ →qᵢ Q₂)
(m : M₁)
:
Q₂ (f m) = Q₁ m
@[simp]
theorem
QuadraticMap.Isometry.coe_toLinearMap
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
(f : Q₁ →qᵢ Q₂)
:
⇑f.toLinearMap = ⇑f
def
QuadraticMap.Isometry.id
{R : Type u_1}
{M : Type u_2}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
(Q : QuadraticMap R M N)
:
Q →qᵢ Q
The identity isometry from a quadratic form to itself.
Equations
- QuadraticMap.Isometry.id Q = { toLinearMap := LinearMap.id, map_app' := ⋯ }
Instances For
@[simp]
theorem
QuadraticMap.Isometry.id_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[Module R M]
[Module R N]
(Q : QuadraticMap R M N)
(a : M)
:
(QuadraticMap.Isometry.id Q) a = a
def
QuadraticMap.Isometry.ofEq
{R : Type u_1}
{M₁ : Type u_3}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid N]
[Module R M₁]
[Module R N]
{Q₁ Q₂ : QuadraticMap R M₁ N}
(h : Q₁ = Q₂)
:
Q₁ →qᵢ Q₂
The identity isometry between equal quadratic forms.
Equations
- QuadraticMap.Isometry.ofEq h = { toLinearMap := LinearMap.id, map_app' := ⋯ }
Instances For
@[simp]
theorem
QuadraticMap.Isometry.ofEq_apply
{R : Type u_1}
{M₁ : Type u_3}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid N]
[Module R M₁]
[Module R N]
{Q₁ Q₂ : QuadraticMap R M₁ N}
(h : Q₁ = Q₂)
(a : M₁)
:
(QuadraticMap.Isometry.ofEq h) a = a
@[simp]
theorem
QuadraticMap.Isometry.ofEq_rfl
{R : Type u_1}
{M₁ : Type u_3}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid N]
[Module R M₁]
[Module R N]
{Q : QuadraticMap R M₁ N}
:
def
QuadraticMap.Isometry.comp
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{M₃ : Type u_5}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
{Q₃ : QuadraticMap R M₃ N}
(g : Q₂ →qᵢ Q₃)
(f : Q₁ →qᵢ Q₂)
:
Q₁ →qᵢ Q₃
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
@[simp]
theorem
QuadraticMap.Isometry.comp_apply
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{M₃ : Type u_5}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
{Q₃ : QuadraticMap R M₃ N}
(g : Q₂ →qᵢ Q₃)
(f : Q₁ →qᵢ Q₂)
(x : M₁)
:
(g.comp f) x = g (f x)
@[simp]
theorem
QuadraticMap.Isometry.toLinearMap_comp
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{M₃ : Type u_5}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
{Q₃ : QuadraticMap R M₃ N}
(g : Q₂ →qᵢ Q₃)
(f : Q₁ →qᵢ Q₂)
:
(g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
@[simp]
theorem
QuadraticMap.Isometry.id_comp
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
(f : Q₁ →qᵢ Q₂)
:
(QuadraticMap.Isometry.id Q₂).comp f = f
@[simp]
theorem
QuadraticMap.Isometry.comp_id
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
(f : Q₁ →qᵢ Q₂)
:
f.comp (QuadraticMap.Isometry.id Q₁) = f
theorem
QuadraticMap.Isometry.comp_assoc
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{M₃ : Type u_5}
{M₄ : Type u_6}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[Module R M₄]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
{Q₃ : QuadraticMap R M₃ N}
{Q₄ : QuadraticMap R M₄ N}
(h : Q₃ →qᵢ Q₄)
(g : Q₂ →qᵢ Q₃)
(f : Q₁ →qᵢ Q₂)
:
(h.comp g).comp f = h.comp (g.comp f)
instance
QuadraticMap.Isometry.instZeroOfNat
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₂ : QuadraticMap R M₂ N}
:
There is a zero map from any module with the zero form.
Equations
- QuadraticMap.Isometry.instZeroOfNat = { zero := let __src := 0; { toLinearMap := __src, map_app' := ⋯ } }
instance
QuadraticMap.Isometry.hasZeroOfSubsingleton
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
[Subsingleton M₁]
:
There is a zero map from the trivial module.
Equations
- QuadraticMap.Isometry.hasZeroOfSubsingleton = { zero := let __src := 0; { toLinearMap := __src, map_app' := ⋯ } }
instance
QuadraticMap.Isometry.instSubsingleton
{R : Type u_1}
{M₁ : Type u_3}
{M₂ : Type u_4}
{N : Type u_7}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N]
[Module R M₁]
[Module R M₂]
[Module R N]
{Q₁ : QuadraticMap R M₁ N}
{Q₂ : QuadraticMap R M₂ N}
[Subsingleton M₂]
:
Subsingleton (Q₁ →qᵢ Q₂)
Maps into the zero module are trivial
Equations
- ⋯ = ⋯