gi — Mathlib · SciLib

English

The hull and toIdeal form a Galois insertion.

Русский

Оболочка и toIdeal образуют Galois-вставку.

LaTeX

$$$ \text{GaloisInsertion}( \text{Ideal.homogeneousHull } 𝒜, toIdeal) $$$

Lean4

/-- `Ideal.homogeneousHull 𝒜` and `toIdeal : HomogeneousIdeal 𝒜 → Ideal A` form a Galois
insertion. -/
def gi : GaloisInsertion (Ideal.homogeneousHull 𝒜) toIdeal
    where
  choice I H := ⟨I, le_antisymm H (I.le_toIdeal_homogeneousHull 𝒜) ▸ isHomogeneous _⟩
  gc := Ideal.homogeneousHull.gc 𝒜
  le_l_u _ := Ideal.le_toIdeal_homogeneousHull _ _
  choice_eq I H := le_antisymm (I.le_toIdeal_homogeneousHull 𝒜) H

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