English
There is a Galois connection between submodules and annihilators given by torsionBySet and annihilator.
Русский
Существует связь Галуа между подмодулями и аннигиляторами через torsionBySet и annihilator.
LaTeX
$$$\text{GaloisConnection}\,\mathrm{Submodule}\,\mathrm{annihilator}\,\text{ and }\mathrm{torsionBySet}$$$
Lean4
theorem torsion_gc :
@GaloisConnection (Submodule R M) (Ideal R)ᵒᵈ _ _ annihilator fun I => torsionBySet R M ↑(OrderDual.ofDual I) :=
fun _ _ =>
⟨fun h x hx => (mem_torsionBySet_iff _ _).mpr fun ⟨_, ha⟩ => mem_annihilator.mp (h ha) x hx, fun h a ha =>
mem_annihilator.mpr fun _ hx => (mem_torsionBySet_iff _ _).mp (h hx) ⟨a, ha⟩⟩