ker_restrict_eq_of_codisjoint — Mathlib

English

If p and q are codisjoint and B x y=0 for all x∈p, y∈q, then ker(B|p) equals comap of ker(B) under p.subtype.

Русский

Если p и q кодиссоединены и для всех x∈p, y∈q выполняется B x y = 0, то ядро ограниченного B по p равно обратному образу ядра B по подтипу p.

LaTeX

$$$\ker(B|_p) = \operatorname{comap}_{p} (\ker B)$$$

Lean4

theorem ker_restrict_eq_of_codisjoint {p q : Submodule R M} (hpq : Codisjoint p q) {B : LinearMap.BilinForm R M}
    (hB : ∀ x ∈ p, ∀ y ∈ q, B x y = 0) : LinearMap.ker (B.restrict p) = (LinearMap.ker B).comap p.subtype :=
  by
  ext ⟨z, hz⟩
  simp only [LinearMap.mem_ker, Submodule.mem_comap, Submodule.coe_subtype]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · ext w
    obtain ⟨x, y, hx, hy, rfl⟩ := Submodule.codisjoint_iff_exists_add_eq.mp hpq w
    simpa [hB z hz y hy] using LinearMap.congr_fun h ⟨x, hx⟩
  · ext ⟨x, hx⟩
    simpa using LinearMap.congr_fun h x

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