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}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
(Q₁ : QuadraticForm R M₁)
(Q₂ : QuadraticForm R M₂)
extends
LinearMap
:
Type (max u_4 u_5)
- toFun : M₁ → M₂
- map_add' : ∀ (x y : M₁), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
- map_smul' : ∀ (r : R) (x : M₁), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
- map_app' : ∀ (m : M₁), ↑Q₂ (AddHom.toFun s.toAddHom 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.
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.
Instances For
instance
QuadraticForm.Isometry.instLinearMapClass
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
:
LinearMapClass (Q₁ →qᵢ Q₂) R M₁ M₂
theorem
QuadraticForm.Isometry.toLinearMap_injective
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
:
Function.Injective QuadraticForm.Isometry.toLinearMap
theorem
QuadraticForm.Isometry.ext
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
⦃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}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
(f : Q₁ →qᵢ Q₂)
:
M₁ → M₂
See Note [custom simps projection].
Instances For
@[simp]
theorem
QuadraticForm.Isometry.map_app
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
(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}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
(f : Q₁ →qᵢ Q₂)
:
↑f.toLinearMap = ↑f
@[simp]
theorem
QuadraticForm.Isometry.id_apply
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(Q : QuadraticForm R M)
:
∀ (a : M), ↑(QuadraticForm.Isometry.id Q) a = a
def
QuadraticForm.Isometry.id
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(Q : QuadraticForm R M)
:
Q →qᵢ Q
The identity isometry from a quadratic form to itself.
Instances For
@[simp]
theorem
QuadraticForm.Isometry.comp_apply
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
{Q₃ : QuadraticForm R M₃}
(g : Q₂ →qᵢ Q₃)
(f : Q₁ →qᵢ Q₂)
(x : M₁)
:
↑(QuadraticForm.Isometry.comp g 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}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
{Q₃ : QuadraticForm R M₃}
(g : Q₂ →qᵢ Q₃)
(f : Q₁ →qᵢ Q₂)
:
Q₁ →qᵢ Q₃
The composition of two isometries between quadratic forms.
Instances For
@[simp]
theorem
QuadraticForm.Isometry.toLinearMap_comp
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
{M₃ : Type u_6}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
{Q₃ : QuadraticForm R M₃}
(g : Q₂ →qᵢ Q₃)
(f : Q₁ →qᵢ Q₂)
:
(QuadraticForm.Isometry.comp g f).toLinearMap = LinearMap.comp g.toLinearMap f.toLinearMap
@[simp]
theorem
QuadraticForm.Isometry.id_comp
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
(f : Q₁ →qᵢ Q₂)
:
@[simp]
theorem
QuadraticForm.Isometry.comp_id
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
(f : Q₁ →qᵢ Q₂)
:
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}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[Module R M₄]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
{Q₃ : QuadraticForm R M₃}
{Q₄ : QuadraticForm R M₄}
(h : Q₃ →qᵢ Q₄)
(g : Q₂ →qᵢ Q₃)
(f : Q₁ →qᵢ Q₂)
:
instance
QuadraticForm.Isometry.instZeroIsometryOfNatQuadraticFormToOfNat0InstZeroQuadraticForm
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₂ : QuadraticForm R M₂}
:
There is a zero map from any module with the zero form.
instance
QuadraticForm.Isometry.hasZeroOfSubsingleton
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
[Subsingleton M₁]
:
There is a zero map from the trivial module.
instance
QuadraticForm.Isometry.instSubsingletonIsometry
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
{Q₁ : QuadraticForm R M₁}
{Q₂ : QuadraticForm R M₂}
[Subsingleton M₂]
:
Subsingleton (Q₁ →qᵢ Q₂)
Maps into the zero module are trivial