English
Membership in the orthogonalBilin submodule is characterized by orthogonality to all elements of N.
Русский
Членство в подмодуле orthogonalBilin определяется тем, что элемент ортогонален всем элементам N.
LaTeX
$$@[simp] theorem mem_orthogonalBilin_iff {m} : m ∈ N.orthogonalBilin B ↔ ∀ n ∈ N, B.IsOrtho n m$$
Lean4
/-- 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. -/
def orthogonalBilin (N : Submodule R₁ M₁) (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M) : Submodule R₁ M₁
where
carrier := {m | ∀ n ∈ N, B.IsOrtho n m}
zero_mem' x _ := B.isOrtho_zero_right x
add_mem' hx hy n
hn := by rw [LinearMap.IsOrtho, map_add, show B n _ = 0 from hx n hn, show B n _ = 0 from hy n hn, zero_add]
smul_mem' c x hx n hn := by rw [LinearMap.IsOrtho, LinearMap.map_smulₛₗ, show B n x = 0 from hx n hn, smul_zero]
