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} [CommSemiring 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)

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

  The quadratic form agrees across the map.

def QuadraticForm.Isometry.«term_→qᵢ_» : Lean.TrailingParserDescr

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.

instance QuadraticForm.Isometry.instFunLike {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} : FunLike (Q₁ →qᵢ Q₂) M₁ M₂

Equations

• One or more equations did not get rendered due to their size.

instance QuadraticForm.Isometry.instLinearMapClass {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring 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₂

Equations

• (_ : LinearMapClass (Q₁ →qᵢ Q₂) R M₁ M₂) = (_ : SemilinearMapClass (Q₁ →qᵢ Q₂) (RingHom.id R) M₁ M₂)

theorem QuadraticForm.Isometry.toLinearMap_injective {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring 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} [CommSemiring 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} [CommSemiring 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].

Equations

• QuadraticForm.Isometry.Simps.apply f = ⇑f

@[simp]

theorem QuadraticForm.Isometry.map_app {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring 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} [CommSemiring 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} [CommSemiring 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} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticForm R M) : Q →qᵢ Q

The identity isometry from a quadratic form to itself.

Equations

• QuadraticForm.Isometry.id Q = let src := LinearMap.id; { toLinearMap := src, map_app' := (_ : ∀ (x : M), Q (LinearMap.id.toAddHom.toFun x) = Q (LinearMap.id.toAddHom.toFun x)) }

@[simp]

theorem QuadraticForm.Isometry.comp_apply {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [CommSemiring 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} [CommSemiring 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuadraticForm.Isometry.toLinearMap_comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [CommSemiring 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 = g.toLinearMap ∘ₗ f.toLinearMap

@[simp]

theorem QuadraticForm.Isometry.id_comp {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) : QuadraticForm.Isometry.comp (QuadraticForm.Isometry.id Q₂) f = f

@[simp]

theorem QuadraticForm.Isometry.comp_id {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) : QuadraticForm.Isometry.comp f (QuadraticForm.Isometry.id Q₁) = 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} [CommSemiring 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₂) : QuadraticForm.Isometry.comp (QuadraticForm.Isometry.comp h g) f = QuadraticForm.Isometry.comp h (QuadraticForm.Isometry.comp g f)

instance QuadraticForm.Isometry.instZeroIsometryOfNatQuadraticFormToOfNat0InstZeroQuadraticForm {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₂ : QuadraticForm R M₂} : Zero (0 →qᵢ Q₂)

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

Equations

• QuadraticForm.Isometry.instZeroIsometryOfNatQuadraticFormToOfNat0InstZeroQuadraticForm = { zero := let src := 0; { toLinearMap := src, map_app' := (_ : M₁ → Q₂ 0 = 0) } }

instance QuadraticForm.Isometry.hasZeroOfSubsingleton {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} [Subsingleton M₁] : 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' := (_ : ∀ (m : M₁), Q₂ (0.toAddHom.toFun m) = Q₁ m) } }

instance QuadraticForm.Isometry.instSubsingletonIsometry {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [CommSemiring 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

Equations

• (_ : Subsingleton (Q₁ →qᵢ Q₂)) = (_ : Subsingleton (Q₁ →qᵢ Q₂))