English
The equality between the dual coannihilator map on p and the dual annihilator map on p via e (and flip) holds, i.e. Submodule.map e.flip.symm p.dualCoannihilator = Submodule.map e p.dualAnnihilator.
Русский
Сохранение равенства между dualCoannihilator и dualAnnihilator проходит через flip и e: Submodule.map e.flip.symm p.dualCoannihilator = Submodule.map e p.dualAnnihilator.
LaTeX
$$$\\text{Submodule.map } e.flip.symm\, p.dualCoannihilator = \\text{Submodule.map } e\\ p.dualAnnihilator$$$
Lean4
@[simp]
theorem map_dualCoannihilator_linearEquiv_flip (p : Submodule R (Dual R M)) :
p.dualCoannihilator.map e.flip = (p.map e.symm).dualAnnihilator :=
by
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive
suffices (p.map e.symm).dualAnnihilator.map e.flip.symm = (p.dualCoannihilator.map e.flip).map e.flip.symm by
exact (Submodule.map_injective_of_injective e.flip.symm.injective this).symm
erw [← dualCoannihilator_map_linearEquiv_flip, flip_flip, ← map_comp, ← map_comp]
simp [-coe_toLinearMap_flip]
