Isometric equivalences with respect to bilinear forms

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

Main definitions

• LinearMap.BilinForm.IsometryEquiv: LinearEquivs which map between two different bilinear forms
• LinearMap.BilinForm.Equivalent: propositional version of the above

structure LinearMap.BilinForm.IsometryEquiv {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 isometric equivalence between two bilinear spaces M₁, B₁ and M₂, B₂ over a ring R, is a linear equivalence between M₁ and M₂ that commutes with the bilinear forms.

• toFun : M₁ → M₂
• map_add' (x y : M₁) : (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' (m : R) (x : M₁) : (↑self.toLinearEquiv).toFun (m • x) = (RingHom.id R) m • (↑self.toLinearEquiv).toFun x
• invFun : M₂ → M₁
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• map_app' (n m : M₁) : (B₂ ((↑self.toLinearEquiv).toFun n)) ((↑self.toLinearEquiv).toFun m) = (B₁ n) m

def LinearMap.BilinForm.Equivalent {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₂) : Prop

Two bilinear forms over a ring R are equivalent if there exists an isometric equivalence between them: a linear equivalence that transforms one bilinear form into the other.

Equations

• B₁.Equivalent B₂ = Nonempty (B₁.IsometryEquiv B₂)

@[implicit_reducible]

instance LinearMap.BilinForm.IsometryEquiv.instEquivLike {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₂} : EquivLike (B₁.IsometryEquiv B₂) M₁ M₂

Equations

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

instance LinearMap.BilinForm.IsometryEquiv.instLinearEquivClass {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₂} : LinearEquivClass (B₁.IsometryEquiv B₂) R M₁ M₂

@[implicit_reducible]

instance LinearMap.BilinForm.IsometryEquiv.instCoeOutLinearEquivId {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₂} : CoeOut (B₁.IsometryEquiv B₂) (M₁ ≃ₗ[R] M₂)

Equations

• LinearMap.BilinForm.IsometryEquiv.instCoeOutLinearEquivId = { coe := LinearMap.BilinForm.IsometryEquiv.toLinearEquiv }

@[simp]

theorem LinearMap.BilinForm.IsometryEquiv.coe_toLinearEquiv {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₁.IsometryEquiv B₂) : ⇑f.toLinearEquiv = ⇑f

@[simp]

theorem LinearMap.BilinForm.IsometryEquiv.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₁.IsometryEquiv B₂) (m n : M₁) : (B₂ (f n)) (f m) = (B₁ n) m

def LinearMap.BilinForm.IsometryEquiv.refl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : B.IsometryEquiv B

The identity isometric equivalence between a bilinear form and itself.

Equations

• LinearMap.BilinForm.IsometryEquiv.refl B = { toLinearEquiv := LinearEquiv.refl R M, map_app' := ⋯ }

def LinearMap.BilinForm.IsometryEquiv.symm {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₁.IsometryEquiv B₂) : B₂.IsometryEquiv B₁

The inverse isometric equivalence of an isometric equivalence between two bilinear forms.

Equations

• f.symm = { toLinearEquiv := f.symm, map_app' := ⋯ }

def LinearMap.BilinForm.IsometryEquiv.trans {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₃} (f : B₁.IsometryEquiv B₂) (g : B₂.IsometryEquiv B₃) : B₁.IsometryEquiv B₃

The composition of two isometric equivalences between bilinear forms.

Equations

• f.trans g = { toLinearEquiv := f.trans g.toLinearEquiv, map_app' := ⋯ }

def LinearMap.BilinForm.IsometryEquiv.toIsometry {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₂} (g : B₁.IsometryEquiv B₂) : B₁ →bᵢ B₂

Isometric equivalences are isometric maps

Equations

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

@[simp]

theorem LinearMap.BilinForm.IsometryEquiv.toIsometry_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₂} (g : B₁.IsometryEquiv B₂) (x : M₁) : g.toIsometry x = g x

theorem LinearMap.BilinForm.Equivalent.refl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : LinearMap.BilinForm R M) : Q.Equivalent Q

theorem LinearMap.BilinForm.Equivalent.symm {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₂} (h : B₁.Equivalent B₂) : B₂.Equivalent B₁

theorem LinearMap.BilinForm.Equivalent.trans {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₃} (h : B₁.Equivalent B₂) (h' : B₂.Equivalent B₃) : B₁.Equivalent B₃

def LinearMap.BilinForm.isometryEquivOfCompLinearEquiv {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (B : LinearMap.BilinForm R M) (f : M₁ ≃ₗ[R] M) : B.IsometryEquiv (B.comp ↑f ↑f)

A bilinear form composed with a LinearEquiv is isometric to itself.

Equations

• B.isometryEquivOfCompLinearEquiv f = { toLinearEquiv := f.symm, map_app' := ⋯ }