# Sesquilinear maps #

This file provides properties about sesquilinear maps and forms. The maps considered are of the form `M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M`, where `I₁ : R₁ →+* R` and `I₂ : R₂ →+* R` are ring homomorphisms and `M₁` is a module over `R₁`, `M₂` is a module over `R₂` and `M` is a module over `R`. Sesquilinear forms are the special case that `M₁ = M₂`, `M = R₁ = R₂ = R`, and `I₁ = RingHom.id R`. Taking additionally `I₂ = RingHom.id R`, then one obtains bilinear forms.

Sesquilinear maps are a special case of the bilinear maps defined in `BilinearMap.lean`, and many basic lemmas about construction and elementary calculations are found there.

## Main declarations #

- `IsOrtho`: states that two vectors are orthogonal with respect to a sesquilinear map
- `IsSymm`, `IsAlt`: states that a sesquilinear form is symmetric and alternating, respectively
- `orthogonalBilin` provides the orthogonal complement with respect to a sesquilinear form

## References #

- https://en.wikipedia.org/wiki/Sesquilinear_form#Over_arbitrary_rings

## Tags #

Sesquilinear form, Sesquilinear map

### Orthogonal vectors #

source
def LinearMap.IsOrtho {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid M] [Module R M] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) (x : M₁) (y : M₂) :
Prop

The proposition that two elements of a sesquilinear map space are orthogonal

Equations

- B.IsOrtho x y = ((B x) y = 0)

Instances For

source
theorem LinearMap.isOrtho_def {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid M] [Module R M] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} {x : M₁} {y : M₂} :
B.IsOrtho x y ↔ (B x) y = 0
source
theorem LinearMap.isOrtho_zero_left {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid M] [Module R M] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) (x : M₂) :
B.IsOrtho 0 x
source
theorem LinearMap.isOrtho_zero_right {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid M] [Module R M] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) (x : M₁) :
B.IsOrtho x 0
source
theorem LinearMap.isOrtho_flip {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M] [Module R M] {I₁ I₁' : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M} {x y : M₁} :
B.IsOrtho x y ↔ B.flip.IsOrtho y x
source
def LinearMap.IsOrthoᵢ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M] [Module R M] {I₁ I₁' : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M) (v : n → M₁) :
Prop

A set of vectors `v` is orthogonal with respect to some bilinear map `B` if and only if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two elements, use `BilinForm.isOrtho`

Equations

- B.IsOrthoᵢ v = Pairwise (Function.onFun B.IsOrtho v)

Instances For

source
theorem LinearMap.isOrthoᵢ_def {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M] [Module R M] {I₁ I₁' : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M} {v : n → M₁} :
B.IsOrthoᵢ v ↔ ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0
source
theorem LinearMap.isOrthoᵢ_flip {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M] [Module R M] {I₁ I₁' : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M) {v : n → M₁} :
B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v
source
theorem LinearMap.ortho_smul_left {K : Type u_13} {K₁ : Type u_14} {K₂ : Type u_15} {V : Type u_16} {V₁ : Type u_17} {V₂ : Type u_18} [Field K] [AddCommGroup V] [Module K V] [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] [Field K₂] [AddCommGroup V₂] [Module K₂ V₂] {I₁ : K₁ →+* K} {I₂ : K₂ →+* K} {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V} {x : V₁} {y : V₂} {a : K₁} (ha : a ≠ 0) :
B.IsOrtho x y ↔ B.IsOrtho (a • x) y
source
theorem LinearMap.ortho_smul_right {K : Type u_13} {K₁ : Type u_14} {K₂ : Type u_15} {V : Type u_16} {V₁ : Type u_17} {V₂ : Type u_18} [Field K] [AddCommGroup V] [Module K V] [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] [Field K₂] [AddCommGroup V₂] [Module K₂ V₂] {I₁ : K₁ →+* K} {I₂ : K₂ →+* K} {B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V} {x : V₁} {y : V₂} {a : K₂} {ha : a ≠ 0} :
B.IsOrtho x y ↔ B.IsOrtho x (a • y)
source
theorem LinearMap.linearIndependent_of_isOrthoᵢ {K : Type u_13} {K₁ : Type u_14} {V : Type u_16} {V₁ : Type u_17} {n : Type u_19} [Field K] [AddCommGroup V] [Module K V] [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] {I₁ I₁' : K₁ →+* K} {B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V} {v : n → V₁} (hv₁ : B.IsOrthoᵢ v) (hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)) :
LinearIndependent K₁ v

A set of orthogonal vectors `v` with respect to some sesquilinear map `B` is linearly independent if for all `i`, `B (v i) (v i) ≠ 0`.

### Reflexive bilinear maps #

source
def LinearMap.IsRefl {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M) :
Prop

The proposition that a sesquilinear map is reflexive

Equations

- B.IsRefl = ∀ (x y : M₁), (B x) y = 0 → (B y) x = 0

Instances For

source
theorem LinearMap.IsRefl.eq_zero {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsRefl) {x y : M₁} :
(B x) y = 0 → (B y) x = 0
source
theorem LinearMap.IsRefl.eq_iff {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsRefl) {x y : M₁} :
(B x) y = 0 ↔ (B y) x = 0
source
theorem LinearMap.IsRefl.ortho_comm {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsRefl) {x y : M₁} :
B.IsOrtho x y ↔ B.IsOrtho y x
source
theorem LinearMap.IsRefl.domRestrict {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsRefl) (p : Submodule R₁ M₁) :
(B.domRestrict₁₂ p p).IsRefl
source
@[simp]
theorem LinearMap.IsRefl.flip_isRefl_iff {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} :
B.flip.IsRefl ↔ B.IsRefl
source
theorem LinearMap.IsRefl.ker_flip_eq_bot {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsRefl) (h : ker B = ⊥) :
ker B.flip = ⊥
source
theorem LinearMap.IsRefl.ker_eq_bot_iff_ker_flip_eq_bot {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsRefl) :
ker B = ⊥ ↔ ker B.flip = ⊥

### Symmetric bilinear forms #

source
structure LinearMap.IsSymm {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} (B : M →ₛₗ[I] M →ₗ[R] R) :
Prop

The proposition that a sesquilinear form is symmetric

- eq (x y : M) : I ((B x) y) = (B y) x

Instances For

source
theorem LinearMap.isSymm_def {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R} :
B.IsSymm ↔ ∀ (x y : M), I ((B x) y) = (B y) x
source
theorem LinearMap.IsSymm.isRefl {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R} (H : B.IsSymm) :
B.IsRefl
source
theorem LinearMap.IsSymm.ortho_comm {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R} (H : B.IsSymm) {x y : M} :
B.IsOrtho x y ↔ B.IsOrtho y x
source
theorem LinearMap.IsSymm.domRestrict {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R} (H : B.IsSymm) (p : Submodule R M) :
(B.domRestrict₁₂ p p).IsSymm
source
@[simp]
theorem LinearMap.isSymm_zero {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} :
IsSymm 0
source
theorem LinearMap.IsSymm.add {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I : R →+* R} {B C : M →ₛₗ[I] M →ₗ[R] R} (hB : B.IsSymm) (hC : C.IsSymm) :
(B + C).IsSymm
source
theorem LinearMap.BilinMap.isSymm_iff_eq_flip {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_20} [AddCommMonoid N] [Module R N] {B : LinearMap.BilinMap R M N} :
(∀ (x y : M), (B x) y = (B y) x) ↔ B = flip B
source
theorem LinearMap.isSymm_iff_eq_flip {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :
IsSymm B ↔ B = flip B

### Positive semidefinite sesquilinear forms #

source
structure LinearMap.IsNonneg {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ I₂ : R →+* R} [LE R] (B : M →ₛₗ[I₁] M →ₛₗ[I₂] R) :
Prop

A sesquilinear form `B` is nonnegative if for any `x` we have `0 ≤ B x x`.

- nonneg (x : M) : 0 ≤ (B x) x

Instances For

source
theorem LinearMap.isNonneg_def {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ I₂ : R →+* R} [LE R] {B : M →ₛₗ[I₁] M →ₛₗ[I₂] R} :
B.IsNonneg ↔ ∀ (x : M), 0 ≤ (B x) x
source
@[simp]
theorem LinearMap.isNonneg_zero {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ I₂ : R →+* R} [Preorder R] :
IsNonneg 0
source
theorem LinearMap.IsNonneg.add {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ I₂ : R →+* R} [Preorder R] [AddLeftMono R] {B C : M →ₛₗ[I₁] M →ₛₗ[I₂] R} (hB : B.IsNonneg) (hC : C.IsNonneg) :
(B + C).IsNonneg
source
theorem LinearMap.IsNonneg.smul {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ I₂ : R →+* R} [Preorder R] [PosMulMono R] {B : M →ₛₗ[I₁] M →ₛₗ[I₂] R} {c : R} (hB : B.IsNonneg) (hc : 0 ≤ c) :
(c • B).IsNonneg
source
structure LinearMap.IsPosSemidef {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ : R →+* R} [LE R] (B : M →ₛₗ[I₁] M →ₗ[R] R) extends B.IsSymm, B.IsNonneg :
Prop

A sesquilinear form `B` is positive semidefinite if it is symmetric and nonnegative.

- eq (x y : M) : I₁ ((B x) y) = (B y) x
- nonneg (x : M) : 0 ≤ (B x) x

Instances For

source
theorem LinearMap.isPosSemidef_def {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ : R →+* R} [LE R] {B : M →ₛₗ[I₁] M →ₗ[R] R} :
B.IsPosSemidef ↔ B.IsSymm ∧ B.IsNonneg
source
@[simp]
theorem LinearMap.isPosSemidef_zero {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ : R →+* R} [Preorder R] :
IsPosSemidef 0
source
theorem LinearMap.IsPosSemidef.add {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] {I₁ : R →+* R} [Preorder R] [AddLeftMono R] {B C : M →ₛₗ[I₁] M →ₗ[R] R} (hB : B.IsPosSemidef) (hC : C.IsPosSemidef) :
(B + C).IsPosSemidef

### Alternating bilinear maps #

source
def LinearMap.IsAlt {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M) :
Prop

The proposition that a sesquilinear map is alternating

Equations

- B.IsAlt = ∀ (x : M₁), (B x) x = 0

Instances For

source
theorem LinearMap.IsAlt.self_eq_zero {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsAlt) (x : M₁) :
(B x) x = 0
source
theorem LinearMap.IsAlt.eq_of_add_add_eq_zero {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsAlt) [IsCancelAdd M] {a b c : M₁} (hAdd : a + b + c = 0) :
(B a) b = (B b) c
source
theorem LinearMap.IsAlt.neg {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommGroup M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsAlt) (x y : M₁) :
-(B x) y = (B y) x
source
theorem LinearMap.IsAlt.isRefl {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommGroup M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsAlt) :
B.IsRefl
source
theorem LinearMap.IsAlt.ortho_comm {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommGroup M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (H : B.IsAlt) {x y : M₁} :
B.IsOrtho x y ↔ B.IsOrtho y x
source
theorem LinearMap.isAlt_iff_eq_neg_flip {R : Type u_1} {R₁ : Type u_2} {M₁ : Type u_6} [CommRing R] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] {I : R₁ →+* R} [NoZeroDivisors R] [CharZero R] {B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R} :
B.IsAlt ↔ B = -B.flip

### The orthogonal complement #

source
def Submodule.orthogonalBilin {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] [AddCommGroup M] [Module R M] {I₁ I₂ : R₁ →+* R} (N : Submodule R₁ M₁) (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M) :
Submodule R₁ M₁

The orthogonal complement of a submodule `N` with respect to some bilinear map 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 maps 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.

Equations

- N.orthogonalBilin B = { carrier := {m : M₁ | ∀ n ∈ N, B.IsOrtho n m}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source
@[simp]
theorem Submodule.mem_orthogonalBilin_iff {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] [AddCommGroup M] [Module R M] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} {N : Submodule R₁ M₁} {m : M₁} :
m ∈ N.orthogonalBilin B ↔ ∀ n ∈ N, B.IsOrtho n m
source
theorem Submodule.orthogonalBilin_le {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] [AddCommGroup M] [Module R M] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} {N L : Submodule R₁ M₁} (h : N ≤ L) :
L.orthogonalBilin B ≤ N.orthogonalBilin B
source
theorem Submodule.le_orthogonalBilin_orthogonalBilin {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] [AddCommGroup M] [Module R M] {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} {N : Submodule R₁ M₁} (b : B.IsRefl) :
N ≤ (N.orthogonalBilin B).orthogonalBilin B
source
theorem LinearMap.span_singleton_inf_orthogonal_eq_bot {K : Type u_13} {K₁ : Type u_14} {V₁ : Type u_17} {V₂ : Type u_18} [Field K] [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] [AddCommGroup V₂] [Module K V₂] {J₁ J₁' : K₁ →+* K} (B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂) (x : V₁) (hx : ¬B.IsOrtho x x) :
Submodule.span K₁ {x} ⊓ (Submodule.span K₁ {x}).orthogonalBilin B = ⊥
source
theorem LinearMap.orthogonal_span_singleton_eq_to_lin_ker {K : Type u_13} {V : Type u_16} {V₂ : Type u_18} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {J : K →+* K} {B : V →ₗ[K] V →ₛₗ[J] V₂} (x : V) :
(Submodule.span K {x}).orthogonalBilin B = ker (B x)
source
theorem LinearMap.span_singleton_sup_orthogonal_eq_top {K : Type u_13} {V : Type u_16} [Field K] [AddCommGroup V] [Module K V] {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.IsOrtho x x) :
Submodule.span K {x} ⊔ (Submodule.span K {x}).orthogonalBilin B = ⊤
source
theorem LinearMap.isCompl_span_singleton_orthogonal {K : Type u_13} {V : Type u_16} [Field K] [AddCommGroup V] [Module K V] {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.IsOrtho x x) :
IsCompl (Submodule.span K {x}) ((Submodule.span K {x}).orthogonalBilin 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 #

source
def LinearMap.IsAdjointPair {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₃] [Module R M₃] {I : R →+* R} (B : M →ₗ[R] M →ₛₗ[I] M₃) (B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃) (f : M → M₁) (g : M₁ → M) :
Prop

Given a pair of modules equipped with bilinear maps, this is the condition for a pair of maps between them to be mutually adjoint.

Equations

- B.IsAdjointPair B' f g = ∀ (x : M) (y : M₁), (B' (f x)) y = (B x) (g y)

Instances For

source
theorem LinearMap.isAdjointPair_iff_comp_eq_compl₂ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₃] [Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃} {f : M →ₗ[R] M₁} {g : M₁ →ₗ[R] M} :
B.IsAdjointPair B' ⇑f ⇑g ↔ B' ∘ₗ f = B.compl₂ g
source
theorem LinearMap.isAdjointPair_zero {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₃] [Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃} :
B.IsAdjointPair B' 0 0
source
theorem LinearMap.isAdjointPair_id {R : Type u_1} {M : Type u_5} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₃] [Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} :
B.IsAdjointPair B _root_.id _root_.id
source
theorem LinearMap.isAdjointPair_one {R : Type u_1} {M : Type u_5} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₃] [Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} :
B.IsAdjointPair B ⇑1 ⇑1
source
theorem LinearMap.IsAdjointPair.add {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₃] [Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃} {f f' : M → M₁} {g g' : M₁ → M} (h : B.IsAdjointPair B' f g) (h' : B.IsAdjointPair B' f' g') :
B.IsAdjointPair B' (f + f') (g + g')
source
theorem LinearMap.IsAdjointPair.comp {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃} {B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃} {f : M → M₁} {g : M₁ → M} {f' : M₁ → M₂} {g' : M₂ → M₁} (h : B.IsAdjointPair B' f g) (h' : B'.IsAdjointPair B'' f' g') :
B.IsAdjointPair B'' (f' ∘ f) (g ∘ g')
source
theorem LinearMap.IsAdjointPair.mul {R : Type u_1} {M : Type u_5} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₃] [Module R M₃] {I : R →+* R} {B : M →ₗ[R] M →ₛₗ[I] M₃} {f g f' g' : Module.End R M} (h : B.IsAdjointPair B ⇑f ⇑g) (h' : B.IsAdjointPair B ⇑f' ⇑g') :
B.IsAdjointPair B ⇑(f * f') ⇑(g' * g)
source
theorem LinearMap.IsAdjointPair.sub {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} {B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂} {f f' : M → M₁} {g g' : M₁ → M} (h : B.IsAdjointPair B' f g) (h' : B.IsAdjointPair B' f' g') :
B.IsAdjointPair B' (f - f') (g - g')
source
theorem LinearMap.IsAdjointPair.smul {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} {B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂} {f : M → M₁} {g : M₁ → M} (c : R) (h : B.IsAdjointPair B' f g) :
B.IsAdjointPair B' (c • f) (c • g)
source
def LinearMap.IsOrthogonal {R : Type u_20} {M : Type u_21} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (f : M → M) :
Prop

A linear transformation `f` is orthogonal with respect to a bilinear form `B` if `B` is bi-invariant with respect to `f`.

Equations

- LinearMap.IsOrthogonal B f = ∀ (x y : M), (B (f x)) (f y) = (B x) y

Instances For

source
@[simp]
theorem LinearEquiv.isAdjointPair_symm_iff {R : Type u_20} {M : Type u_21} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M ≃ M} :
LinearMap.IsAdjointPair B B ⇑f ⇑f.symm ↔ LinearMap.IsOrthogonal B ⇑f
source
theorem LinearMap.isOrthogonal_of_forall_apply_same {R : Type u_20} {M : Type u_21} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {F : Type u_22} [FunLike F M M] [LinearMapClass F R M M] (f : F) (h : IsLeftRegular 2) (hB : IsSymm B) (hf : ∀ (x : M), (B (f x)) (f x) = (B x) x) :
IsOrthogonal B ⇑f

### Self-adjoint pairs #

source
def LinearMap.IsPairSelfAdjoint {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] {I : R →+* R} (B F : M →ₗ[R] M →ₛₗ[I] M₁) (f : M → M) :
Prop

The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear maps on the underlying module. In the case that these two maps are identical, this is the usual concept of self adjointness. In the case that one of the maps is the negation of the other, this is the usual concept of skew adjointness.

Equations

- B.IsPairSelfAdjoint F f = B.IsAdjointPair F f f

Instances For

source
def LinearMap.IsSelfAdjoint {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R M₁] {I : R →+* R} (B : M →ₗ[R] M →ₛₗ[I] M₁) (f : M → M) :
Prop

An endomorphism of a module is self-adjoint with respect to a bilinear map if it serves as an adjoint for itself.

Equations

- B.IsSelfAdjoint f = B.IsAdjointPair B f f

Instances For

source
def LinearMap.isPairSelfAdjointSubmodule {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (B F : M →ₗ[R] M →ₗ[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.isPairSelfAdjointSubmodule F = { carrier := {f : Module.End R M | B.IsPairSelfAdjoint F ⇑f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source
def LinearMap.IsSkewAdjoint {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (B : M →ₗ[R] M →ₗ[R] M₂) (f : M → M) :
Prop

An endomorphism of a module is skew-adjoint with respect to a bilinear map if its negation serves as an adjoint.

Equations

- B.IsSkewAdjoint f = B.IsAdjointPair B f (-f)

Instances For

source
def LinearMap.selfAdjointSubmodule {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (B : M →ₗ[R] M →ₗ[R] M₂) :
Submodule R (Module.End R M)

The set of self-adjoint endomorphisms of a module with bilinear map is a submodule. (In fact it is a Jordan subalgebra.)

Equations

- B.selfAdjointSubmodule = B.isPairSelfAdjointSubmodule B

Instances For

source
def LinearMap.skewAdjointSubmodule {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (B : M →ₗ[R] M →ₗ[R] M₂) :
Submodule R (Module.End R M)

The set of skew-adjoint endomorphisms of a module with bilinear map is a submodule. (In fact it is a Lie subalgebra.)

Equations

- B.skewAdjointSubmodule = (-B).isPairSelfAdjointSubmodule B

Instances For

source
@[simp]
theorem LinearMap.mem_isPairSelfAdjointSubmodule {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {B F : M →ₗ[R] M →ₗ[R] M₂} (f : Module.End R M) :
f ∈ B.isPairSelfAdjointSubmodule F ↔ B.IsPairSelfAdjoint F ⇑f
source
theorem LinearMap.isPairSelfAdjoint_equiv {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] {B F : M →ₗ[R] M →ₗ[R] M₂} (e : M₁ ≃ₗ[R] M) (f : Module.End R M) :
B.IsPairSelfAdjoint F ⇑f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) ⇑(e.symm.conj f)
source
theorem LinearMap.isSkewAdjoint_iff_neg_self_adjoint {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} (f : M → M) :
B.IsSkewAdjoint f ↔ (-B).IsAdjointPair B f f
source
@[simp]
theorem LinearMap.mem_selfAdjointSubmodule {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} (f : Module.End R M) :
f ∈ B.selfAdjointSubmodule ↔ B.IsSelfAdjoint ⇑f
source
@[simp]
theorem LinearMap.mem_skewAdjointSubmodule {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {B : M →ₗ[R] M →ₗ[R] M₂} (f : Module.End R M) :
f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint ⇑f

### Nondegenerate bilinear maps #

source
def LinearMap.SeparatingLeft {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) :
Prop

A bilinear map 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`.

Equations

- B.SeparatingLeft = ∀ (x : M₁), (∀ (y : M₂), (B x) y = 0) → x = 0

Instances For

source
theorem LinearMap.not_separatingLeft_zero {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} (M₁ : Type u_6) (M₂ : Type u_7) [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] (I₁ : R₁ →+* R) (I₂ : R₂ →+* R) [Nontrivial M₁] :
¬SeparatingLeft 0

In a non-trivial module, zero is not non-degenerate.

source
theorem LinearMap.SeparatingLeft.ne_zero {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} [Nontrivial M₁] {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} (h : B.SeparatingLeft) :
B ≠ 0
source
theorem LinearMap.SeparatingLeft.congr {R : Type u_1} {M : Type u_5} {Mₗ₁ : Type u_9} {Mₗ₁' : Type u_10} {Mₗ₂ : Type u_11} {Mₗ₂' : Type u_12} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid Mₗ₁] [AddCommMonoid Mₗ₂] [AddCommMonoid Mₗ₁'] [AddCommMonoid Mₗ₂'] [Module R Mₗ₁] [Module R Mₗ₂] [Module R Mₗ₁'] [Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M} (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂') (h : B.SeparatingLeft) :
((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft
source
@[simp]
theorem LinearMap.separatingLeft_congr_iff {R : Type u_1} {M : Type u_5} {Mₗ₁ : Type u_9} {Mₗ₁' : Type u_10} {Mₗ₂ : Type u_11} {Mₗ₂' : Type u_12} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid Mₗ₁] [AddCommMonoid Mₗ₂] [AddCommMonoid Mₗ₁'] [AddCommMonoid Mₗ₂'] [Module R Mₗ₁] [Module R Mₗ₂] [Module R Mₗ₁'] [Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M} (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂') :
((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft ↔ B.SeparatingLeft
source
def LinearMap.SeparatingRight {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) :
Prop

A bilinear map 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`.

Equations

- B.SeparatingRight = ∀ (y : M₂), (∀ (x : M₁), (B x) y = 0) → y = 0

Instances For

source
def LinearMap.Nondegenerate {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) :
Prop

A bilinear map is called non-degenerate if it is left-separating and right-separating.

Equations

- B.Nondegenerate = (B.SeparatingLeft ∧ B.SeparatingRight)

Instances For

source
@[simp]
theorem LinearMap.flip_separatingRight {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
B.flip.SeparatingRight ↔ B.SeparatingLeft
source
@[simp]
theorem LinearMap.flip_separatingLeft {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
B.flip.SeparatingLeft ↔ B.SeparatingRight
source
@[simp]
theorem LinearMap.flip_nondegenerate {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
B.flip.Nondegenerate ↔ B.Nondegenerate
source
theorem LinearMap.separatingLeft_iff_linear_nontrivial {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
B.SeparatingLeft ↔ ∀ (x : M₁), B x = 0 → x = 0
source
theorem LinearMap.separatingRight_iff_linear_flip_nontrivial {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
B.SeparatingRight ↔ ∀ (y : M₂), B.flip y = 0 → y = 0
source
theorem LinearMap.separatingLeft_iff_ker_eq_bot {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
B.SeparatingLeft ↔ ker B = ⊥

A bilinear map is left-separating if and only if it has a trivial kernel.

source
theorem LinearMap.separatingRight_iff_flip_ker_eq_bot {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
B.SeparatingRight ↔ ker B.flip = ⊥

A bilinear map is right-separating if and only if its flip has a trivial kernel.

source
theorem LinearMap.IsRefl.nondegenerate_iff_separatingLeft {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} (hB : B.IsRefl) :
B.Nondegenerate ↔ B.SeparatingLeft
source
theorem LinearMap.IsRefl.nondegenerate_iff_separatingRight {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} (hB : B.IsRefl) :
B.Nondegenerate ↔ B.SeparatingRight
source
theorem LinearMap.disjoint_ker_of_nondegenerate_restrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} {W : Submodule R M} (hW : (B.domRestrict₁₂ W W).Nondegenerate) :
Disjoint W (ker B)
source
theorem LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker {R : Type u_1} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] {B : M →ₗ[R] M →ₗ[R] R} (hB : B.IsSymm) {W : Submodule R M} (hW : IsCompl W (ker B)) :
(B.domRestrict₁₂ W W).Nondegenerate
source
theorem LinearMap.nondegenerate_restrict_of_disjoint_orthogonal {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} (hB : B.IsRefl) {W : Submodule R M} (hW : Disjoint W (W.orthogonalBilin B)) :
(B.domRestrict₁₂ W W).Nondegenerate

The restriction of a reflexive bilinear map `B` onto a submodule `W` is nondegenerate if `W` has trivial intersection with its orthogonal complement, that is `Disjoint W (W.orthogonalBilin B)`.

source
theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingLeft {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {I I' : R →+* R} [Nontrivial R] {B : M →ₛₗ[I] M →ₛₗ[I'] M₁} {v : Module.Basis n R M} (h : B.IsOrthoᵢ ⇑v) (hB : B.SeparatingLeft) (i : n) :
¬B.IsOrtho (v i) (v i)

An orthogonal basis with respect to a left-separating bilinear map has no self-orthogonal elements.

source
theorem LinearMap.IsOrthoᵢ.not_isOrtho_basis_self_of_separatingRight {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] {I I' : R →+* R} [Nontrivial R] {B : M →ₛₗ[I] M →ₛₗ[I'] M₁} {v : Module.Basis n R M} (h : B.IsOrthoᵢ ⇑v) (hB : B.SeparatingRight) (i : n) :
¬B.IsOrtho (v i) (v i)

An orthogonal basis with respect to a right-separating bilinear map has no self-orthogonal elements.

source
theorem LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] [NoZeroSMulDivisors R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} (v : Module.Basis n R M) (hO : B.IsOrthoᵢ ⇑v) (h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)) :
B.SeparatingLeft

Given an orthogonal basis with respect to a bilinear map, the bilinear map is left-separating if the basis has no elements which are self-orthogonal.

source
theorem LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] [NoZeroSMulDivisors R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} (v : Module.Basis n R M) (hO : B.IsOrthoᵢ ⇑v) (h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)) :
B.SeparatingRight

Given an orthogonal basis with respect to a bilinear map, the bilinear map is right-separating if the basis has no elements which are self-orthogonal.

source
theorem LinearMap.IsOrthoᵢ.nondegenerate_of_not_isOrtho_basis_self {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₁] [Module R M₁] [NoZeroSMulDivisors R M₁] {B : M →ₗ[R] M →ₗ[R] M₁} (v : Module.Basis n R M) (hO : B.IsOrthoᵢ ⇑v) (h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)) :
B.Nondegenerate

Given an orthogonal basis with respect to a bilinear map, the bilinear map is nondegenerate if the basis has no elements which are self-orthogonal.

source
theorem LinearMap.BilinForm.apply_smul_sub_smul_sub_eq {R : Type u_1} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (x y : M) :
(B ((B x) y • x - (B x) x • y)) ((B x) y • x - (B x) x • y) = (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
source
theorem LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hs : ∀ (x : M), 0 ≤ (B x) x) (x y : M) :
(B x) y * (B y) x ≤ (B x) x * (B y) y

The Cauchy-Schwarz inequality for positive semidefinite forms.

source
theorem LinearMap.BilinForm.apply_sq_le_of_symm {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hs : ∀ (x : M), 0 ≤ (B x) x) (hB : IsSymm B) (x y : M) :
(B x) y ^ 2 ≤ (B x) x * (B y) y

The Cauchy-Schwarz inequality for positive semidefinite symmetric forms.

source
theorem LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x) (x y : M) (he : (B x) y * (B y) x = (B x) x * (B y) y) :
¬LinearIndependent R ![x, y]

The equality case of Cauchy-Schwarz.

source
theorem LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) [NoZeroSMulDivisors R M] (hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x) (x y : M) :
(B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Strict Cauchy-Schwarz is equivalent to linear independence for positive definite forms.

source
theorem LinearMap.BilinForm.apply_sq_lt_iff_linearIndependent_of_symm {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) [NoZeroSMulDivisors R M] (hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x) (hB : IsSymm B) (x y : M) :
(B x) y ^ 2 < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Strict Cauchy-Schwarz is equivalent to linear independence for positive definite symmetric forms.

source
theorem LinearMap.BilinForm.apply_apply_same_eq_zero_iff {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hs : ∀ (x : M), 0 ≤ (B x) x) (hB : IsSymm B) {x : M} :
(B x) x = 0 ↔ x ∈ ker B
source
theorem LinearMap.BilinForm.nondegenerate_iff {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hs : ∀ (x : M), 0 ≤ (B x) x) (hB : IsSymm B) :
Nondegenerate B ↔ ∀ (x : M), (B x) x = 0 ↔ x = 0
source
theorem LinearMap.BilinForm.nondegenerate_iff' {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hs : ∀ (x : M), 0 ≤ (B x) x) (hB : IsSymm B) :
Nondegenerate B ↔ ∀ (x : M), x ≠ 0 → 0 < (B x) x

A convenience variant of `LinearMap.BilinForm.nondegenerate_iff` characterising nondegeneracy as positive definiteness.

source
theorem LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker {R : Type u_1} {M : Type u_5} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) (hs : ∀ (x : M), 0 ≤ (B x) x) (hB : IsSymm B) {W : Submodule R M} :
(domRestrict₁₂ B W W).Nondegenerate ↔ Disjoint W (ker B)