refactor(Localization/AtPrime/Basic): add predicate for algebra instance on Localization.AtPrime (#38465)

Currently [Localization.AtPrime](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Localization/AtPrime/Basic.html#Localization.AtPrime.instAlgebraOfLiesOver) induces a diamond when the top ring is already an algebra over the localization of the bottom ring (e.g., this happens for `Ideal.Fiber`). This PR resolves the diamond by turning the instance into a def and adding a predicate typeclass.

Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/instance.20diamond.20with.20.60Ideal.2EFiber.60

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/AlgebraicGeometry/Morphisms/QuasiFinite.lean

@@ -419,6 +419,7 @@ nonrec lemma Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber
   rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)] at ‹LocallyOfFiniteType (Spec.map φ)›
   algebraize [φ.hom]
   rw [← Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber]
+  let := Localization.AtPrime.algebraOfLiesOver (x.asIdeal.under R) x.asIdeal
   trans Algebra.QuasiFinite (Localization.AtPrime (x.asIdeal.under R))
     (Localization.AtPrime x.asIdeal)
   · rw [← RingHom.quasiFinite_algebraMap]

Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

@@ -247,11 +247,12 @@ lemma formallySmooth_stalkMap_iff {f : X ⟶ Y} {x : X} (U : Y.Opens)
     (f.stalkMap x).hom.FormallySmooth ↔
       hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus Γ(Y, U) Γ(X, V) := by
   letI := (f.appLE U V hVU).hom.toAlgebra
-  have : (hV.primeIdealOf ⟨x, hx⟩).asIdeal.LiesOver (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal :=
+  let p := (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal
+  let q := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
+  have : q.LiesOver p :=
     ⟨congr($(IsAffineOpen.comap_primeIdealOf_appLE U hU V hV hVU hx).1).symm⟩
-  trans Algebra.FormallySmooth
-    (Localization.AtPrime (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal)
-    (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)
+  let := Localization.AtPrime.algebraOfLiesOver p q
+  trans Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)
   · rw [← formallySmooth_algebraMap]
     exact RingHom.FormallySmooth.respectsIso.arrow_mk_iso_iff
       (IsAffineOpen.arrowStalkMapIso f U hU V hV hVU hx)

Mathlib/NumberTheory/RamificationInertia/Unramified.lean

@@ -37,6 +37,7 @@ lemma Ideal.ramificationIdx_eq_one_of_isUnramifiedAt
     {p : Ideal S} [p.IsPrime] [IsNoetherianRing S] [IsUnramifiedAt R p]
     (hp : p ≠ ⊥) [IsDomain S] [EssFiniteType R S] :
     e(p|R) = 1 :=
+  let := Localization.AtPrime.algebraOfLiesOver (p.under R) p
   (Ideal.ramificationIdx_eq_one_of_map_localization Ideal.map_comap_le hp
     p.primeCompl_le_nonZeroDivisors
     ((isUnramifiedAt_iff_map_eq R (p.under R) p).mp ‹_›).2)
@@ -49,6 +50,9 @@ lemma IsUnramifiedAt.of_liesOver_of_ne_bot
     IsUnramifiedAt R p := by
   let p₀ : Ideal R := p.under R
   have : P.LiesOver p₀ := .trans P p p₀
+  let := Localization.AtPrime.algebraOfLiesOver p₀ p
+  let := Localization.AtPrime.algebraOfLiesOver p P
+  let := Localization.AtPrime.algebraOfLiesOver p₀ P
   have hp₀ : p₀ = P.under R := Ideal.LiesOver.over
   have : EssFiniteType S T := .of_comp R S T
   have := Algebra.EssFiniteType.isNoetherianRing S T
@@ -91,6 +95,7 @@ lemma Algebra.isUnramifiedAt_iff_of_isDedekindDomain
     [Module.Finite ℤ R] [CharZero R] [Algebra.IsIntegral R S]
     (hp : p ≠ ⊥) :
     Algebra.IsUnramifiedAt R p ↔ e(p|R) = 1 := by
+  let := Localization.AtPrime.algebraOfLiesOver (p.under R) p
   rw [isUnramifiedAt_iff_map_eq R (p.under R) p, and_iff_right,
     Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hp Ideal.map_comap_le]
   have : Finite (R ⧸ p.under R) :=

Mathlib/RingTheory/DedekindDomain/Different.lean

@@ -923,6 +923,7 @@ theorem not_dvd_differentIdeal_iff
   have hp' := (Ideal.map_eq_bot_iff_of_injective
     (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
   have := Ideal.IsPrime.isMaximal inferInstance hPbot
+  let := Localization.AtPrime.algebraOfLiesOver (P.under A) P
   constructor
   · intro H
     · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]

Mathlib/RingTheory/Etale/Locus.lean

@@ -46,6 +46,7 @@ lemma mem_etaleLocus_iff {p : PrimeSpectrum A} : p ∈ etaleLocus R A ↔ IsEtal
 lemma IsEtaleAt.comp
     (p : Ideal A) (P : Ideal B) [P.LiesOver p] [p.IsPrime] [P.IsPrime]
     [IsEtaleAt R p] [IsEtaleAt A P] : IsEtaleAt R P := by
+  let := Localization.AtPrime.algebraOfLiesOver p P
   have : FormallyEtale (Localization.AtPrime p) (Localization.AtPrime P) :=
     .localization_base p.primeCompl
   exact FormallyEtale.comp R (Localization.AtPrime p) _

Mathlib/RingTheory/Etale/QuasiFinite.lean

@@ -39,6 +39,7 @@ noncomputable
 def Ideal.fiberIsoOfBijectiveResidueField
     (H : Function.Bijective (Ideal.ResidueField.mapₐ p q (Algebra.ofId _ _) (q.over_def p))) :
     q.primesOver (R' ⊗[R] S) ≃o p.primesOver S :=
+  let := Localization.AtPrime.algebraOfLiesOver p q
   let e : q.Fiber (R' ⊗[R] S) ≃ₐ[p.ResidueField] p.Fiber S :=
     ((Algebra.TensorProduct.cancelBaseChange _ _ q.ResidueField _ _).restrictScalars _).trans
       (Algebra.TensorProduct.congr (.symm <| .ofBijective (Algebra.ofId _ _) H) .refl)
@@ -251,6 +252,7 @@ lemma Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux
     simp only [e₀, ← aeval_algHom_apply]; rfl
   have he : IsIdempotentElem e := he₀e ▸ he₀.map _
   let P' := (Ideal.fiberIsoOfBijectiveResidueField hP).symm ⟨q, ‹_›, ‹_›⟩
+  let := Localization.AtPrime.algebraOfLiesOver P P'.1
   have hP'q : P'.1.comap Algebra.TensorProduct.includeRight.toRingHom = q :=
     Ideal.comap_fiberIsoOfBijectiveResidueField_symm ..
   have hs'P' : s' ∉ P'.1 := mt (fun h ↦ hP'q.le h) hsq

Mathlib/RingTheory/Flat/Localization.lean

@@ -105,7 +105,9 @@ end Module
 
 variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
 
-instance [Module.Flat A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p] :
+instance [Module.Flat A B] (p : Ideal A) [p.IsPrime] (P : Ideal B) [P.IsPrime] [P.LiesOver p]
+    [Algebra (Localization.AtPrime p) (Localization.AtPrime P)]
+    [Localization.AtPrime.IsLiesOverAlgebra p P] :
     Module.Flat (Localization.AtPrime p) (Localization.AtPrime P) := by
   rw [Module.flat_iff_of_isLocalization (Localization.AtPrime p) p.primeCompl]
   exact Module.Flat.trans A B (Localization.AtPrime P)

Mathlib/RingTheory/Flat/Rank.lean

@@ -60,6 +60,7 @@ lemma PrimeSpectrum.comap_surjective_iff_injective_of_finite :
   rw [← faithfulSMul_iff_algebraMap_injective]
   obtain ⟨⟨Q, _⟩, hQ⟩ := h ⟨p, inferInstance⟩
   have : Q.LiesOver p := ⟨congr($(hQ).asIdeal).symm⟩
+  let := Localization.AtPrime.algebraOfLiesOver p Q
   have : Nontrivial (Localization.AtPrime p ⊗[R] S) := by
     let f : Localization.AtPrime p ⊗[R] S →ₐ[R] Localization.AtPrime Q :=
       Algebra.TensorProduct.lift (IsScalarTower.toAlgHom R _ _)

Mathlib/RingTheory/Ideal/GoingDown.lean

@@ -144,7 +144,8 @@ lemma of_comap_localRingHom_surjective
     obtain ⟨⟨Pl, _⟩, hl⟩ := H Q ⟨pl, inferInstance⟩
     refine ⟨Pl.under S, ?_, Ideal.IsPrime.under S Pl, ⟨?_⟩⟩
     · exact (IsLocalization.AtPrime.orderIsoOfPrime _ Q ⟨Pl, inferInstance⟩).2.2
-    · replace hl : Pl.under _ = pl := by simpa [PrimeSpectrum.ext_iff] using hl
+    · let := Localization.AtPrime.algebraOfLiesOver (Q.under R) Q
+      replace hl : Pl.under _ = pl := by simpa [PrimeSpectrum.ext_iff] using hl
       rw [Ideal.under_under, ← Ideal.under_under (B := (Localization.AtPrime <| Q.under R)) Pl, hl,
         Ideal.under_map_of_isLocalizationAtPrime (Q.under R) hlt.le]
 
@@ -153,6 +154,7 @@ lemma of_comap_localRingHom_surjective
 instance of_flat [Module.Flat R S] : Algebra.HasGoingDown R S := by
   apply of_comap_localRingHom_surjective
   intro P hP
+  let := Localization.AtPrime.algebraOfLiesOver (P.under R) P
   have : IsLocalHom (algebraMap (Localization.AtPrime <| P.under R) (Localization.AtPrime P)) := by
     rw [RingHom.algebraMap_toAlgebra]
     exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over

Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

@@ -145,15 +145,20 @@ lemma Ideal.surjectiveOnStalks_residueField (I : Ideal R) [I.IsPrime] :
   (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective).comp
     (RingHom.surjectiveOnStalks_of_isLocalization I.primeCompl _)
 
-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 _ _)
+instance (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p]
+    [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
+    [Localization.AtPrime.IsLiesOverAlgebra p q] :
+    IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) := by
+  rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]
+  exact Localization.isLocalHom_localRingHom _ _ _ (Ideal.over_def _ _)
 
 instance (p : Ideal R) [p.IsPrime] : Algebra.EssFiniteType R p.ResidueField :=
   .comp _ (Localization.AtPrime p) _
 
 instance [Algebra.EssFiniteType R A]
-    (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p] :
+    (p : Ideal R) [p.IsPrime] (q : Ideal A) [q.IsPrime] [q.LiesOver p]
+    [Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
+    [Localization.AtPrime.IsLiesOverAlgebra p q] :
     Algebra.EssFiniteType p.ResidueField q.ResidueField := by
   have : Algebra.EssFiniteType R q.ResidueField := .comp _ A _
   refine .of_comp R _ _