Bilinear form
This file defines a bilinear form over a module. Basic ideas such as orthogonality are also introduced, as well as reflexivive, symmetric and alternating bilinear forms. Adjoints of linear maps with respect to a bilinear form are also introduced.
A bilinear form on an R-module M, is a function from M x M to R, that is linear in both arguments
Notations
Given any term B of type bilin_form, due to a coercion, can use the notation B x y to refer to the function field, ie. B x y = B.bilin x y.
References
Tags
Bilinear form,
structure
bilin_form
(R : Type u)
(M : Type v)
[ring R]
[add_comm_group M]
[module R M] :
Type (max u v)
- bilin : M → M → R
- bilin_add_left : ∀ (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z
- bilin_smul_left : ∀ (a : R) (x y : M), c.bilin (a • x) y = a * c.bilin x y
- bilin_add_right : ∀ (x y z : M), c.bilin x (y + z) = c.bilin x y + c.bilin x z
- bilin_smul_right : ∀ (a : R) (x y : M), c.bilin x (a • y) = a * c.bilin x y
A bilinear form over a module
def
linear_map.to_bilin
{R : Type u}
{M : Type v}
[comm_ring R]
[add_comm_group M]
[module R M] :
(M →ₗ[R] M →ₗ[R] R) → bilin_form R M
A map with two arguments that is linear in both is a bilinear form
Equations
- f.to_bilin = {bilin := λ (x y : M), ⇑(⇑f x) y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
@[instance]
def
bilin_form.has_coe_to_fun
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M] :
has_coe_to_fun (bilin_form R M)
Equations
- bilin_form.has_coe_to_fun = {F := λ (B : bilin_form R M), M → M → R, coe := λ (B : bilin_form R M), B.bilin}
@[simp]
theorem
bilin_form.coe_fn_mk
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(f : M → M → R)
(h₁ : ∀ (x y z : M), f (x + y) z = f x z + f y z)
(h₂ : ∀ (a : R) (x y : M), f (a • x) y = a * f x y)
(h₃ : ∀ (x y z : M), f x (y + z) = f x y + f x z)
(h₄ : ∀ (a : R) (x y : M), f x (a • y) = a * f x y) :
⇑{bilin := f, bilin_add_left := h₁, bilin_smul_left := h₂, bilin_add_right := h₃, bilin_smul_right := h₄} = f
theorem
bilin_form.coe_fn_congr
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
{x x' y y' : M} :
theorem
bilin_form.add_left
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x y z : M) :
theorem
bilin_form.smul_left
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(a : R)
(x y : M) :
theorem
bilin_form.add_right
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x y z : M) :
theorem
bilin_form.smul_right
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(a : R)
(x y : M) :
theorem
bilin_form.zero_left
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x : M) :
theorem
bilin_form.zero_right
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x : M) :
theorem
bilin_form.neg_left
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x y : M) :
theorem
bilin_form.neg_right
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x y : M) :
theorem
bilin_form.sub_left
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x y z : M) :
theorem
bilin_form.sub_right
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x y z : M) :
@[ext]
theorem
bilin_form.ext
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B D : bilin_form R M} :
@[instance]
def
bilin_form.add_comm_group
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M] :
add_comm_group (bilin_form R M)
Equations
- bilin_form.add_comm_group = {add := λ (B D : bilin_form R M), {bilin := λ (x y : M), ⇑B x y + ⇑D x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, add_assoc := _, zero := {bilin := λ (x y : M), 0, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, zero_add := _, add_zero := _, neg := λ (B : bilin_form R M), {bilin := λ (x y : M), -B.bilin x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, add_left_neg := _, add_comm := _}
theorem
bilin_form.add_apply
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B D : bilin_form R M}
(x y : M) :
theorem
bilin_form.neg_apply
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x y : M) :
@[instance]
def
bilin_form.inhabited
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M] :
inhabited (bilin_form R M)
Equations
- bilin_form.inhabited = {default := 0}
@[instance]
def
bilin_form.to_module
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M] :
module R₂ (bilin_form R₂ M)
Equations
- bilin_form.to_module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (c : R₂) (B : bilin_form R₂ M), {bilin := λ (x y : M), c * ⇑B x y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
theorem
bilin_form.smul_apply
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M]
(F : bilin_form R₂ M)
(a : R₂)
(x y : M) :
def
bilin_form.to_linear_map
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M] :
bilin_form R₂ M → (M →ₗ[R₂] M →ₗ[R₂] R₂)
B.to_linear_map applies B on the left argument, then the right.
Equations
- F.to_linear_map = linear_map.mk₂ R₂ F.bilin _ _ _ _
def
bilin_form.bilin_linear_map_equiv
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M] :
Bilinear forms are equivalent to maps with two arguments that is linear in both.
Equations
- bilin_form.bilin_linear_map_equiv = {to_fun := bilin_form.to_linear_map _inst_5, map_add' := _, map_smul' := _, inv_fun := linear_map.to_bilin _inst_5, left_inv := _, right_inv := _}
theorem
bilin_form.coe_fn_to_linear_map
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M]
(F : bilin_form R₂ M)
(x : M) :
⇑(⇑(F.to_linear_map) x) = ⇑F x
theorem
bilin_form.map_sum_left
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M]
{α : Type u_2}
(B : bilin_form R₂ M)
(t : finset α)
(g : α → M)
(w : M) :
theorem
bilin_form.map_sum_right
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M]
{α : Type u_2}
(B : bilin_form R₂ M)
(t : finset α)
(g : α → M)
(v : M) :
def
bilin_form.comp
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{N : Type w}
[add_comm_group N]
[module R N] :
bilin_form R N → (M →ₗ[R] N) → (M →ₗ[R] N) → bilin_form R M
Apply a linear map on the left and right argument of a bilinear form.
Equations
- B.comp l r = {bilin := λ (x y : M), ⇑B (⇑l x) (⇑r y), bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
def
bilin_form.comp_left
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M] :
bilin_form R M → (M →ₗ[R] M) → bilin_form R M
Apply a linear map to the left argument of a bilinear form.
Equations
- B.comp_left f = B.comp f linear_map.id
def
bilin_form.comp_right
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M] :
bilin_form R M → (M →ₗ[R] M) → bilin_form R M
Apply a linear map to the right argument of a bilinear form.
Equations
- B.comp_right f = B.comp linear_map.id f
@[simp]
theorem
bilin_form.comp_left_comp_right
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(B : bilin_form R M)
(l r : M →ₗ[R] M) :
(B.comp_left l).comp_right r = B.comp l r
@[simp]
theorem
bilin_form.comp_right_comp_left
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(B : bilin_form R M)
(l r : M →ₗ[R] M) :
(B.comp_right r).comp_left l = B.comp l r
@[simp]
theorem
bilin_form.comp_apply
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{N : Type w}
[add_comm_group N]
[module R N]
(B : bilin_form R N)
(l r : M →ₗ[R] N)
(v w : M) :
@[simp]
theorem
bilin_form.comp_left_apply
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(B : bilin_form R M)
(f : M →ₗ[R] M)
(v w : M) :
@[simp]
theorem
bilin_form.comp_right_apply
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
(B : bilin_form R M)
(f : M →ₗ[R] M)
(v w : M) :
⇑(B.comp_right f) v w = ⇑B v (⇑f w)
theorem
bilin_form.comp_injective
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{N : Type w}
[add_comm_group N]
[module R N]
(B₁ B₂ : bilin_form R N)
(l r : M →ₗ[R] N) :
function.surjective ⇑l → function.surjective ⇑r → (B₁.comp l r = B₂.comp l r ↔ B₁ = B₂)
def
bilin_form.lin_mul_lin
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M] :
(M →ₗ[R₂] R₂) → (M →ₗ[R₂] R₂) → bilin_form R₂ M
lin_mul_lin f g is the bilinear form mapping x and y to f x * g y
Equations
- bilin_form.lin_mul_lin f g = {bilin := λ (x y : M), ⇑f x * ⇑g y, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}
@[simp]
theorem
bilin_form.lin_mul_lin_apply
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M]
{f g : M →ₗ[R₂] R₂}
(x y : M) :
@[simp]
theorem
bilin_form.lin_mul_lin_comp
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M]
{N : Type w}
[add_comm_group N]
[module R₂ N]
{f g : M →ₗ[R₂] R₂}
(l r : N →ₗ[R₂] M) :
(bilin_form.lin_mul_lin f g).comp l r = bilin_form.lin_mul_lin (f.comp l) (g.comp r)
@[simp]
theorem
bilin_form.lin_mul_lin_comp_left
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M]
{f g : M →ₗ[R₂] R₂}
(l : M →ₗ[R₂] M) :
(bilin_form.lin_mul_lin f g).comp_left l = bilin_form.lin_mul_lin (f.comp l) g
@[simp]
theorem
bilin_form.lin_mul_lin_comp_right
{M : Type v}
[add_comm_group M]
{R₂ : Type u_1}
[comm_ring R₂]
[module R₂ M]
{f g : M →ₗ[R₂] R₂}
(r : M →ₗ[R₂] M) :
(bilin_form.lin_mul_lin f g).comp_right r = bilin_form.lin_mul_lin f (g.comp r)
def
bilin_form.is_ortho
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M] :
bilin_form R M → M → M → Prop
The proposition that two elements of a bilinear form space are orthogonal
theorem
bilin_form.ortho_zero
{R : Type u}
{M : Type v}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(x : M) :
B.is_ortho 0 x
theorem
bilin_form.ortho_smul_left
{M : Type v}
[add_comm_group M]
{R₃ : Type u_1}
[domain R₃]
[module R₃ M]
{G : bilin_form R₃ M}
{x y : M}
{a : R₃} :
theorem
bilin_form.ortho_smul_right
{M : Type v}
[add_comm_group M]
{R₃ : Type u_1}
[domain R₃]
[module R₃ M]
{G : bilin_form R₃ M}
{x y : M}
{a : R₃} :
def
matrix.to_bilin_formₗ
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n] :
matrix n n R →ₗ[R] bilin_form R (n → R)
The linear map from matrix n n R to bilinear forms on n → R.
Equations
- matrix.to_bilin_formₗ = {to_fun := λ (M : matrix n n R), {bilin := λ (v w : n → R), ((matrix.row v).mul M).mul (matrix.col w) punit.star punit.star, bilin_add_left := _, bilin_smul_left := _, bilin_add_right := _, bilin_smul_right := _}, map_add' := _, map_smul' := _}
def
matrix.to_bilin_form
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n] :
matrix n n R → bilin_form R (n → R)
The map from matrix n n R to bilinear forms on n → R.
Equations
theorem
matrix.to_bilin_form_apply
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
(M : matrix n n R)
(v w : n → R) :
⇑(M.to_bilin_form) v w = ((matrix.row v).mul M).mul (matrix.col w) punit.star punit.star
def
bilin_form.to_matrixₗ
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n] :
bilin_form R (n → R) →ₗ[R] matrix n n R
The linear map from bilinear forms on n → R to matrix n n R.
def
bilin_form.to_matrix
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n] :
bilin_form R (n → R) → matrix n n R
The map from bilinear forms on n → R to matrix n n R.
Equations
theorem
bilin_form.to_matrix_apply
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n]
(B : bilin_form R (n → R))
(i j : n) :
theorem
bilin_form.to_matrix_smul
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n]
(B : bilin_form R (n → R))
(x : R) :
theorem
bilin_form.to_matrix_comp
{R : Type u}
[comm_ring R]
{n : Type u_1}
{o : Type u_2}
[fintype n]
[fintype o]
[decidable_eq n]
[decidable_eq o]
(B : bilin_form R (n → R))
(l r : (o → R) →ₗ[R] n → R) :
theorem
bilin_form.to_matrix_comp_left
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n]
(B : bilin_form R (n → R))
(f : (n → R) →ₗ[R] n → R) :
theorem
bilin_form.to_matrix_comp_right
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n]
(B : bilin_form R (n → R))
(f : (n → R) →ₗ[R] n → R) :
theorem
bilin_form.mul_to_matrix_mul
{R : Type u}
[comm_ring R]
{n : Type u_1}
{o : Type u_2}
[fintype n]
[fintype o]
[decidable_eq n]
[decidable_eq o]
(B : bilin_form R (n → R))
(M : matrix o n R)
(N : matrix n o R) :
theorem
bilin_form.mul_to_matrix
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n]
(B : bilin_form R (n → R))
(M : matrix n n R) :
theorem
bilin_form.to_matrix_mul
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n]
(B : bilin_form R (n → R))
(M : matrix n n R) :
@[simp]
theorem
to_matrix_to_bilin_form
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n]
(B : bilin_form R (n → R)) :
B.to_matrix.to_bilin_form = B
@[simp]
theorem
to_bilin_form_to_matrix
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n]
(M : matrix n n R) :
M.to_bilin_form.to_matrix = M
def
bilin_form_equiv_matrix
{R : Type u}
[comm_ring R]
{n : Type u_1}
[fintype n]
[decidable_eq n] :
bilin_form R (n → R) ≃ₗ[R] matrix n n R
Bilinear forms are linearly equivalent to matrices.
Equations
- bilin_form_equiv_matrix = {to_fun := bilin_form.to_matrixₗ.to_fun, map_add' := _, map_smul' := _, inv_fun := matrix.to_bilin_form _inst_2, left_inv := _, right_inv := _}
def
refl_bilin_form.is_refl
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M] :
bilin_form R M → Prop
The proposition that a bilinear form is reflexive
theorem
refl_bilin_form.eq_zero
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(H : refl_bilin_form.is_refl B)
{x y : M} :
theorem
refl_bilin_form.ortho_sym
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(H : refl_bilin_form.is_refl B)
{x y : M} :
def
sym_bilin_form.is_sym
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M] :
bilin_form R M → Prop
The proposition that a bilinear form is symmetric
Equations
- sym_bilin_form.is_sym B = ∀ (x y : M), ⇑B x y = ⇑B y x
theorem
sym_bilin_form.sym
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(H : sym_bilin_form.is_sym B)
(x y : M) :
theorem
sym_bilin_form.is_refl
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M} :
theorem
sym_bilin_form.ortho_sym
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(H : sym_bilin_form.is_sym B)
{x y : M} :
def
alt_bilin_form.is_alt
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M] :
bilin_form R M → Prop
The proposition that a bilinear form is alternating
Equations
- alt_bilin_form.is_alt B = ∀ (x : M), ⇑B x x = 0
theorem
alt_bilin_form.self_eq_zero
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(H : alt_bilin_form.is_alt B)
(x : M) :
theorem
alt_bilin_form.neg
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{B : bilin_form R M}
(H : alt_bilin_form.is_alt B)
(x y : M) :
def
bilin_form.is_adjoint_pair
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{M₂ : Type w}
[add_comm_group M₂]
[module R M₂] :
bilin_form R M → bilin_form R M₂ → (M →ₗ[R] M₂) → (M₂ →ₗ[R] M) → Prop
Given a pair of modules equipped with bilinear forms, this is the condition for a pair of maps between them to be mutually adjoint.
theorem
bilin_form.is_adjoint_pair.eq
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{M₂ : Type w}
[add_comm_group M₂]
[module R M₂]
{B : bilin_form R M}
{B₂ : bilin_form R M₂}
{f : M →ₗ[R] M₂}
{g : M₂ →ₗ[R] M}
(h : B.is_adjoint_pair B₂ f g)
{x : M}
{y : M₂} :
theorem
bilin_form.is_adjoint_pair_iff_comp_left_eq_comp_right
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{B B' : bilin_form R M}
(f g : module.End R M) :
B.is_adjoint_pair B' f g ↔ B'.comp_left f = B.comp_right g
theorem
bilin_form.is_adjoint_pair_zero
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{M₂ : Type w}
[add_comm_group M₂]
[module R M₂]
{B : bilin_form R M}
{B₂ : bilin_form R M₂} :
B.is_adjoint_pair B₂ 0 0
theorem
bilin_form.is_adjoint_pair_id
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{B : bilin_form R M} :
B.is_adjoint_pair B 1 1
theorem
bilin_form.is_adjoint_pair.add
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{M₂ : Type w}
[add_comm_group M₂]
[module R M₂]
{B : bilin_form R M}
{B₂ : bilin_form R M₂}
{f f' : M →ₗ[R] M₂}
{g g' : M₂ →ₗ[R] M} :
B.is_adjoint_pair B₂ f g → B.is_adjoint_pair B₂ f' g' → B.is_adjoint_pair B₂ (f + f') (g + g')
theorem
bilin_form.is_adjoint_pair.sub
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{M₂ : Type w}
[add_comm_group M₂]
[module R M₂]
{B : bilin_form R M}
{B₂ : bilin_form R M₂}
{f f' : M →ₗ[R] M₂}
{g g' : M₂ →ₗ[R] M} :
B.is_adjoint_pair B₂ f g → B.is_adjoint_pair B₂ f' g' → B.is_adjoint_pair B₂ (f - f') (g - g')
theorem
bilin_form.is_adjoint_pair.smul
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{M₂ : Type w}
[add_comm_group M₂]
[module R M₂]
{B : bilin_form R M}
{B₂ : bilin_form R M₂}
{f : M →ₗ[R] M₂}
{g : M₂ →ₗ[R] M}
(c : R) :
B.is_adjoint_pair B₂ f g → B.is_adjoint_pair B₂ (c • f) (c • g)
theorem
bilin_form.is_adjoint_pair.comp
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{M₂ : Type w}
[add_comm_group M₂]
[module R M₂]
{B : bilin_form R M}
{B₂ : bilin_form R M₂}
{f : M →ₗ[R] M₂}
{g : M₂ →ₗ[R] M}
{M₃ : Type v}
[add_comm_group M₃]
[module R M₃]
{B₃ : bilin_form R M₃}
{f' : M₂ →ₗ[R] M₃}
{g' : M₃ →ₗ[R] M₂} :
B.is_adjoint_pair B₂ f g → B₂.is_adjoint_pair B₃ f' g' → B.is_adjoint_pair B₃ (f'.comp f) (g.comp g')
theorem
bilin_form.is_adjoint_pair.mul
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{B : bilin_form R M}
{f g f' g' : module.End R M} :
B.is_adjoint_pair B f g → B.is_adjoint_pair B f' g' → B.is_adjoint_pair B (f * f') (g' * g)
def
bilin_form.is_pair_self_adjoint
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M] :
bilin_form R M → bilin_form R M → module.End R M → Prop
The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms on the underlying module. In the case that these two forms are identical, this is the usual concept of self adjointness. In the case that one of the forms is the negation of the other, this is the usual concept of skew adjointness.
Equations
- B.is_pair_self_adjoint B' f = B.is_adjoint_pair B' f f
def
bilin_form.is_pair_self_adjoint_submodule
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M] :
bilin_form R M → bilin_form R M → submodule R (module.End R M)
The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms.
Equations
- B.is_pair_self_adjoint_submodule B' = {carrier := {f : module.End R M | B.is_pair_self_adjoint B' f}, zero_mem' := _, add_mem' := _, smul_mem' := _}
@[simp]
theorem
bilin_form.mem_is_pair_self_adjoint_submodule
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
(B B' : bilin_form R M)
(f : module.End R M) :
f ∈ B.is_pair_self_adjoint_submodule B' ↔ B.is_pair_self_adjoint B' f
theorem
bilin_form.is_pair_self_adjoint_equiv
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{M₂ : Type w}
[add_comm_group M₂]
[module R M₂]
(B B' : bilin_form R M)
(e : M₂ ≃ₗ[R] M)
(f : module.End R M) :
def
bilin_form.is_self_adjoint
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M] :
bilin_form R M → module.End R M → Prop
An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an adjoint for itself.
Equations
- B.is_self_adjoint f = B.is_adjoint_pair B f f
def
bilin_form.is_skew_adjoint
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M] :
bilin_form R M → module.End R M → Prop
An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation serves as an adjoint.
Equations
- B.is_skew_adjoint f = B.is_adjoint_pair B f (-f)
theorem
bilin_form.is_skew_adjoint_iff_neg_self_adjoint
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
(B : bilin_form R M)
(f : module.End R M) :
B.is_skew_adjoint f ↔ (-B).is_adjoint_pair B f f
def
bilin_form.self_adjoint_submodule
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M] :
bilin_form R M → submodule R (module.End R M)
The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Jordan subalgebra.)
Equations
@[simp]
theorem
bilin_form.mem_self_adjoint_submodule
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
(B : bilin_form R M)
(f : module.End R M) :
f ∈ B.self_adjoint_submodule ↔ B.is_self_adjoint f
def
bilin_form.skew_adjoint_submodule
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M] :
bilin_form R M → submodule R (module.End R M)
The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Lie subalgebra.)
Equations
@[simp]
theorem
bilin_form.mem_skew_adjoint_submodule
{R : Type u}
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
(B : bilin_form R M)
(f : module.End R M) :
f ∈ B.skew_adjoint_submodule ↔ B.is_skew_adjoint f
The condition for the square matrices A, B to be an adjoint pair with respect to the square
matrices J, J₂.
The condition for a square matrix A to be self-adjoint with respect to the square matrix
J.
Equations
- J.is_self_adjoint A = J.is_adjoint_pair J A A
The condition for a square matrix A to be skew-adjoint with respect to the square matrix
J.
Equations
- J.is_skew_adjoint A = J.is_adjoint_pair J A (-A)
@[simp]
theorem
matrix_is_adjoint_pair_bilin_form
{R : Type u}
[comm_ring R]
{n : Type w}
[fintype n]
(J J₂ A B : matrix n n R) :
J.to_bilin_form.is_adjoint_pair J₂.to_bilin_form A.to_lin B.to_lin ↔ J.is_adjoint_pair J₂ A B
theorem
matrix.is_adjoint_pair_equiv
{R : Type u}
[comm_ring R]
{n : Type w}
[fintype n]
(J A B : matrix n n R)
[decidable_eq n]
(P : matrix n n R) :
def
pair_self_adjoint_matrices_submodule
{R : Type u}
[comm_ring R]
{n : Type w}
[fintype n]
(J J₂ : matrix n n R)
[decidable_eq n] :
The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to
given matrices J, J₂.
@[simp]
theorem
mem_pair_self_adjoint_matrices_submodule
{R : Type u}
[comm_ring R]
{n : Type w}
[fintype n]
(J J₂ A : matrix n n R)
[decidable_eq n] :
A ∈ pair_self_adjoint_matrices_submodule J J₂ ↔ J.is_adjoint_pair J₂ A A
def
self_adjoint_matrices_submodule
{R : Type u}
[comm_ring R]
{n : Type w}
[fintype n]
(J : matrix n n R)
[decidable_eq n] :
The submodule of self-adjoint matrices with respect to the bilinear form corresponding to
the matrix J.
Equations
@[simp]
theorem
mem_self_adjoint_matrices_submodule
{R : Type u}
[comm_ring R]
{n : Type w}
[fintype n]
(J A : matrix n n R)
[decidable_eq n] :
def
skew_adjoint_matrices_submodule
{R : Type u}
[comm_ring R]
{n : Type w}
[fintype n]
(J : matrix n n R)
[decidable_eq n] :
The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to
the matrix J.
Equations
@[simp]
theorem
mem_skew_adjoint_matrices_submodule
{R : Type u}
[comm_ring R]
{n : Type w}
[fintype n]
(J A : matrix n n R)
[decidable_eq n] :