toLin_restrict_ker_eq_inf_orthogonal

English

The orthogonal to the span of x is the kernel of the linear map y ↦ B(x,y).

Русский

Ортогональность к спану x равна ядру отображения y ↦ B(x,y).

LaTeX

$$$B.orthogonal(K \cdot x) = \ker( y \mapsto B(x,y) )$$$

Lean4

theorem toLin_restrict_ker_eq_inf_orthogonal (B : BilinForm K V) (W : Subspace K V) (b : B.IsRefl) :
    (LinearMap.ker <| B.domRestrict W).map W.subtype = (W ⊓ B.orthogonal ⊤ : Subspace K V) :=
  by
  ext x; constructor <;> intro hx
  · rcases hx with ⟨⟨x, hx⟩, hker, rfl⟩
    constructor
    · simp [hx]
    · intro y _
      rw [IsOrtho, b]
      change (B.domRestrict W) ⟨x, hx⟩ y = 0
      rw [hker]
      rfl
  · simp_rw [Submodule.mem_map, LinearMap.mem_ker]
    refine ⟨⟨x, hx.1⟩, ?_, rfl⟩
    ext y
    change B x y = 0
    rw [b]
    exact hx.2 _ Submodule.mem_top

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