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.

Instances For

source

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

Instances For

source

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

source

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₂

source

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 toLinearMap

source

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

source

theorem QuadraticMap.Isometry.ext_iff {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₂} :

f = g ↔ ∀ (x : M₁), f x = g x

source

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

source

@[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

source

@[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

source

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

Instances For

source

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

(id Q) a = a

source

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

Instances For

source

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

(ofEq h) a = a

source

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

ofEq ⋯ = id Q

source

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

Instances For

source

@[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)

source

@[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

source

@[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₂) :

(id Q₂).comp f = f

source

@[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 (id Q₁) = f

source

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)

source

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

source

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

source

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

Documentation

Mathlib.LinearAlgebra.QuadraticForm.Isometry

Isometric linear maps #

Main definitions #

Notation #