English
For a bilinear form B and subspace W, the kernel of the restricted B corresponds to W ∩ B.orthogonal(⊤).
Русский
Yдко B и подпространство W, ядро ограниченного B соответствует W ∩ B.orthogonal(⊤).
LaTeX
$$(LinearMap.ker B.domRestrict W).map W.subtype = W ⊓ B.orthogonal ⊤$$
Lean4
/-- The restriction of a reflexive, non-degenerate bilinear form on the orthogonal complement of
the span of a singleton is also non-degenerate. -/
theorem restrict_nondegenerate_orthogonal_spanSingleton (B : BilinForm K V) (b₁ : B.Nondegenerate) (b₂ : B.IsRefl)
{x : V} (hx : ¬B.IsOrtho x x) : Nondegenerate <| B.restrict <| B.orthogonal (K ∙ x) :=
by
refine fun m hm => Submodule.coe_eq_zero.1 (b₁ m.1 fun n => ?_)
have : n ∈ (K ∙ x) ⊔ B.orthogonal (K ∙ x) := (span_singleton_sup_orthogonal_eq_top hx).symm ▸ Submodule.mem_top
rcases Submodule.mem_sup.1 this with ⟨y, hy, z, hz, rfl⟩
specialize hm ⟨z, hz⟩
rw [restrict] at hm
erw [add_right, show B m.1 y = 0 by rw [b₂]; exact m.2 y hy, hm, add_zero]
