# mathlibdocumentation

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.

## Tags

Sesquilinear form,

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

A sesquilinear form over a module

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

Equations
theorem sesq_form.add_left {R : Type u} {M : Type v} [ring R] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S : M I} (x : M) :
S 0 x = 0

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

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

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

theorem sesq_form.sub_left {R : Type u} {M : Type v} [ring R] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S D : M I} :
(∀ (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] [ M] {I : R ≃+* Rᵒᵖ} :

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

Equations
def sesq_form.is_ortho {R : Type u} {M : Type v} [ring R] [ M] {I : R ≃+* Rᵒᵖ} :
M IM → 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] [ M] {I : R ≃+* Rᵒᵖ} {S : M I} (x : M) :
S.is_ortho 0 x

theorem sesq_form.is_add_monoid_hom_left {R : Type u} {M : Type v} [ring R] [ M] {I : R ≃+* Rᵒᵖ} (S : M I) (x : M) :
is_add_monoid_hom (λ (z : M), S z x)

theorem sesq_form.is_add_monoid_hom_right {R : Type u} {M : Type v} [ring R] [ M] {I : R ≃+* Rᵒᵖ} (S : M I) (x : M) :
is_add_monoid_hom (λ (z : M), S x z)

theorem sesq_form.map_sum_left {R : Type u} {M : Type v} [ring R] [ M] {I : R ≃+* Rᵒᵖ} {α : Type u_1} (S : 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.map_sum_right {R : Type u} {M : Type v} [ring R] [ M] {I : R ≃+* Rᵒᵖ} {α : Type u_1} (S : M I) (t : finset α) (g : α → M) (w : M) :
S w (∑ (i : α) in t, g i) = ∑ (i : α) in t, S w (g i)

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

Equations
theorem sesq_form.ortho_smul_left {R : Type u_1} [domain R] {M : Type v} [ M] {K : R ≃+* Rᵒᵖ} {G : M K} {x y : M} {a : R} :
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} [ M] {K : R ≃+* Rᵒᵖ} {G : M K} {x y : M} {a : R} :
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] [ M] {I : R ≃+* Rᵒᵖ} :
M I → Prop

The proposition that a sesquilinear form is reflexive

Equations
• = ∀ (x y : M), S x y = 0S y x = 0
theorem refl_sesq_form.eq_zero {R : Type u_1} {M : Type u_2} [ring R] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* 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] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S : M I} :

theorem sym_sesq_form.ortho_sym {R : Type u_1} {M : Type u_2} [ring R] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} :
M I → Prop

The proposition that a sesquilinear form is alternating

Equations
• = ∀ (x : M), S x x = 0
theorem alt_sesq_form.self_eq_zero {R : Type u_1} {M : Type u_2} [ring R] [ M] {I : R ≃+* Rᵒᵖ} {S : 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] [ M] {I : R ≃+* Rᵒᵖ} {S : M I} (H : alt_sesq_form.is_alt S) (x y : M) :
-S x y = S y x