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_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.

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

Equations

• QuadraticMap.Isometry.instFunLike = { coe := fun (f : Q₁ →qᵢ Q₂) => ⇑f.toLinearMap, coe_injective' := ⋯ }

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₂

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

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

@[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' := ⋯ }

@[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' := ⋯ }

@[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} : QuadraticMap.Isometry.ofEq ⋯ = QuadraticMap.Isometry.id Q

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' := ⋯ }

@[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} : Zero (0 →qᵢ Q₂)

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₁] : Zero (Q₁ →qᵢ Q₂)

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