English
Let B be a symmetric bilinear form on M with hs: B(x,x) ≥ 0 for all x, and let W be a submodule. The restricted form B|W×W is nondegenerate if and only if W ∩ ker B = {0}.
Русский
Пусть B — симметричная билинейная форма на M с неотрицательностью на квадратах и W — подмодуль. Ограниченная форма B|W×W необразна тогда, когда пересечение W и ядра B тривиально (равно {0}).
LaTeX
$$$\big( \forall x, 0 \le B(x,x) \big) \land B \text{ симметрична} \Rightarrow ( (B|_{W}\!\_{1}\!2) \text{ необразна} \iff W \cap \ker B = \{0\} )$$$
Lean4
theorem nondegenerate_restrict_iff_disjoint_ker (hs : ∀ x, 0 ≤ B x x) (hB : B.IsSymm) {W : Submodule R M} :
(B.domRestrict₁₂ W W).Nondegenerate ↔ Disjoint W (LinearMap.ker B) :=
by
refine ⟨disjoint_ker_of_nondegenerate_restrict, fun hW ↦ ?_⟩
have hB' : (B.domRestrict₁₂ W W).IsRefl := fun x y ↦ hB.isRefl (W.subtype x) (W.subtype y)
rw [IsRefl.nondegenerate_iff_separatingLeft hB']
intro ⟨x, hx⟩ h
simp_rw [Subtype.forall, domRestrict₁₂_apply] at h
specialize h x hx
rw [B.apply_apply_same_eq_zero_iff hs hB] at h
have key : x ∈ W ⊓ LinearMap.ker B := ⟨hx, h⟩
simpa [hW.eq_bot] using key
