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.toFun (x + y) = self.toFun x + self.toFun y
• 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.

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₂} (self : Q₁ →qᵢ Q₂) (m : M₁) : Q₂ (self.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

• 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} [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

• ⋯ = ⋯

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 __spread.0 := LinearMap.id; { toLinearMap := __spread.0, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.Isometry.ofEq_apply {R : Type u_2} {M₁ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₁} (h : Q₁ = Q₂) (a : M₁) : (QuadraticForm.Isometry.ofEq h) a = a

def QuadraticForm.Isometry.ofEq {R : Type u_2} {M₁ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₁} (h : Q₁ = Q₂) : Q₁ →qᵢ Q₂

The identity isometry between equal quadratic forms.

Equations

• QuadraticForm.Isometry.ofEq h = let __spread.0 := LinearMap.id; { toLinearMap := __spread.0, map_app' := ⋯ }

@[simp]

theorem QuadraticForm.Isometry.ofEq_rfl {R : Type u_2} {M₁ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] {Q : QuadraticForm R M₁} : QuadraticForm.Isometry.ofEq ⋯ = QuadraticForm.Isometry.id Q

@[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₁) : (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} [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

• g.comp f = let __spread.0 := g.toLinearMap ∘ₗ f.toLinearMap; { toFun := fun (x : M₁) => g (f x), map_add' := ⋯, map_smul' := ⋯, map_app' := ⋯ }

@[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₂) : (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} [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.id Q₂).comp 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₂) : f.comp (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₂) : (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} [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.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} [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' := ⋯ } }

instance QuadraticForm.Isometry.instSubsingleton {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

• ⋯ = ⋯