mathlib documentation

linear_algebra.sesquilinear_form

Sesquilinear form

This file defines a sesquilinear form over a module. The definition requires a ring antiautomorphism on the scalar ring. Basic ideas such as orthogonality are also introduced.

A sesquilinear form on an R-module M, is a function from M × M to R, that is linear in the first argument and antilinear in the second, with respect to an antiautomorphism on R (an antiisomorphism from R to R).

Notations

Given any term S of type sesq_form, due to a coercion, can use the notation S x y to refer to the function field, ie. S x y = S.sesq x y.

References

https://en.wikipedia.org/wiki/Sesquilinear_form#Over_arbitrary_rings

Tags

Sesquilinear form,

structure sesq_form (R : Type u) (M : Type v) [ring R] (I : R ≃+* Rᵒᵖ) [add_comm_group M] [module R M] :

Type (max u v)

sesq : M → M → R
sesq_add_left : ∀ (x y z : M), c.sesq (x + y) z = c.sesq x z + c.sesq y z
sesq_smul_left : ∀ (a : R) (x y : M), c.sesq (a • x) y = a * c.sesq x y
sesq_add_right : ∀ (x y z : M), c.sesq x (y + z) = c.sesq x y + c.sesq x z
sesq_smul_right : ∀ (a : R) (x y : M), c.sesq x (a • y) = (opposite.unop (⇑I a)) * c.sesq x y

A sesquilinear form over a module

@[instance]

def sesq_form.has_coe_to_fun {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} :

has_coe_to_fun (sesq_form R M I)

Equations

sesq_form.has_coe_to_fun = {F := λ (S : sesq_form R M I), M → M → R, coe := λ (S : sesq_form R M I), S.sesq}

theorem sesq_form.add_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x y z : M) :

⇑S (x + y) z = ⇑S x z + ⇑S y z

theorem sesq_form.smul_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (a : R) (x y : M) :

⇑S (a • x) y = a * ⇑S x y

theorem sesq_form.add_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x y z : M) :

⇑S x (y + z) = ⇑S x y + ⇑S x z

theorem sesq_form.smul_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (a : R) (x y : M) :

⇑S x (a • y) = (opposite.unop (⇑I a)) * ⇑S x y

theorem sesq_form.zero_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x : M) :

⇑S 0 x = 0

theorem sesq_form.zero_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x : M) :

⇑S x 0 = 0

theorem sesq_form.neg_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x y : M) :

⇑S (-x) y = -⇑S x y

theorem sesq_form.neg_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x y : M) :

⇑S x (-y) = -⇑S x y

theorem sesq_form.sub_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x y z : M) :

⇑S (x - y) z = ⇑S x z - ⇑S y z

theorem sesq_form.sub_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x y z : M) :

⇑S x (y - z) = ⇑S x y - ⇑S x z

@[ext]

theorem sesq_form.ext {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S D : sesq_form R M I} (H : ∀ (x y : M), ⇑S x y = ⇑D x y) :

S = D

@[instance]

def sesq_form.add_comm_group {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} :

add_comm_group (sesq_form R M I)

Equations

sesq_form.add_comm_group = {add := λ (S D : sesq_form R M I), {sesq := λ (x y : M), ⇑S x y + ⇑D x y, sesq_add_left := _, sesq_smul_left := _, sesq_add_right := _, sesq_smul_right := _}, add_assoc := _, zero := {sesq := λ (x y : M), 0, sesq_add_left := _, sesq_smul_left := _, sesq_add_right := _, sesq_smul_right := _}, zero_add := _, add_zero := _, neg := λ (S : sesq_form R M I), {sesq := λ (x y : M), -S.sesq x y, sesq_add_left := _, sesq_smul_left := _, sesq_add_right := _, sesq_smul_right := _}, add_left_neg := _, add_comm := _}

@[instance]

def sesq_form.inhabited {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} :

inhabited (sesq_form R M I)

Equations

sesq_form.inhabited = {default := 0}

def sesq_form.is_ortho {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} (S : sesq_form R M I) (x y : M) :

Prop

The proposition that two elements of a sesquilinear form space are orthogonal

Equations

S.is_ortho x y = (⇑S x y = 0)

theorem sesq_form.ortho_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (x : M) :

@[instance]

def sesq_form.to_module {R : Type u_1} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {J : R ≃+* Rᵒᵖ} :

module R (sesq_form R M J)

Equations

sesq_form.to_module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (c : R) (S : sesq_form R M J), {sesq := λ (x y : M), c * ⇑S x y, sesq_add_left := _, sesq_smul_left := _, sesq_add_right := _, sesq_smul_right := _}}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}

theorem sesq_form.ortho_smul_left {R : Type u_1} [domain R] {M : Type v} [add_comm_group M] [module R M] {K : R ≃+* Rᵒᵖ} {G : sesq_form R M K} {x y : M} {a : R} (ha : a ≠ 0) :

G.is_ortho x y ↔ G.is_ortho (a • x) y

theorem sesq_form.ortho_smul_right {R : Type u_1} [domain R] {M : Type v} [add_comm_group M] [module R M] {K : R ≃+* Rᵒᵖ} {G : sesq_form R M K} {x y : M} {a : R} (ha : a ≠ 0) :

G.is_ortho x y ↔ G.is_ortho x (a • y)

def refl_sesq_form.is_refl {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} (S : sesq_form R M I) :

Prop

The proposition that a sesquilinear form is reflexive

Equations

refl_sesq_form.is_refl S = ∀ (x y : M), ⇑S x y = 0 → ⇑S y x = 0

theorem refl_sesq_form.eq_zero {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (H : refl_sesq_form.is_refl S) {x y : M} (a : ⇑S x y = 0) :

⇑S y x = 0

theorem refl_sesq_form.ortho_sym {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (H : refl_sesq_form.is_refl S) {x y : M} :

S.is_ortho x y ↔ S.is_ortho y x

def sym_sesq_form.is_sym {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} (S : sesq_form R M I) :

Prop

The proposition that a sesquilinear form is symmetric

Equations

sym_sesq_form.is_sym S = ∀ (x y : M), opposite.unop (⇑I (⇑S x y)) = ⇑S y x

theorem sym_sesq_form.sym {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (H : sym_sesq_form.is_sym S) (x y : M) :

opposite.unop (⇑I (⇑S x y)) = ⇑S y x

theorem sym_sesq_form.is_refl {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (H : sym_sesq_form.is_sym S) :

refl_sesq_form.is_refl S

theorem sym_sesq_form.ortho_sym {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (H : sym_sesq_form.is_sym S) {x y : M} :

S.is_ortho x y ↔ S.is_ortho y x

def alt_sesq_form.is_alt {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} (S : sesq_form R M I) :

Prop

The proposition that a sesquilinear form is alternating

Equations

alt_sesq_form.is_alt S = ∀ (x : M), ⇑S x x = 0

theorem alt_sesq_form.self_eq_zero {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (H : alt_sesq_form.is_alt S) (x : M) :

⇑S x x = 0

theorem alt_sesq_form.neg {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {S : sesq_form R M I} (H : alt_sesq_form.is_alt S) (x y : M) :

-⇑S x y = ⇑S y x