iff_map_maximalIdeal_eq — Mathlib

English

Equivalence between FormallyUnramified and (IsSeparable residue fields) ∧ (maximalIdeal map equality).

Русский

Эквивалентность формально неразветвленного и (разделимости остаточных полей) ∧ (равенство отображения максимальных идеалов).

LaTeX

$$FormallyUnramified R S ↔ IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) ∧ (maximalIdeal R).map (algebraMap R S) = maximalIdeal S$$

Lean4

theorem iff_map_maximalIdeal_eq :
    Algebra.FormallyUnramified R S ↔
      Algebra.IsSeparable (ResidueField R) (ResidueField S) ∧ (maximalIdeal R).map (algebraMap R S) = maximalIdeal S :=
  ⟨fun _ ↦ ⟨inferInstance, map_maximalIdeal⟩, fun ⟨_, e⟩ ↦ of_map_maximalIdeal e⟩

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