English
If R → S is unramified, then the image of maximalIdeal R under the map to S equals maximalIdeal S.
Русский
Если отображение R → S неразветвлено, то образ максимального идеала R под этот отображение равен максимальному идеалу S.
LaTeX
$$$(maximalIdeal R).map (algebraMap R S) = maximalIdeal S$$$
Lean4
theorem isField_quotient_map_maximalIdeal [FormallyUnramified R S] :
IsField (S ⧸ (maximalIdeal R).map (algebraMap R S)) :=
by
let mR := (maximalIdeal R).map (algebraMap R S)
have hmR : mR ≤ maximalIdeal S := ((local_hom_TFAE (algebraMap R S)).out 0 2 rfl rfl).mp ‹_›
letI : Algebra (ResidueField R) (S ⧸ mR) := inferInstanceAs (Algebra (R ⧸ _) _)
have : IsScalarTower R (ResidueField R) (S ⧸ mR) := inferInstanceAs (IsScalarTower R (R ⧸ _) _)
have : FormallyUnramified (ResidueField R) (S ⧸ mR) := .of_comp R _ _
have : EssFiniteType (ResidueField R) (S ⧸ mR) := .of_comp R _ _
have : Module.Finite (ResidueField R) (S ⧸ mR) := FormallyUnramified.finite_of_free _ _
have : IsReduced (S ⧸ mR) := FormallyUnramified.isReduced_of_field (ResidueField R) (S ⧸ mR)
have : IsArtinianRing (S ⧸ mR) := isArtinian_of_tower (ResidueField R) inferInstance
have : Nontrivial (S ⧸ mR) :=
Ideal.Quotient.nontrivial fun e ↦ (maximalIdeal.isMaximal S).ne_top (top_le_iff.mp <| e.symm.trans_le hmR)
have : IsLocalRing (S ⧸ mR) := .of_surjective' _ Ideal.Quotient.mk_surjective
have : maximalIdeal (S ⧸ mR) = ⊥ := by
rw [← jacobson_eq_maximalIdeal _ bot_ne_top, IsArtinianRing.jacobson_eq_radical, ← Ideal.zero_eq_bot, ← nilradical,
nilradical_eq_zero]
rwa [← isField_iff_maximalIdeal_eq] at this
