gi — Mathlib · SciLib

English

There is a Galois coinsertion between toIdeal and Ideal.homogeneousCore 𝒜.

Русский

Существует сопряжённое вложение между toIdeal и Ideal.homogeneousCore 𝒜.

LaTeX

$$$ \text{GaloisCoinsertion}(\text{toIdeal}, \text{Ideal.homogeneousCore } 𝒜) $$$

Lean4

/-- `toIdeal : HomogeneousIdeal 𝒜 → Ideal A` and `Ideal.homogeneousCore 𝒜` forms a Galois
coinsertion. -/
def gi : GaloisCoinsertion toIdeal (Ideal.homogeneousCore 𝒜)
    where
  choice I HI := ⟨I, le_antisymm (I.toIdeal_homogeneousCore_le 𝒜) HI ▸ HomogeneousIdeal.isHomogeneous _⟩
  gc := Ideal.homogeneousCore.gc 𝒜
  u_l_le _ := Ideal.homogeneousCore'_le _ _
  choice_eq I H := le_antisymm H (I.toIdeal_homogeneousCore_le _)

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