English
If unramified, then the map of maximal ideals is compatible with residue fields isomorphisms; equivalence provided.
Русский
Если неразветвленно, отображение максимальных идеалов совместимо с изоморфизмами остаточных полей; приводится эквивалентность.
LaTeX
$$map_maximalIdeal$$
Lean4
@[stacks 02FM]
theorem of_map_maximalIdeal [Algebra.IsSeparable (ResidueField R) (ResidueField S)]
(H : (maximalIdeal R).map (algebraMap R S) = maximalIdeal S) : Algebra.FormallyUnramified R S :=
by
constructor
have : FormallyUnramified (ResidueField R) (ResidueField S) := .of_isSeparable _ _
have : FormallyUnramified R (ResidueField S) := .comp _ (ResidueField R) _
rw [← subsingleton_tensorProduct (R := S)]
refine subsingleton_of_forall_eq 0 fun x ↦ ?_
obtain ⟨x, rfl⟩ :=
(KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange R S (ResidueField S) Ideal.Quotient.mk_surjective
x).mp
(Subsingleton.elim _ _)
obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
simp only [KaehlerDifferential.kerCotangentToTensor_toCotangent]
replace hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R) := by simpa [H] using hx
induction hx using Submodule.span_induction with
| zero => simp
| mem x h => obtain ⟨x, hx, rfl⟩ := h; simp
| add x y hx hy _ _ => simp [*, TensorProduct.tmul_add]
| smul a x hx _ =>
have : residue S x = 0 := by rwa [residue_eq_zero_iff, ← H]
simp [*, TensorProduct.tmul_add, TensorProduct.smul_tmul', ← Algebra.algebraMap_eq_smul_one]
