Orthogonal complement

This file defines the orthogonal submodule of a submodule with respect to a sesqui-blinear map.

Main declarations

• orthogonalBilin provides the orthogonal complement with respect to a sesqui-bilinear map

The orthogonal complement

def Submodule.orthogonalBilin {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) (S : Submodule R₁ 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

• Submodule.orthogonalBilin B S = { carrier := {y : M₂ | ∀ x ∈ S, (B x) y = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Submodule.mem_orthogonalBilin_iff {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} {S : Submodule R₁ M₁} {m : M₂} : m ∈ orthogonalBilin B S ↔ ∀ n ∈ S, (B n) m = 0

theorem Submodule.orthogonalBilin_le {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} {S T : Submodule R₁ M₁} (h : S ≤ T) : orthogonalBilin B T ≤ orthogonalBilin B S

theorem Submodule.le_orthogonalBilin_orthogonalBilin {R : Type u_1} {R₁ : Type u_2} {M : Type u_4} {M₁ : Type u_5} [CommSemiring R] [CommSemiring R₁] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R₁ M₁] {I₁ : R₁ →+* R} {S : Submodule R₁ M₁} {I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M} (b : B.IsRefl) : S ≤ orthogonalBilin B (orthogonalBilin B S)

theorem LinearMap.span_singleton_inf_orthogonal_eq_bot {K : Type u_7} {K₁ : Type u_8} {V₁ : Type u_10} {V₂ : Type u_11} [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 x) x ≠ 0) : K₁ ∙ x ⊓ Submodule.orthogonalBilin B (K₁ ∙ x) = ⊥

theorem LinearMap.orthogonal_span_singleton_eq_to_lin_ker {K : Type u_7} {V : Type u_9} {V₂ : Type u_11} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup V₂] [Module K V₂] {J : K →+* K} {B : V →ₗ[K] V →ₛₗ[J] V₂} (x : V) : Submodule.orthogonalBilin B (K ∙ x) = (B x).ker

theorem LinearMap.span_singleton_sup_orthogonal_eq_top {K : Type u_7} {V : Type u_9} [Field K] [AddCommGroup V] [Module K V] {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : (B x) x ≠ 0) : K ∙ x ⊔ Submodule.orthogonalBilin B (K ∙ x) = ⊤

theorem LinearMap.isCompl_span_singleton_orthogonal {K : Type u_7} {V : Type u_9} [Field K] [AddCommGroup V] [Module K V] {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : (B x) x ≠ 0) : IsCompl (K ∙ x) (Submodule.orthogonalBilin B (K ∙ x))

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.

theorem LinearMap.nondegenerate_restrict_of_disjoint_orthogonal {R : Type u_1} {M : Type u_4} {M₁ : Type u_5} [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 (Submodule.orthogonalBilin B W)) : (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).