feat(RingTheory): More API for Ideal.ResidueField (leanprover-community#32375)

Author: erdOne

Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

@@ -61,8 +61,8 @@ variable (R S) in
 noncomputable def PrimeSpectrum.preimageEquivFiber (p : PrimeSpectrum R) :
     (algebraMap R S).specComap ⁻¹' {p} ≃ PrimeSpectrum (p.asIdeal.Fiber S) where
   toFun q := ⟨RingHom.ker (Algebra.TensorProduct.lift
-        (Ideal.ResidueField.mapₐ p.asIdeal q.1.asIdeal congr($(q.2.symm).asIdeal))
-          (IsScalarTower.toAlgHom _ _ _) (fun _ _ ↦ .all _ _)).toRingHom, RingHom.ker_isPrime _⟩
+    (Ideal.ResidueField.mapₐ p.asIdeal q.1.asIdeal (Algebra.ofId _ _) congr($(q.2.symm).asIdeal))
+      (IsScalarTower.toAlgHom _ _ _) fun _ _ ↦ .all _ _).toRingHom, RingHom.ker_isPrime _⟩
   invFun q := ⟨Algebra.TensorProduct.includeRight.toRingHom.specComap q, by
     simp only [AlgHom.toRingHom_eq_coe, Set.mem_preimage, ← specComap_comp_apply,
       AlgHom.comp_algebraMap_of_tower]
@@ -78,7 +78,8 @@ noncomputable def PrimeSpectrum.preimageEquivFiber (p : PrimeSpectrum R) :
     · rw [← Ideal.mem_comap, ← PrimeSpectrum.specComap_asIdeal]
       convert hr
       exact (residueField_specComap _).le ⟨(algebraMap _ _).specComap q, rfl⟩
-    · simpa [-Algebra.algebraMap_self, -AlgHom.commutes, -AlgHom.map_algebraMap]
+    · simpa [-Algebra.algebraMap_self, -AlgHom.commutes, -AlgHom.map_algebraMap,
+        -Ideal.ResidueField.map_algebraMap]
 
 variable (R S) in
 /-- The `OrderIso` between the fiber of `PrimeSpectrum S → PrimeSpectrum R` at a prime

Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

@@ -20,8 +20,10 @@ and provide an `IsFractionRing (R ⧸ I) I.ResidueField` instance.
 
 @[expose] public section
 
-variable {R A} [CommRing R] [CommRing A] [Algebra R A]
-variable (I : Ideal R) [I.IsPrime]
+open scoped nonZeroDivisors
+
+variable {R S A B : Type*} [CommRing R] [CommRing S] [CommRing A] [CommRing B]
+variable [Algebra R A] [Algebra R B] (I : Ideal R) [I.IsPrime]
 
 /--
 The residue field at a prime ideal, defined to be the residue field of the local ring
@@ -33,25 +35,30 @@ abbrev Ideal.ResidueField : Type _ :=
 
 /-- If `I = f⁻¹(J)`, then there is a canonical embedding `κ(I) ↪ κ(J)`. -/
 noncomputable
-abbrev Ideal.ResidueField.map (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime]
-    (f : R →+* A) (hf : I = J.comap f) : I.ResidueField →+* J.ResidueField :=
+abbrev Ideal.ResidueField.map (I : Ideal R) [I.IsPrime] (J : Ideal S) [J.IsPrime]
+    (f : R →+* S) (hf : I = J.comap f) : I.ResidueField →+* J.ResidueField :=
   IsLocalRing.ResidueField.map (Localization.localRingHom I J f hf)
 
+@[simp]
+lemma Ideal.ResidueField.map_algebraMap (I : Ideal R) [I.IsPrime] (J : Ideal S) [J.IsPrime]
+    (f : R →+* S) (hf : I = J.comap f) (r : R) :
+    ResidueField.map I J f hf (algebraMap _ _ r) = algebraMap _ _ (f r) := by
+  rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I)]
+  simp [IsLocalRing.ResidueField.map_residue, Localization.localRingHom_to_map]
+  rfl
+
 /-- If `I = f⁻¹(J)`, then there is a canonical embedding `κ(I) ↪ κ(J)`. -/
 noncomputable
-def Ideal.ResidueField.mapₐ (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime]
-    (hf : I = J.comap (algebraMap R A)) : I.ResidueField →ₐ[R] J.ResidueField where
-  __ := Ideal.ResidueField.map I J (algebraMap R A) hf
+def Ideal.ResidueField.mapₐ (I : Ideal A) [I.IsPrime] (J : Ideal B) [J.IsPrime]
+    (f : A →ₐ[R] B) (hf : I = J.comap f.toRingHom) : I.ResidueField →ₐ[R] J.ResidueField where
+  __ := Ideal.ResidueField.map I J f hf
   commutes' r := by
-    rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I),
-      IsLocalRing.ResidueField.algebraMap_eq]
-    simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
-      MonoidHom.coe_coe, IsLocalRing.ResidueField.map_residue, Localization.localRingHom_to_map]
-    rfl
+    simp [IsScalarTower.algebraMap_apply R A I.ResidueField,
+      IsScalarTower.algebraMap_apply R B J.ResidueField]
 
-@[simp] lemma Ideal.ResidueField.mapₐ_apply (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime]
-    (hf : I = J.comap (algebraMap R A)) (x) :
-    Ideal.ResidueField.mapₐ I J hf x = Ideal.ResidueField.map I J _ hf x := rfl
+@[simp] lemma Ideal.ResidueField.mapₐ_apply (I : Ideal A) [I.IsPrime] (J : Ideal B) [J.IsPrime]
+    (f : A →ₐ[R] B) (hf : I = J.comap f.toRingHom) (x) :
+    Ideal.ResidueField.mapₐ I J f hf x = Ideal.ResidueField.map I J _ hf x := rfl
 
 variable {I} in
 @[simp high] -- marked `high` to override the more general `FaithfulSMul.algebraMap_eq_zero_iff`
@@ -75,10 +82,13 @@ instance : IsScalarTower R (R ⧸ I) I.ResidueField :=
   IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
 
 @[simp]
-lemma algebraMap_mk (x) :
+lemma Ideal.algebraMap_quotient_residueField_mk (x) :
     algebraMap (R ⧸ I) I.ResidueField (Ideal.Quotient.mk _ x) =
     algebraMap R I.ResidueField x := rfl
 
+@[deprecated (since := "2025-12-02")]
+alias algebraMap_mk := Ideal.algebraMap_quotient_residueField_mk
+
 lemma Ideal.injective_algebraMap_quotient_residueField :
     Function.Injective (algebraMap (R ⧸ I) I.ResidueField) := by
   rw [RingHom.injective_iff_ker_eq_bot]
@@ -100,8 +110,9 @@ instance : IsFractionRing (R ⧸ I) I.ResidueField where
     obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
     rw [← sub_eq_zero, ← map_sub, ← map_sub] at e
     simp only [IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff,
-      IsScalarTower.algebraMap_apply R (Localization.AtPrime I) I.ResidueField, algebraMap_mk,
-      IsLocalization.AtPrime.to_map_mem_maximal_iff _ I, ← Ideal.Quotient.mk_eq_mk_iff_sub_mem] at e
+      IsScalarTower.algebraMap_apply R (Localization.AtPrime I) I.ResidueField,
+      Ideal.algebraMap_quotient_residueField_mk, IsLocalization.AtPrime.to_map_mem_maximal_iff _ I,
+      ← Ideal.Quotient.mk_eq_mk_iff_sub_mem] at e
     use 1
     simp [e]
 
@@ -118,3 +129,45 @@ lemma Ideal.surjectiveOnStalks_residueField (I : Ideal R) [I.IsPrime] :
 instance (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p] :
     IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) :=
   Localization.isLocalHom_localRingHom _ _ _ (Ideal.over_def _ _)
+
+/-- If `f` sends `I` to `0` and `Iᶜ` to units, then `f` lifts to `κ(I)`. -/
+noncomputable def Ideal.ResidueField.lift
+    (f : R →+* S) (hf₁ : I ≤ RingHom.ker f)
+    (hf₂ : I.primeCompl ≤ (IsUnit.submonoid S).comap f) : I.ResidueField →+* S :=
+  IsLocalization.lift (M := (R ⧸ I)⁰) (g := Ideal.Quotient.lift I (f := f) hf₁) <| by
+    simpa [Ideal.Quotient.mk_surjective.forall, Ideal.Quotient.eq_zero_iff_mem]
+
+@[simp] lemma Ideal.ResidueField.lift_algebraMap
+    (f : R →+* S) (hf₁ : I ≤ RingHom.ker f)
+    (hf₂ : I.primeCompl ≤ (IsUnit.submonoid S).comap f) (r : R) :
+    lift I f hf₁ hf₂ (algebraMap _ _ r) = f r := by
+  rw [lift, IsScalarTower.algebraMap_apply R (R ⧸ I) I.ResidueField, IsLocalization.lift_eq]
+  simp
+
+/-- If `f` sends `I` to `0` and `Iᶜ` to units, then `f` lifts to `κ(I)`. -/
+noncomputable
+def Ideal.ResidueField.liftₐ (I : Ideal A) [I.IsPrime] (f : A →ₐ[R] B) (hf₁ : I ≤ RingHom.ker f)
+    (hf₂ : I.primeCompl ≤ (IsUnit.submonoid B).comap f) : I.ResidueField →ₐ[R] B where
+  __ := Ideal.ResidueField.lift I f.toRingHom hf₁ hf₂
+  commutes' r := by simp [IsScalarTower.algebraMap_apply R A I.ResidueField]
+
+@[simp]
+lemma Ideal.ResidueField.liftₐ_algebraMap (I : Ideal A) [I.IsPrime] (f : A →ₐ[R] B)
+    (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ (IsUnit.submonoid B).comap f) (r : A) :
+    liftₐ I f hf₁ hf₂ (algebraMap _ _ r) = f r :=
+  lift_algebraMap _ _ _ hf₂ _
+
+@[simp] lemma Ideal.ResidueField.liftₐ_comp_toAlgHom (I : Ideal A) [I.IsPrime] (f : A →ₐ[R] B)
+    (hf₁ : I ≤ RingHom.ker f) (hf₂ : I.primeCompl ≤ (IsUnit.submonoid B).comap f) :
+    (liftₐ I f hf₁ hf₂).comp (IsScalarTower.toAlgHom _ A _) = f :=
+  AlgHom.ext fun _ ↦ liftₐ_algebraMap _ _ _ hf₂ _
+
+@[ext high] -- higher than `RingHom.ext`.
+lemma Ideal.ResidueField.ringHom_ext {I : Ideal R} [I.IsPrime]
+    {f g : I.ResidueField →+* S} (H : f.comp (algebraMap R _) = g.comp (algebraMap R _)) : f = g :=
+  IsLocalization.ringHom_ext (R ⧸ I)⁰ (Ideal.Quotient.ringHom_ext H)
+
+@[ext high] -- higher than `AlgHom.ext`.
+lemma Ideal.ResidueField.algHom_ext {I : Ideal A} [I.IsPrime] {f g : I.ResidueField →ₐ[R] B}
+    (H : f.comp (IsScalarTower.toAlgHom R A _) = g.comp (IsScalarTower.toAlgHom R A _)) : f = g :=
+  AlgHom.coe_ringHom_injective (ringHom_ext congr($H))

Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean

@@ -32,7 +32,7 @@ instance [p.IsMaximal] [q.IsMaximal] [Algebra.IsSeparable p.ResidueField q.Resid
   refine Algebra.IsSeparable.of_equiv_equiv
     (.symm <| .ofBijective _ p.bijective_algebraMap_quotient_residueField)
     (.symm <| .ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_
-  ext x
+  apply RingHom.ext fun x ↦ ?_
   obtain ⟨x, rfl⟩ :=
     (RingEquiv.ofBijective _ p.bijective_algebraMap_quotient_residueField).surjective x
   obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean

@@ -83,7 +83,7 @@ lemma mem_image_comap_zeroLocus_sdiff (f : A) (s : Set A) (x) :
         q.asIdeal.ResidueField :=
       Algebra.TensorProduct.lift
         (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A _) hs)
-        (Ideal.ResidueField.mapₐ _ _ rfl)
+        (Ideal.ResidueField.mapₐ _ _ (Algebra.ofId _ _) rfl)
         fun _ _ ↦ .all _ _
     have := H.map F
     rw [AlgHom.commutes, isNilpotent_iff_eq_zero, ← RingHom.mem_ker,

Mathlib/RingTheory/Spectrum/Prime/RingHom.lean

@@ -279,7 +279,7 @@ lemma PrimeSpectrum.nontrivial_iff_mem_rangeComap {S : Type*} [CommRing S]
     simp [Ideal.eq_bot_of_prime, k, ← RingHom.ker_eq_comap_bot]
   · obtain ⟨q, rfl⟩ := h
     let f : k ⊗[R] S →ₐ[R] q.asIdeal.ResidueField :=
-      Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ _ _ rfl)
+      Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ _ _ (Algebra.ofId _ _) rfl)
         (IsScalarTower.toAlgHom _ _ _) (fun _ _ ↦ Commute.all ..)
     exact RingHom.domain_nontrivial f.toRingHom