idealOfLE — Mathlib

English

Given R ≤ S, the ideal of LE on R with respect to S is obtained by pulling back the maximal ideal of S along the inclusion R → S.

Русский

Пусть R ≤ S. Идеал, связанный с упрощением, получается как обратное образ максимального идеала S по включению R → S.

LaTeX

$$idealOfLE(R,S,h) = IsLocalRing.maximalIdeal(S).comap(R.inclusion S h)$$

Lean4

/-- The ideal corresponding to a coarsening of a valuation ring. -/
def idealOfLE (R S : ValuationSubring K) (h : R ≤ S) : Ideal R :=
  (IsLocalRing.maximalIdeal S).comap (R.inclusion S h)

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