nondegenerate_restrict_of_disjoint_orthogonal

English

If a reflexive bilinear form B is nondegenerate on the whole space and W is such that W ∩ B.orthogonal W = {0}, then the restriction B|W is nondegenerate.

Русский

Если B - рефлексивная билинейная форма на всю поверхность пространства и W такова, что W ∩ B.orthogonal W = {0}, то ограничение B|W недегнерируемо.

LaTeX

$$$B.IsRefl \Rightarrow (W \cap B.orthogonal W = \bot) \Rightarrow (B.restrict W).Nondegenerate$$$

Lean4

/-- The restriction of a reflexive bilinear form `B` onto a submodule `W` is
nondegenerate if `Disjoint W (B.orthogonal W)`. -/
theorem nondegenerate_restrict_of_disjoint_orthogonal (B : BilinForm R₁ M₁) (b : B.IsRefl) {W : Submodule R₁ M₁}
    (hW : Disjoint W (B.orthogonal W)) : (B.restrict W).Nondegenerate :=
  by
  rintro ⟨x, hx⟩ b₁
  rw [Submodule.mk_eq_zero, ← Submodule.mem_bot R₁]
  refine hW.le_bot ⟨hx, fun y hy => ?_⟩
  specialize b₁ ⟨y, hy⟩
  simp only [restrict_apply, domRestrict_apply] at b₁
  exact isOrtho_def.mpr (b x y b₁)

Похожие утверждения