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), 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)
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) :
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) :
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) :
@[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ᵒᵖ} :
Equations
- sesq_form.inhabited = {default := 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) :
S.is_ortho 0 x
@[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ᵒᵖ} :
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 := _}
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ᵒᵖ} :
sesq_form R M I → Prop
The proposition that a sesquilinear form is reflexive
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} :
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} :
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ᵒᵖ} :
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} :
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} :
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ᵒᵖ} :
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) :
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) :