map_maximalIdeal — Mathlib

English

Unramified at a prime is equivalent to residue fields separable plus the maximal ideal mapping condition after localization.

Русский

Неразветвленность в отношении данного максимального идеала эквивалентна разделимости остаточных полей плюс условие отображения максимального идеала после локализации.

LaTeX

$$$\\text{IsUnramifiedAt } R q \\iff (\\text{IsSeparable } p.ResidueField q.ResidueField) \\land \\big( p.map (algebraMap R (Localization.AtPrime q)) = maximalIdeal _ \\big)$$$

Lean4

@[stacks 00UW "(1)"]
theorem map_maximalIdeal [FormallyUnramified R S] : (maximalIdeal R).map (algebraMap R S) = maximalIdeal S :=
  by
  apply eq_maximalIdeal
  rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient]
  exact isField_quotient_map_maximalIdeal

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