torsion_gc — Mathlib

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⟩⟩

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