nondegenerate_restrict_of_disjoint_orthogonal

English

Similarly for a right-separating bilinear form with its flip.

Русский

Аналогично для правого разделяющего билинейного отображения и его перевернутой формы.

LaTeX

$$Notations analogous to left-right for IsOrthoᵢ basis$$

Lean4

/-- 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)`. -/
theorem nondegenerate_restrict_of_disjoint_orthogonal {B : M →ₗ[R] M →ₗ[R] M₁} (hB : B.IsRefl) {W : Submodule R M}
    (hW : Disjoint W (W.orthogonalBilin B)) : (B.domRestrict₁₂ W W).Nondegenerate :=
  by
  rw [(hB.domRestrict W).nondegenerate_iff_separatingLeft]
  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_rw [domRestrict₁₂_apply] at b₁
  rw [hB.ortho_comm]
  exact b₁

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