English
Let R be a commutative ring, M and N be modules with reflexive structure, and e a linear equivalence between N and the dual of M. For any submodule p of Dual R N, the dual annihilator of the image of p under the induced flip map equals the image under e of the dual coannihilator of p.
Русский
Пусть R — коммутативное кольцо, M и N — модули с рефлексивной структурой, и e — линейное эквивалентное отображение между N и двойственным пространством M. Для любой подпространства p ⊆ Dual R N верная дуальная аннигиляция образа p под индуцированной отображением flip равна образу под p.dualCoannihilator через e.
LaTeX
$$$(p.map\, e.flip.symm).dualAnnihilator = p.dualCoannihilator.map\, e$$$
Lean4
@[simp]
theorem dualAnnihilator_map_linearEquiv_flip_symm (p : Submodule R (Dual R N)) :
(p.map e.flip.symm).dualAnnihilator = p.dualCoannihilator.map e :=
by
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
rw [← map_dualCoannihilator_linearEquiv_flip, flip_flip]
