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 #

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), self.sesq (x + y) z = self.sesq x z + self.sesq y z
  • sesq_smul_left : ∀ (a : R) (x y : M), self.sesq (a x) y = a * self.sesq x y
  • sesq_add_right : ∀ (x y z : M), self.sesq x (y + z) = self.sesq x y + self.sesq x z
  • sesq_smul_right : ∀ (a : R) (x y : M), self.sesq x (a y) = (opposite.unop (I a)) * self.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) (λ (_x : sesq_form R M I), M → M → R)
Equations
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.has_add {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} :
Equations
@[instance]
def sesq_form.has_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} :
Equations
@[instance]
def sesq_form.has_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} :
Equations
@[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ᵒᵖ} :
Equations
@[instance]
def sesq_form.inhabited {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} :
Equations
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
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) :
S.is_ortho 0 x
@[simp]
theorem sesq_form.linear_map_left_apply {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 z : M) :
(S.linear_map_left x) z = S z x
def sesq_form.linear_map_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) :

For fixed y : M, the R-linear map sending x : M to S x y, where S is a sesquilinear form.

Equations
@[simp]
theorem sesq_form.add_monoid_hom_right_apply {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 z : M) :
def sesq_form.add_monoid_hom_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) :
M →+ R

For fixed x : M, the add_monoid_hom sending y : M to S x y, where S is a sesquilinear form.

Equations
theorem sesq_form.sum_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {α : Type u_1} (S : sesq_form R M I) (t : finset α) (g : α → M) (w : M) :
S (∑ (i : α) in t, g i) w = ∑ (i : α) in t, S (g i) w
theorem sesq_form.sum_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {α : Type u_1} (S : sesq_form R M I) (t : finset α) (g : α → M) (w : M) :
S w (∑ (i : α) in t, g i) = ∑ (i : α) in t, S w (g i)
def sesq_form.comp {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {M₂ : Type w} [add_comm_group M₂] [module R M₂] (S : sesq_form R M I) (f g : M₂ →ₗ[R] M) :
sesq_form R M₂ I

Apply the linear maps f and g to the left and right arguments of the sesquilinear form.

Equations
def sesq_form.comp_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) (f : M →ₗ[R] M) :
sesq_form R M I

Apply the linear map f to the left argument of the sesquilinear form.

Equations
def sesq_form.comp_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) (f : M →ₗ[R] M) :
sesq_form R M I

Apply the linear map f to the right argument of the sesquilinear form.

Equations
theorem sesq_form.comp_left_comp_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) (f g : M →ₗ[R] M) :
(S.comp_left f).comp_right g = S.comp f g
theorem sesq_form.comp_right_comp_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) (f g : M →ₗ[R] M) :
(S.comp_right g).comp_left f = S.comp f g
theorem sesq_form.comp_comp {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {M₂ : Type w} [add_comm_group M₂] [module R M₂] {M₃ : Type u_1} [add_comm_group M₃] [module R M₃] (S : sesq_form R M₃ I) (l r : M →ₗ[R] M₂) (l' r' : M₂ →ₗ[R] M₃) :
(S.comp l' r').comp l r = S.comp (l'.comp l) (r'.comp r)
@[simp]
theorem sesq_form.comp_apply {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {M₂ : Type w} [add_comm_group M₂] [module R M₂] (S : sesq_form R M₂ I) (l r : M →ₗ[R] M₂) (v w : M) :
(S.comp l r) v w = S (l v) (r w)
@[simp]
theorem sesq_form.comp_left_apply {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} (S : sesq_form R M I) (f : M →ₗ[R] M) (v w : M) :
(S.comp_left f) v w = S (f v) w
@[simp]
theorem sesq_form.comp_right_apply {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} (S : sesq_form R M I) (f : M →ₗ[R] M) (v w : M) :
(S.comp_right f) v w = S v (f w)
theorem sesq_form.comp_injective {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {I : R ≃+* Rᵒᵖ} {M₂ : Type w} [add_comm_group M₂] [module R M₂] (S₁ S₂ : sesq_form R M₂ I) {l r : M →ₗ[R] M₂} (hl : function.surjective l) (hr : function.surjective r) :
S₁.comp l r = S₂.comp l r S₁ = S₂

Let l, r be surjective linear maps, then two sesquilinear forms are equal if and only if the sesquilinear forms resulting from composition with l and r are equal.

@[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
theorem sesq_form.ortho_smul_left {R : Type u_1} [ring R] [is_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} [ring R] [is_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
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} :
S x y = 0S 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
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) :
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
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