ker_dualMap_eq_dualAnnihilator_range

English

For any submodule U of the dual space Module.Dual(R,M), applying dual annihilator, then dual coannihilator, then dual annihilator returns you to the original dual annihilator: U.dualAnnihilator.dualCoannihilator.dualAnnihilator = U.dualAnnihilator.

Русский

Для подмодуля U дуального пространства выполняется тройная цепочка: дуал-аннигилятор → дуал-коаннигилятора → дуал-аннигилятор возвращает исходный дуал-аннигилятор.

LaTeX

$$$ U.dualAnnihilator.dualCoannihilator.dualAnnihilator = U.dualAnnihilator $$$

Lean4

theorem ker_dualMap_eq_dualAnnihilator_range : LinearMap.ker f.dualMap = (range f).dualAnnihilator :=
  by
  ext
  simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator, ← SetLike.mem_coe, coe_range,
    Set.forall_mem_range]
  rfl

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