Orthogonal complement #
This file defines the orthogonal submodule of a submodule with respect to a sesqui-blinear map.
Main declarations #
orthogonalBilinprovides 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
Instances For
@[simp]
theorem
Submodule.mem_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₁}
{m : M₂}
:
@[deprecated Submodule.mem_orthogonalBilin (since := "2026-06-19")]
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₂}
:
Alias of Submodule.mem_orthogonalBilin.
theorem
Submodule.mem_orthogonalBilin_iff_le_ker_flip
{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₁}
{y : M₂}
:
@[simp]
theorem
Submodule.mem_orthogonalBilin_span
{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 : Set M₁}
{y : M₂}
:
theorem
Submodule.orthogonalBilin_gc
{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)
:
theorem
Submodule.le_orthogonalBilin_flip_iff_le_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₁}
{T : Submodule R₂ M₂}
:
theorem
Submodule.le_orthogonalBilin_flip_of_le_orthogonBilin
{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₁}
{T : Submodule R₂ M₂}
:
T ≤ orthogonalBilin B S → S ≤ orthogonalBilin B.flip T
Alias of the reverse direction of Submodule.le_orthogonalBilin_flip_iff_le_orthogonalBilin.
theorem
Submodule.le_orthogonalBilin_of_le_orthogonBilin_flip
{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₁}
{T : Submodule R₂ M₂}
:
S ≤ orthogonalBilin B.flip T → T ≤ orthogonalBilin B S
Alias of the forward direction of Submodule.le_orthogonalBilin_flip_iff_le_orthogonalBilin.
@[simp]
theorem
Submodule.orthogonalBilin_bot
{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}
:
@[simp]
theorem
Submodule.orthogonalBilin_ker
{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}
:
theorem
Submodule.orthogonalBilin_top_eq_ker
{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}
:
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)
:
theorem
Submodule.orthogonalBilin_anti
{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)
:
Alias of Submodule.orthogonalBilin_le.
theorem
Submodule.orthogonalBilin_antitone
{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}
:
theorem
Submodule.ker_flip_le_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₁)
:
theorem
Submodule.ker_le_orthogonalBilin_flip
{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₂)
:
theorem
Submodule.orthogonalBilin_span_singleton
{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}
(x : M₁)
:
@[deprecated Submodule.orthogonalBilin_span_singleton (since := "2026-06-19")]
theorem
LinearMap.orthogonal_span_singleton_eq_to_lin_ker
{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}
(x : M₁)
:
Alias of Submodule.orthogonalBilin_span_singleton.
theorem
Submodule.orthogonalBilin_sSup
{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 : Set (Submodule R₁ M₁))
:
theorem
Submodule.orthogonalBilin_iSup
{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}
{ι : Sort u_7}
(f : ι → Submodule R₁ M₁)
:
theorem
Submodule.orthogonalBilin_sup
{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₁)
:
@[simp]
theorem
Submodule.orthogonalBilin_sup_ker
{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₁)
:
theorem
Submodule.le_orthogonalBilin_flip_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₁}
:
Every submodule is contained in the orthogonal complement of its orthogonal complement.
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)
:
@[simp]
theorem
Submodule.orthogonalBilin_orthogonalBilin_flip_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₁)
:
@[simp]
theorem
Submodule.orthogonalBilin_flip_orthogonalBilin_orthogonalBilin_flip
{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₂)
:
theorem
Submodule.orthogonalBilin_sup_orthogonalBilin_le_orthogonalBilin_inf
{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₁)
:
@[simp]
theorem
Submodule.orthogonalBilin_eval_eq_dualAnnihilator
{R₁ : Type u_2}
{M₁ : Type u_5}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(S : Submodule R₁ M₁)
:
The orthogonal submodule w.r.t. the standard bilinear pairing is the dual annihilator.
@[simp]
theorem
Submodule.orthogonalBilin_id_eq_dualCoannihilator
{R₁ : Type u_2}
{M₁ : Type u_5}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(S : Submodule R₁ (Module.Dual R₁ M₁))
:
The orthogonal submodule w.r.t. the identity pairing is the dual coannihilator.
theorem
Submodule.orthogonalBilin_map
{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}
{R₃ : Type u_7}
[CommSemiring R₃]
{M₃ : Type u_8}
[AddCommMonoid M₃]
[Module R₃ M₃]
{J₃ : R₃ →+* R₁}
{J : R₃ →+* R}
[RingHomCompTriple J₃ I₁ J]
[RingHomSurjective J₃]
(S : Submodule R₃ M₃)
(q : M₃ →ₛₗ[J₃] M₁)
:
@[simp]
theorem
Submodule.orthogonalBilin_id_map
{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}
[RingHomSurjective I₁]
(S : Submodule R₁ M₁)
:
Orthogonality w.r.t. a general bilinear map can be expressed as orthogonality w.r.t the identity pairing.
theorem
Submodule.comap_orthogonalBilin_eval
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₁]
[CommSemiring R₂]
[AddCommMonoid M₁]
[Module R₁ M₁]
[AddCommMonoid M₂]
[Module R₂ M₂]
{I₂ : R₂ →+* R₁}
{B : M₁ →ₗ[R₁] M₂ →ₛₗ[I₂] R₁}
(S : Submodule R₁ M₁)
:
Orthogonality w.r.t. a general bilinear map can be expressed as orthogonality w.r.t the evaluation pairing.
@[simp]
theorem
Submodule.comap_dualAnnihilator_eq_orthogonalBilin
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₁]
[CommSemiring R₂]
[AddCommMonoid M₁]
[Module R₁ M₁]
[AddCommMonoid M₂]
[Module R₂ M₂]
{I₂ : R₂ →+* R₁}
(B : M₁ →ₗ[R₁] M₂ →ₛₗ[I₂] R₁)
(S : Submodule R₁ M₁)
:
theorem
Submodule.dualCoannihilator_map_eq_orthogonalBilin
{R₁ : Type u_2}
{R₂ : Type u_3}
{M₁ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R₁]
[CommSemiring R₂]
[AddCommMonoid M₁]
[Module R₁ M₁]
[AddCommMonoid M₂]
[Module R₂ M₂]
{I₁ : R₁ →+* R₂}
{B : M₁ →ₛₗ[I₁] M₂ →ₗ[R₂] R₂}
[RingHomSurjective I₁]
(S : Submodule R₁ M₁)
:
theorem
Submodule.orthogonalBilin_eval_map
{R₁ : Type u_2}
{M₁ : Type u_5}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{M₁' : Type u_9}
[AddCommMonoid M₁']
[Module R₁ M₁']
(q : M₁ →ₗ[R₁] M₁')
(S : Submodule R₁ M₁)
:
orthogonalBilin (Module.Dual.eval R₁ M₁') (map q S) = comap q.dualMap (orthogonalBilin (Module.Dual.eval R₁ M₁) S)
theorem
Submodule.orthogonalBilin_id_map_dualMap
{R₁ : Type u_2}
{M₁ : Type u_5}
[CommSemiring R₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{M₁' : Type u_9}
[AddCommMonoid M₁']
[Module R₁ M₁']
(q : M₁ →ₗ[R₁] M₁')
(S : Submodule R₁ (Module.Dual R₁ M₁'))
:
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).