Sesquilinear form #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This files provides properties about sesquilinear forms. The maps considered are of the form
M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R, where I₁ : R₁ →+* R and I₂ : R₂ →+* R are ring homomorphisms and
M₁ is a module over R₁ and M₂ is a module over R₂.
Sesquilinear forms are the special case that M₁ = M₂, R₁ = R₂ = R, and I₁ = ring_hom.id R.
Taking additionally I₂ = ring_hom.id R, then one obtains bilinear forms.
These forms are a special case of the bilinear maps defined in bilinear_map.lean and all basic
lemmas about construction and elementary calculations are found there.
Main declarations #
is_ortho: states that two vectors are orthogonal with respect to a sesquilinear formis_symm,is_alt: states that a sesquilinear form is symmetric and alternating, respectivelyorthogonal_bilin: provides the orthogonal complement with respect to sesquilinear form
References #
Tags #
Sesquilinear form,
Orthogonal vectors #
def
linear_map.is_ortho
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
(B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R)
(x : M₁)
(y : M₂) :
Prop
The proposition that two elements of a sesquilinear form space are orthogonal
theorem
linear_map.is_ortho_def
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R}
{x : M₁}
{y : M₂} :
theorem
linear_map.is_ortho_zero_left
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
(B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R)
(x : M₂) :
B.is_ortho 0 x
theorem
linear_map.is_ortho_zero_right
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
(B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R)
(x : M₁) :
B.is_ortho x 0
theorem
linear_map.is_ortho_flip
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₁' : R₁ →+* R}
{B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R}
{x y : M₁} :
def
linear_map.is_Ortho
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
{n : Type u_18}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₁' : R₁ →+* R}
(B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R)
(v : n → M₁) :
Prop
A set of vectors v is orthogonal with respect to some bilinear form B if and only
if for all i ≠ j, B (v i) (v j) = 0. For orthogonality between two elements, use
bilin_form.is_ortho
theorem
linear_map.is_Ortho_flip
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
{n : Type u_18}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₁' : R₁ →+* R}
(B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R)
{v : n → M₁} :
theorem
linear_map.ortho_smul_left
{K : Type u_12}
{K₁ : Type u_13}
{K₂ : Type u_14}
{V₁ : Type u_16}
{V₂ : Type u_17}
[field K]
[field K₁]
[add_comm_group V₁]
[module K₁ V₁]
[field K₂]
[add_comm_group V₂]
[module K₂ V₂]
{I₁ : K₁ →+* K}
{I₂ : K₂ →+* K}
{B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K}
{x : V₁}
{y : V₂}
{a : K₁}
(ha : a ≠ 0) :
theorem
linear_map.ortho_smul_right
{K : Type u_12}
{K₁ : Type u_13}
{K₂ : Type u_14}
{V₁ : Type u_16}
{V₂ : Type u_17}
[field K]
[field K₁]
[add_comm_group V₁]
[module K₁ V₁]
[field K₂]
[add_comm_group V₂]
[module K₂ V₂]
{I₁ : K₁ →+* K}
{I₂ : K₂ →+* K}
{B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] K}
{x : V₁}
{y : V₂}
{a : K₂}
{ha : a ≠ 0} :
theorem
linear_map.linear_independent_of_is_Ortho
{K : Type u_12}
{K₁ : Type u_13}
{V₁ : Type u_16}
{n : Type u_18}
[field K]
[field K₁]
[add_comm_group V₁]
[module K₁ V₁]
{I₁ I₁' : K₁ →+* K}
{B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] K}
{v : n → V₁}
(hv₁ : B.is_Ortho v)
(hv₂ : ∀ (i : n), ¬B.is_ortho (v i) (v i)) :
linear_independent K₁ v
A set of orthogonal vectors v with respect to some sesquilinear form B is linearly
independent if for all i, B (v i) (v i) ≠ 0.
Reflexive bilinear forms #
def
linear_map.is_refl
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
(B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :
Prop
The proposition that a sesquilinear form is reflexive
theorem
linear_map.is_refl.ortho_comm
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
{B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
(H : B.is_refl)
{x y : M₁} :
theorem
linear_map.is_refl.dom_restrict_refl
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
{B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
(H : B.is_refl)
(p : submodule R₁ M₁) :
(B.dom_restrict₁₂ p p).is_refl
@[simp]
theorem
linear_map.is_refl.flip_is_refl_iff
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
{B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R} :
theorem
linear_map.is_refl.ker_flip_eq_bot
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
{B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
(H : B.is_refl)
(h : linear_map.ker B = ⊥) :
linear_map.ker B.flip = ⊥
theorem
linear_map.is_refl.ker_eq_bot_iff_ker_flip_eq_bot
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
{B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
(H : B.is_refl) :
linear_map.ker B = ⊥ ↔ linear_map.ker B.flip = ⊥
Symmetric bilinear forms #
theorem
linear_map.is_symm.is_refl
{R : Type u_1}
{M : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{I : R →+* R}
{B : M →ₛₗ[I] M →ₗ[R] R}
(H : B.is_symm) :
B.is_refl
theorem
linear_map.is_symm.dom_restrict_symm
{R : Type u_1}
{M : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{I : R →+* R}
{B : M →ₛₗ[I] M →ₗ[R] R}
(H : B.is_symm)
(p : submodule R M) :
(B.dom_restrict₁₂ p p).is_symm
theorem
linear_map.is_symm_iff_eq_flip
{R : Type u_1}
{M : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{B : M →ₗ[R] M →ₗ[R] R} :
Alternating bilinear forms #
def
linear_map.is_alt
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_ring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
(B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :
Prop
The proposition that a sesquilinear form is alternating
The orthogonal complement #
def
submodule.orthogonal_bilin
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_ring R]
[comm_ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
(N : submodule R₁ M₁)
(B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) :
submodule R₁ M₁
The orthogonal complement of a submodule N with respect to some bilinear form is the set of
elements x which are orthogonal to all elements of N; i.e., for all y in N, B x y = 0.
Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a
chirality; in addition to this "left" orthogonal complement one could define a "right" orthogonal
complement for which, for all y in N, B y x = 0. This variant definition is not currently
provided in mathlib.
@[simp]
theorem
submodule.orthogonal_bilin_le
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_ring R]
[comm_ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
{B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
{N L : submodule R₁ M₁}
(h : N ≤ L) :
L.orthogonal_bilin B ≤ N.orthogonal_bilin B
theorem
submodule.le_orthogonal_bilin_orthogonal_bilin
{R : Type u_1}
{R₁ : Type u_2}
{M₁ : Type u_6}
[comm_ring R]
[comm_ring R₁]
[add_comm_group M₁]
[module R₁ M₁]
{I₁ I₂ : R₁ →+* R}
{B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
{N : submodule R₁ M₁}
(b : B.is_refl) :
N ≤ (N.orthogonal_bilin B).orthogonal_bilin B
theorem
linear_map.span_singleton_inf_orthogonal_eq_bot
{K : Type u_12}
{K₁ : Type u_13}
{V₁ : Type u_16}
[field K]
[field K₁]
[add_comm_group V₁]
[module K₁ V₁]
{J₁ J₁' : K₁ →+* K}
(B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] K)
(x : V₁)
(hx : ¬B.is_ortho x x) :
submodule.span K₁ {x} ⊓ (submodule.span K₁ {x}).orthogonal_bilin B = ⊥
theorem
linear_map.orthogonal_span_singleton_eq_to_lin_ker
{K : Type u_12}
{V : Type u_15}
[field K]
[add_comm_group V]
[module K V]
{J : K →+* K}
{B : V →ₗ[K] V →ₛₗ[J] K}
(x : V) :
(submodule.span K {x}).orthogonal_bilin B = linear_map.ker (⇑B x)
theorem
linear_map.span_singleton_sup_orthogonal_eq_top
{K : Type u_12}
{V : Type u_15}
[field K]
[add_comm_group V]
[module K V]
{B : V →ₗ[K] V →ₗ[K] K}
{x : V}
(hx : ¬B.is_ortho x x) :
submodule.span K {x} ⊔ (submodule.span K {x}).orthogonal_bilin B = ⊤
theorem
linear_map.is_compl_span_singleton_orthogonal
{K : Type u_12}
{V : Type u_15}
[field K]
[add_comm_group V]
[module K V]
{B : V →ₗ[K] V →ₗ[K] K}
{x : V}
(hx : ¬B.is_ortho x x) :
is_compl (submodule.span K {x}) ((submodule.span K {x}).orthogonal_bilin B)
Given a bilinear form B and some x such that B x x ≠ 0, the span of the singleton of x
is complement to its orthogonal complement.
Adjoint pairs #
def
linear_map.is_adjoint_pair
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₁]
[module R M₁]
{I : R →+* R}
(B : M →ₗ[R] M →ₛₗ[I] R)
(B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R)
(f : M →ₗ[R] M₁)
(g : 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
linear_map.is_adjoint_pair_iff_comp_eq_compl₂
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₁]
[module R M₁]
{I : R →+* R}
{B : M →ₗ[R] M →ₛₗ[I] R}
{B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R}
{f : M →ₗ[R] M₁}
{g : M₁ →ₗ[R] M} :
B.is_adjoint_pair B' f g ↔ B'.comp f = B.compl₂ g
theorem
linear_map.is_adjoint_pair_zero
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₁]
[module R M₁]
{I : R →+* R}
{B : M →ₗ[R] M →ₛₗ[I] R}
{B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R} :
B.is_adjoint_pair B' 0 0
theorem
linear_map.is_adjoint_pair_id
{R : Type u_1}
{M : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{I : R →+* R}
{B : M →ₗ[R] M →ₛₗ[I] R} :
B.is_adjoint_pair B 1 1
theorem
linear_map.is_adjoint_pair.add
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₁]
[module R M₁]
{I : R →+* R}
{B : M →ₗ[R] M →ₛₗ[I] R}
{B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R}
{f f' : M →ₗ[R] M₁}
{g g' : M₁ →ₗ[R] M}
(h : B.is_adjoint_pair B' f g)
(h' : B.is_adjoint_pair B' f' g') :
B.is_adjoint_pair B' (f + f') (g + g')
theorem
linear_map.is_adjoint_pair.comp
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
[add_comm_monoid M₁]
[module R M₁]
[add_comm_monoid M₂]
[module R M₂]
{I : R →+* R}
{B : M →ₗ[R] M →ₛₗ[I] R}
{B' : M₁ →ₗ[R] M₁ →ₛₗ[I] R}
{B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] R}
{f : M →ₗ[R] M₁}
{g : M₁ →ₗ[R] M}
{f' : M₁ →ₗ[R] M₂}
{g' : M₂ →ₗ[R] M₁}
(h : B.is_adjoint_pair B' f g)
(h' : B'.is_adjoint_pair B'' f' g') :
B.is_adjoint_pair B'' (f'.comp f) (g.comp g')
theorem
linear_map.is_adjoint_pair.mul
{R : Type u_1}
{M : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{I : R →+* R}
{B : M →ₗ[R] M →ₛₗ[I] R}
{f g f' g' : module.End R M}
(h : B.is_adjoint_pair B f g)
(h' : B.is_adjoint_pair B f' g') :
B.is_adjoint_pair B (f * f') (g' * g)
theorem
linear_map.is_adjoint_pair.sub
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[comm_ring R]
[add_comm_group M]
[module R M]
[add_comm_group M₁]
[module R M₁]
{B : M →ₗ[R] M →ₗ[R] R}
{B' : M₁ →ₗ[R] M₁ →ₗ[R] R}
{f f' : M →ₗ[R] M₁}
{g g' : M₁ →ₗ[R] M}
(h : B.is_adjoint_pair B' f g)
(h' : B.is_adjoint_pair B' f' g') :
B.is_adjoint_pair B' (f - f') (g - g')
theorem
linear_map.is_adjoint_pair.smul
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[comm_ring R]
[add_comm_group M]
[module R M]
[add_comm_group M₁]
[module R M₁]
{B : M →ₗ[R] M →ₗ[R] R}
{B' : M₁ →ₗ[R] M₁ →ₗ[R] R}
{f : M →ₗ[R] M₁}
{g : M₁ →ₗ[R] M}
(c : R)
(h : B.is_adjoint_pair B' f g) :
B.is_adjoint_pair B' (c • f) (c • g)
Self-adjoint pairs #
def
linear_map.is_pair_self_adjoint
{R : Type u_1}
{M : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{I : R →+* R}
(B F : M →ₗ[R] M →ₛₗ[I] R)
(f : 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 F f = B.is_adjoint_pair F f f
@[protected]
def
linear_map.is_self_adjoint
{R : Type u_1}
{M : Type u_5}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{I : R →+* R}
(B : M →ₗ[R] M →ₛₗ[I] R)
(f : 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
linear_map.is_pair_self_adjoint_submodule
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
(B F : M →ₗ[R] M →ₗ[R] R) :
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 F = {carrier := {f : module.End R M | B.is_pair_self_adjoint F f}, add_mem' := _, zero_mem' := _, smul_mem' := _}
def
linear_map.is_skew_adjoint
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
(B : M →ₗ[R] M →ₗ[R] R)
(f : 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)
def
linear_map.self_adjoint_submodule
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
(B : M →ₗ[R] M →ₗ[R] R) :
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
def
linear_map.skew_adjoint_submodule
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
(B : M →ₗ[R] M →ₗ[R] R) :
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
linear_map.mem_is_pair_self_adjoint_submodule
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
{B F : M →ₗ[R] M →ₗ[R] R}
(f : module.End R M) :
f ∈ B.is_pair_self_adjoint_submodule F ↔ B.is_pair_self_adjoint F f
theorem
linear_map.is_pair_self_adjoint_equiv
{R : Type u_1}
{M : Type u_5}
{M₁ : Type u_6}
[comm_ring R]
[add_comm_group M]
[module R M]
[add_comm_group M₁]
[module R M₁]
{B F : M →ₗ[R] M →ₗ[R] R}
(e : M₁ ≃ₗ[R] M)
(f : module.End R M) :
theorem
linear_map.is_skew_adjoint_iff_neg_self_adjoint
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
{B : M →ₗ[R] M →ₗ[R] R}
(f : module.End R M) :
B.is_skew_adjoint f ↔ (-B).is_adjoint_pair B f f
@[simp]
theorem
linear_map.mem_self_adjoint_submodule
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
{B : M →ₗ[R] M →ₗ[R] R}
(f : module.End R M) :
f ∈ B.self_adjoint_submodule ↔ B.is_self_adjoint f
@[simp]
theorem
linear_map.mem_skew_adjoint_submodule
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
{B : M →ₗ[R] M →ₗ[R] R}
(f : module.End R M) :
f ∈ B.skew_adjoint_submodule ↔ B.is_skew_adjoint f
Nondegenerate bilinear forms #
def
linear_map.separating_left
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
(B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) :
Prop
A bilinear form is called left-separating if
the only element that is left-orthogonal to every other element is 0; i.e.,
for every nonzero x in M₁, there exists y in M₂ with B x y ≠ 0.
theorem
linear_map.not_separating_left_zero
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
(M₁ : Type u_6)
(M₂ : Type u_7)
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
(I₁ : R₁ →+* R)
(I₂ : R₂ →+* R)
[nontrivial M₁] :
In a non-trivial module, zero is not non-degenerate.
theorem
linear_map.separating_left.ne_zero
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
[nontrivial M₁]
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R}
(h : B.separating_left) :
B ≠ 0
theorem
linear_map.separating_left.congr
{R : Type u_1}
{Mₗ₁ : Type u_8}
{Mₗ₁' : Type u_9}
{Mₗ₂ : Type u_10}
{Mₗ₂' : Type u_11}
[comm_semiring R]
[add_comm_monoid Mₗ₁]
[add_comm_monoid Mₗ₂]
[add_comm_monoid Mₗ₁']
[add_comm_monoid Mₗ₂']
[module R Mₗ₁]
[module R Mₗ₂]
[module R Mₗ₁']
[module R Mₗ₂']
{B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R}
(e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁')
(e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂')
(h : B.separating_left) :
(⇑(e₁.arrow_congr (e₂.arrow_congr (linear_equiv.refl R R))) B).separating_left
@[simp]
theorem
linear_map.separating_left_congr_iff
{R : Type u_1}
{Mₗ₁ : Type u_8}
{Mₗ₁' : Type u_9}
{Mₗ₂ : Type u_10}
{Mₗ₂' : Type u_11}
[comm_semiring R]
[add_comm_monoid Mₗ₁]
[add_comm_monoid Mₗ₂]
[add_comm_monoid Mₗ₁']
[add_comm_monoid Mₗ₂']
[module R Mₗ₁]
[module R Mₗ₂]
[module R Mₗ₁']
[module R Mₗ₂']
{B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] R}
(e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁')
(e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂') :
(⇑(e₁.arrow_congr (e₂.arrow_congr (linear_equiv.refl R R))) B).separating_left ↔ B.separating_left
def
linear_map.separating_right
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
(B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) :
Prop
A bilinear form is called right-separating if
the only element that is right-orthogonal to every other element is 0; i.e.,
for every nonzero y in M₂, there exists x in M₁ with B x y ≠ 0.
def
linear_map.nondegenerate
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
(B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) :
Prop
A bilinear form is called non-degenerate if it is left-separating and right-separating.
Equations
- B.nondegenerate = (B.separating_left ∧ B.separating_right)
@[simp]
theorem
linear_map.flip_separating_right
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
@[simp]
theorem
linear_map.flip_separating_left
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
@[simp]
theorem
linear_map.flip_nondegenerate
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
theorem
linear_map.separating_left_iff_linear_nontrivial
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
theorem
linear_map.separating_right_iff_linear_flip_nontrivial
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
theorem
linear_map.separating_left_iff_ker_eq_bot
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
B.separating_left ↔ linear_map.ker B = ⊥
A bilinear form is left-separating if and only if it has a trivial kernel.
theorem
linear_map.separating_right_iff_flip_ker_eq_bot
{R : Type u_1}
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_6}
{M₂ : Type u_7}
[comm_semiring R]
[comm_semiring R₁]
[add_comm_monoid M₁]
[module R₁ M₁]
[comm_semiring R₂]
[add_comm_monoid M₂]
[module R₂ M₂]
{I₁ : R₁ →+* R}
{I₂ : R₂ →+* R}
{B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} :
A bilinear form is right-separating if and only if its flip has a trivial kernel.
theorem
linear_map.is_refl.nondegenerate_of_separating_left
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
{B : M →ₗ[R] M →ₗ[R] R}
(hB : B.is_refl)
(hB' : B.separating_left) :
theorem
linear_map.is_refl.nondegenerate_of_separating_right
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
{B : M →ₗ[R] M →ₗ[R] R}
(hB : B.is_refl)
(hB' : B.separating_right) :
theorem
linear_map.nondegenerate_restrict_of_disjoint_orthogonal
{R : Type u_1}
{M : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
{B : M →ₗ[R] M →ₗ[R] R}
(hB : B.is_refl)
{W : submodule R M}
(hW : disjoint W (W.orthogonal_bilin B)) :
(B.dom_restrict₁₂ W W).nondegenerate
The restriction of a reflexive bilinear form B onto a submodule W is
nondegenerate if W has trivial intersection with its orthogonal complement,
that is disjoint W (W.orthogonal_bilin B).
theorem
linear_map.is_Ortho.not_is_ortho_basis_self_of_separating_left
{R : Type u_1}
{M : Type u_5}
{n : Type u_18}
[comm_ring R]
[add_comm_group M]
[module R M]
{I I' : R →+* R}
[nontrivial R]
{B : M →ₛₗ[I] M →ₛₗ[I'] R}
{v : basis n R M}
(h : B.is_Ortho ⇑v)
(hB : B.separating_left)
(i : n) :
An orthogonal basis with respect to a left-separating bilinear form has no self-orthogonal elements.
theorem
linear_map.is_Ortho.not_is_ortho_basis_self_of_separating_right
{R : Type u_1}
{M : Type u_5}
{n : Type u_18}
[comm_ring R]
[add_comm_group M]
[module R M]
{I I' : R →+* R}
[nontrivial R]
{B : M →ₛₗ[I] M →ₛₗ[I'] R}
{v : basis n R M}
(h : B.is_Ortho ⇑v)
(hB : B.separating_right)
(i : n) :
An orthogonal basis with respect to a right-separating bilinear form has no self-orthogonal elements.
theorem
linear_map.is_Ortho.separating_left_of_not_is_ortho_basis_self
{R : Type u_1}
{M : Type u_5}
{n : Type u_18}
[comm_ring R]
[add_comm_group M]
[module R M]
[no_zero_divisors R]
{B : M →ₗ[R] M →ₗ[R] R}
(v : basis n R M)
(hO : B.is_Ortho ⇑v)
(h : ∀ (i : n), ¬B.is_ortho (⇑v i) (⇑v i)) :
Given an orthogonal basis with respect to a bilinear form, the bilinear form is left-separating if the basis has no elements which are self-orthogonal.
theorem
linear_map.is_Ortho.separating_right_iff_not_is_ortho_basis_self
{R : Type u_1}
{M : Type u_5}
{n : Type u_18}
[comm_ring R]
[add_comm_group M]
[module R M]
[no_zero_divisors R]
{B : M →ₗ[R] M →ₗ[R] R}
(v : basis n R M)
(hO : B.is_Ortho ⇑v)
(h : ∀ (i : n), ¬B.is_ortho (⇑v i) (⇑v i)) :
Given an orthogonal basis with respect to a bilinear form, the bilinear form is right-separating if the basis has no elements which are self-orthogonal.
theorem
linear_map.is_Ortho.nondegenerate_of_not_is_ortho_basis_self
{R : Type u_1}
{M : Type u_5}
{n : Type u_18}
[comm_ring R]
[add_comm_group M]
[module R M]
[no_zero_divisors R]
{B : M →ₗ[R] M →ₗ[R] R}
(v : basis n R M)
(hO : B.is_Ortho ⇑v)
(h : ∀ (i : n), ¬B.is_ortho (⇑v i) (⇑v i)) :
Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate if the basis has no elements which are self-orthogonal.