gc — Mathlib · SciLib

English

There is a natural Galois connection between the two constructions fromIdeal and asIdeal, linking ideals and two-sided ideals via these two functors.

Русский

Существует естественное сопряжение Галуа между конструкциями fromIdeal и asIdeal, устанавливающее связь между идеалами и двусторонними идеалами через эти функторы.

LaTeX

$$$\mathrm{GaloisConnection}(\mathrm{fromIdeal},\mathrm{asIdeal})$$$

Lean4

theorem gc : GaloisConnection fromIdeal (asIdeal (R := R)) := fun I J =>
  ⟨fun h x hx ↦ h <| mem_span_iff.2 fun _ H ↦ H hx, fun h x hx ↦
    by
    simp only [fromIdeal, OrderHom.coe_mk, mem_span_iff] at hx
    exact hx _ h⟩

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