Isometric linear maps

In this file, we define isometries of bilinear spaces as linear maps that respect the associated bilinear forms. This file should be kept in sync with the corresponding file for quadratic maps, namely Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean

Main definitions

• LinearMap.BilinForm.Isometry: LinearMaps which respect a given pair of bilinear forms

Notation

B₁ →bᵢ B₂ is notation for B₁.Isometry B₂.

structure LinearMap.BilinForm.Isometry {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (B₁ : LinearMap.BilinForm R M₁) (B₂ : LinearMap.BilinForm R M₂) extends M₁ →ₗ[R] M₂ : Type (max u_3 u_4)

An isometry between two bilinear spaces M₁, B₁ and M₂, B₂ over a ring R, is a linear map between M₁ and M₂ that commutes with the bilinear 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' : M₁) : (B₂ (self.toFun m)) (self.toFun m') = (B₁ m) m'

  The bilinear forms agree across the map.

def LinearMap.BilinForm.Isometry.«term_→bᵢ_» : Lean.TrailingParserDescr

An isometry between two bilinear spaces M₁, B₁ and M₂, B₂ over a ring R, is a linear map between M₁ and M₂ that commutes with the bilinear forms.

Equations

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

@[implicit_reducible]

instance LinearMap.BilinForm.Isometry.instFunLike {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} : FunLike (B₁ →bᵢ B₂) M₁ M₂

Equations

• LinearMap.BilinForm.Isometry.instFunLike = { coe := fun (f : B₁ →bᵢ B₂) => ⇑f.toLinearMap, coe_injective' := ⋯ }

instance LinearMap.BilinForm.Isometry.instLinearMapClass {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} : LinearMapClass (B₁ →bᵢ B₂) R M₁ M₂

theorem LinearMap.BilinForm.Isometry.toLinearMap_injective {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} : Function.Injective toLinearMap

theorem LinearMap.BilinForm.Isometry.ext {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} ⦃f g : B₁ →bᵢ B₂⦄ (h : ∀ (x : M₁), f x = g x) : f = g

theorem LinearMap.BilinForm.Isometry.ext_iff {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} {f g : B₁ →bᵢ B₂} : f = g ↔ ∀ (x : M₁), f x = g x

def LinearMap.BilinForm.Isometry.Simps.apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂) : M₁ → M₂

See Note [custom simps projection].

Equations

• LinearMap.BilinForm.Isometry.Simps.apply f = ⇑f

@[simp]

theorem LinearMap.BilinForm.Isometry.map_app {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂) (m m' : M₁) : (B₂ (f m)) (f m') = (B₁ m) m'

@[simp]

theorem LinearMap.BilinForm.Isometry.coe_toLinearMap {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂) : ⇑f.toLinearMap = ⇑f

def LinearMap.BilinForm.Isometry.id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : B →bᵢ B

The identity isometry from a bilinear form to itself.

Equations

• LinearMap.BilinForm.Isometry.id B = { toLinearMap := LinearMap.id, map_app' := ⋯ }

@[simp]

theorem LinearMap.BilinForm.Isometry.id_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (x : M) : (id B) x = x

def LinearMap.BilinForm.Isometry.ofEq {R : Type u_1} {M₁ : Type u_3} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] {B₁ B₂ : LinearMap.BilinForm R M₁} (h : B₁ = B₂) : B₁ →bᵢ B₂

The identity isometry between equal bilinear forms.

Equations

• LinearMap.BilinForm.Isometry.ofEq h = { toLinearMap := LinearMap.id, map_app' := ⋯ }

@[simp]

theorem LinearMap.BilinForm.Isometry.ofEq_apply {R : Type u_1} {M₁ : Type u_3} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] {B₁ B₂ : LinearMap.BilinForm R M₁} (h : B₁ = B₂) (x : M₁) : (ofEq h) x = x

@[simp]

theorem LinearMap.BilinForm.Isometry.ofEq_rfl {R : Type u_1} {M₁ : Type u_3} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] {B : LinearMap.BilinForm R M₁} : ofEq ⋯ = id B

def LinearMap.BilinForm.Isometry.comp {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} {B₃ : LinearMap.BilinForm R M₃} (g : B₂ →bᵢ B₃) (f : B₁ →bᵢ B₂) : B₁ →bᵢ B₃

The composition of two isometries between bilinear forms.

Equations

• g.comp f = { toFun := fun (x : M₁) => g (f x), map_add' := ⋯, map_smul' := ⋯, map_app' := ⋯ }

@[simp]

theorem LinearMap.BilinForm.Isometry.comp_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} {B₃ : LinearMap.BilinForm R M₃} (g : B₂ →bᵢ B₃) (f : B₁ →bᵢ B₂) (x : M₁) : (g.comp f) x = g (f x)

@[simp]

theorem LinearMap.BilinForm.Isometry.toLinearMap_comp {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₁] [Module R M₂] [Module R M₃] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} {B₃ : LinearMap.BilinForm R M₃} (g : B₂ →bᵢ B₃) (f : B₁ →bᵢ B₂) : (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

@[simp]

theorem LinearMap.BilinForm.Isometry.id_comp {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂) : (id B₂).comp f = f

@[simp]

theorem LinearMap.BilinForm.Isometry.comp_id {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂) : f.comp (id B₁) = f

theorem LinearMap.BilinForm.Isometry.comp_assoc {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} {M₄ : Type u_6} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} {B₃ : LinearMap.BilinForm R M₃} {B₄ : LinearMap.BilinForm R M₄} (h : B₃ →bᵢ B₄) (g : B₂ →bᵢ B₃) (f : B₁ →bᵢ B₂) : (h.comp g).comp f = h.comp (g.comp f)

@[implicit_reducible]

instance LinearMap.BilinForm.Isometry.instZeroOfNat {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₂ : LinearMap.BilinForm R M₂} : Zero (0 →bᵢ B₂)

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

Equations

• LinearMap.BilinForm.Isometry.instZeroOfNat = { zero := let __src := 0; { toLinearMap := __src, map_app' := ⋯ } }

@[implicit_reducible]

instance LinearMap.BilinForm.Isometry.hasZeroOfSubsingleton {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} [Subsingleton M₁] : Zero (B₁ →bᵢ B₂)

There is a zero map from the trivial module.

Equations

• LinearMap.BilinForm.Isometry.hasZeroOfSubsingleton = { zero := let __src := 0; { toLinearMap := __src, map_app' := ⋯ } }

instance LinearMap.BilinForm.Isometry.instSubsingleton {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} [Subsingleton M₂] : Subsingleton (B₁ →bᵢ B₂)

Maps into the zero module are trivial