isCompl_ker_of_disjoint_of_ne_bot

English

Under projectivity, W.dualAnnihilator = ⊤ if and only if W = ⊥.

Русский

При проективности W.dualAnnihilator = ⊤ тогда и только тогда, когда W = ⊥.

LaTeX

$$W.dualAnnihilator = ⊤ ↔ W = ⊥$$

Lean4

theorem isCompl_ker_of_disjoint_of_ne_bot {p : Submodule K V₁} (hpf : Disjoint (LinearMap.ker f) p) (hp : p ≠ ⊥) :
    IsCompl (LinearMap.ker f) p :=
  by
  refine ⟨hpf, codisjoint_iff.mpr <| eq_of_le_of_finrank_le le_top ?_⟩
  have : finrank K ↑(LinearMap.ker f ⊔ p) = finrank K (LinearMap.ker f) + finrank K p := by
    simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]
  rwa [finrank_top, this, ← finrank_ker_add_one_of_ne_zero hf, add_le_add_iff_left, Submodule.one_le_finrank_iff]

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