dualCoannihilator_map_linearEquiv_flip

English

For a reflexive module N and a perfect pairing, the dual coannihilator under the flip map corresponds to the dual annihilator under the inverse map; this is a compatibility relation between flips and annihilators.

Русский

Для рефлексивного модуля N и идеальной пары двойственные коаннигилятора под flip соответствуют двойственному аннигилятору через обратный отображатель.

LaTeX

$$$p: \\mathrm{dualCoannihilator}(p.map\\,\\text{flip}) = p.dualAnnihilator.map({\\text{symm}})$$$

Lean4

@[simp]
theorem dualCoannihilator_map_linearEquiv_flip (p : Submodule R M) :
    (p.map e.flip).dualCoannihilator = p.dualAnnihilator.map e.symm := by ext;
  simp [LinearEquiv.symm_apply_eq, Submodule.mem_dualCoannihilator]

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