feat(Algebra/Category/Ring): Under.pushout preserves finite limits for properties with stable equalizers (#39572)

We introduce a predicate `RingHom.HasStableEqualizers` for properties of ring homomorphisms: This is satisfied for `P` if base change along *arbitrary* ring homomorphisms preserves the equalizer of any two algebra maps between algebras satisfying `P`. In a follow-up PR we will show that finite étale ring homomorphisms satisfy this predicate.

We relate `RingHom.HasStableEqualizers` to preservation of finite limits in `P.Under R` for `R : CommRingCat`.

From Pi1.

Author: chrisflav

Mathlib/Algebra/Category/Ring/Under/Basic.lean

@@ -80,7 +80,7 @@ def toUnder {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
 @[simp]
 lemma toUnder_right {A B : Type u} [CommRing A] [CommRing B] [Algebra R A]
     [Algebra R B] (f : A →ₐ[R] B) (a : A) :
-    f.toUnder.right a = f a :=
+    Under.Hom.right f.toUnder a = f a :=
   rfl
 
 @[simp]
@@ -130,7 +130,7 @@ variable [Algebra R S]
 
 variable (R S) in
 /-- The base change functor `A ↦ S ⊗[R] A`. -/
-@[simps! map_right]
+@[simps! obj_right map_right]
 def tensorProd : Under R ⥤ Under S where
   obj A := mkUnder S (S ⊗[R] A)
   map f := Algebra.TensorProduct.map (AlgHom.id S S) (toAlgHom f) |>.toUnder

Mathlib/Algebra/Category/Ring/Under/Property.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Category.Ring.Under.Limits
 public import Mathlib.CategoryTheory.Limits.MorphismProperty
 public import Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
+public import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
 
 /-!
 # Properties of `P.Under ⊤ R` for `R : CommRingCat`
@@ -19,6 +20,8 @@ In this file we translate ring theoretic properties of a property of ring homomo
 
 - `CommRingCat.Under.hasFiniteLimits`: If `P` is stable under finite products and equalizers,
   `P.Under ⊤ R` has finite limits.
+- `RingHom.HasStableEqualizers.preservesFiniteLimits_pushout`: If `P` has stable equalizers,
+  base change along arbitrary morphisms preserve finite limits.
 -/
 
 @[expose] public section
@@ -80,6 +83,18 @@ lemma RingHom.HasFiniteProducts.hasFiniteProducts (hQi : RespectsIso Q) (hQp : H
   have := hQp.createsFiniteProductsForget hQi R
   exact CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)
 
+lemma RingHom.HasFiniteProducts.preservesFiniteProducts_pushout (hQi : RingHom.RespectsIso Q)
+    (hQp : RingHom.HasFiniteProducts Q) [(toMorphismProperty Q).IsStableUnderCobaseChange]
+    {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    PreservesFiniteProducts (Under.pushout (toMorphismProperty Q) ⊤ f) := by
+  have := hQp.createsFiniteProductsForget hQi R
+  refine ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩
+  have : PreservesLimit K (Under.pushout (toMorphismProperty Q) ⊤ f ⋙
+        Under.forget (toMorphismProperty Q) ⊤ S) := by
+    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
+    infer_instance
+  exact preservesLimit_of_reflects_of_preserves _ (MorphismProperty.Under.forget _ ⊤ S)
+
 /-- If `Q` is stable under equalizers, the inclusion from the subcategory of `Under R` defined
 by `Q` creates equalizers. -/
 @[implicit_reducible]
@@ -117,3 +132,74 @@ lemma Under.hasFiniteLimits (hQi : RingHom.RespectsIso Q)
   hasFiniteLimits_of_hasEqualizers_and_finite_products
 
 end CommRingCat
+
+variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)
+
+open RingHom
+
+variable {P}
+
+lemma CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective
+    {R S : CommRingCat.{u}} [Algebra R S] {A B : Under R} {f g : A ⟶ B} :
+    PreservesLimit (parallelPair f g) (tensorProd R S) ↔
+      Function.Bijective ((toAlgHom f).tensorEqualizer R S (toAlgHom g)) := by
+  let c : Fork f g := Under.equalizerFork f g
+  let hc : IsLimit c := Under.equalizerForkIsLimit f g
+  let ι : R.mkUnder (AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
+    (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder
+  let h' := (R.tensorProd S).map ι
+  have w' : h' ≫ (tensorProd R S).map f = h' ≫ (tensorProd R S).map g := by
+    simpa using congr((R.tensorProd S).map $(CommRingCat.Under.equalizer_comp f g))
+  let e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') :=
+    isLimitMapConeForkEquiv (tensorProd R S) (Under.equalizer_comp f g)
+  rw [preservesLimit_iff_isLimit_mapCone hc, e.nonempty_congr,
+    (Under.equalizerForkIsLimit _ _).nonempty_isLimit_iff_isIso_lift]
+  have heq : (Under.equalizerForkIsLimit _ _).lift (Fork.ofι h' w') =
+      (AlgHom.tensorEqualizer S S (toAlgHom f) (toAlgHom g)).toUnder ≫
+        Under.homMk (CommRingCat.ofHom (.id _)) := by
+    refine Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_
+    rw [Fork.IsLimit.lift_ι]
+    ext : 2
+    dsimp
+    ext x <;> rfl
+  rw [heq, ← isIso_iff_of_reflects_iso _ (CategoryTheory.Under.forget S),
+    ConcreteCategory.isIso_iff_bijective]
+  rfl
+
+lemma RingHom.HasStableEqualizers.preservesLimit_parallelPair_tensorProd
+    (hPse : HasStableEqualizers P) {R S : CommRingCat.{u}} [Algebra R S]
+    {A B : Under R} (f g : A ⟶ B) (hA : P A.hom.hom) (hB : P B.hom.hom) :
+    PreservesLimit (parallelPair f g) (CommRingCat.tensorProd R S) := by
+  rw [CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective]
+  exact hPse _ _ hA hB
+
+lemma RingHom.HasStableEqualizers.preservesEqualizers_pushout (hPi : RespectsIso P)
+    (hPe : HasEqualizers P) (hPse : HasStableEqualizers P)
+    [(toMorphismProperty P).IsStableUnderCobaseChange] {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    PreservesLimitsOfShape WalkingParallelPair (Under.pushout (toMorphismProperty P) ⊤ f) := by
+  refine ⟨fun {K} ↦ ?_⟩
+  have := hPe.createsLimitsWalkingParallelPair hPi R
+  algebraize [f.hom]
+  have : PreservesLimit (K ⋙ Under.forget (toMorphismProperty P) ⊤ R)
+      (CategoryTheory.Under.pushout f) := by
+    rw [← CommRingCat.ofHom_hom f,
+      ← preservesLimit_iff_of_natIso _ (CommRingCat.tensorProdIsoPushout R S),
+      ← preservesLimit_iff_of_iso_diagram _ (diagramIsoParallelPair _).symm]
+    exact hPse.preservesLimit_parallelPair_tensorProd _ _ ((K.obj _).prop) ((K.obj _).prop)
+  have : PreservesLimit K (Under.pushout (toMorphismProperty P) ⊤ f ⋙
+        Under.forget (toMorphismProperty P) ⊤ S) := by
+    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
+    infer_instance
+  exact preservesLimit_of_reflects_of_preserves _ (Under.forget _ ⊤ S)
+
+/-- If `P` is a property of ring homs that is stable under finite products and
+equalizers, and the latter are preserved by arbitrary base change,
+pushout along any ring homomorphism preserves finite limits. -/
+lemma RingHom.HasStableEqualizers.preservesFiniteLimits_pushout (hPi : RingHom.RespectsIso P)
+    (hPp : HasFiniteProducts P) (hPe : HasEqualizers P) (hPse : HasStableEqualizers P)
+    [(toMorphismProperty P).IsStableUnderCobaseChange] {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    PreservesFiniteLimits (Under.pushout (toMorphismProperty P) ⊤ f) :=
+  have := hPp.preservesFiniteProducts_pushout hPi f
+  have := hPse.preservesEqualizers_pushout hPi hPe f
+  have := CommRingCat.Under.hasFiniteLimits hPi hPp hPe
+  preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts _

Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

@@ -231,6 +231,10 @@ lemma preservesLimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K
     apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)
     exact Cone.ext (Iso.refl _)⟩
 
+lemma preservesLimit_iff_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) :
+    PreservesLimit K₁ F ↔ PreservesLimit K₂ F :=
+  ⟨fun _ ↦ preservesLimit_of_iso_diagram _ h, fun _ ↦ preservesLimit_of_iso_diagram _ h.symm⟩
+
 /-- Transfer preservation of a limit along a natural isomorphism in the functor. -/
 lemma preservesLimit_of_natIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesLimit K F] :
     PreservesLimit K G where
@@ -307,6 +311,10 @@ lemma preservesColimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K
     apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)
     exact Cocone.ext (Iso.refl _)⟩
 
+lemma preservesColimit_iff_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) :
+    PreservesColimit K₁ F ↔ PreservesColimit K₂ F :=
+  ⟨fun _ ↦ preservesColimit_of_iso_diagram _ h, fun _ ↦ preservesColimit_of_iso_diagram _ h.symm⟩
+
 /-- Transfer preservation of a colimit along a natural isomorphism in the functor. -/
 lemma preservesColimit_of_natIso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [PreservesColimit K F] :
     PreservesColimit K G where

Mathlib/CategoryTheory/MorphismProperty/Limits.lean

@@ -131,11 +131,17 @@ as `f`, the pullback of that morphism along `f` exists. -/
 protected class HasPullbacksAlong {X Y : C} (f : X ⟶ Y) : Prop where
   hasPullback {W} (g : W ⟶ Y) : P g → HasPullback g f
 
+instance {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] : P.HasPullbacksAlong f where
+  hasPullback _ _ := inferInstance
+
 /-- `P.HasPushoutsAlong f` states that for any morphism satisfying `P` with the same domain
 as `f`, the pushout of that morphism along `f` exists. -/
 protected class HasPushoutsAlong {X Y : C} (f : X ⟶ Y) : Prop where
   hasPushout {W} (g : X ⟶ W) : P g → HasPushout g f
 
+instance {X Y : C} (f : X ⟶ Y) [HasPushoutsAlong f] : P.HasPushoutsAlong f where
+  hasPushout _ _ := inferInstance
+
 /-- `P.IsStableUnderBaseChangeAlong f` states that for any morphism satisfying `P` with the same
 codomain as `f`, any pullback of that morphism along `f` also satisfies `P`. -/
 class IsStableUnderBaseChangeAlong {X Y : C} (f : X ⟶ Y) : Prop where

Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean

@@ -157,6 +157,15 @@ noncomputable def Over.pullbackMapHomPullback [P.IsStableUnderComposition]
     Over.homMk (pullback.map _ _ _ _ (𝟙 A.left) f (𝟙 Z) (by simp) (by cat_disch))
     (by simp) (Q.pullbackMap (Q.id_mem _) hQf (by simp) (by cat_disch))
 
+/-- `MorphismProperty.Over.pullback` commutes with `MorphismProperty.Over.forget`. -/
+@[simps!]
+noncomputable
+def Over.pullbackCompForgetIso {X Y : T} (f : X ⟶ Y) [HasPullbacksAlong f]
+    [P.IsStableUnderBaseChangeAlong f] [Q.IsStableUnderBaseChange] :
+    Over.pullback P Q f ⋙ Over.forget _ _ _ ≅
+      Over.forget _ _ _ ⋙ CategoryTheory.Over.pullback f :=
+  Iso.refl _
+
 end Pullback
 
 section Adjunction
@@ -297,6 +306,15 @@ lemma Under.pushoutCongr_hom_app_left_fst {f : X ⟶ Y} [P.HasPushoutsAlong f] {
   subst h
   simp [pushoutCongr]
 
+/-- `MorphismProperty.Under.pushout` commutes with `MorphismProperty.Under.forget`. -/
+@[simps!]
+noncomputable
+def Under.pushoutCompForgetIso {X Y : T} (f : X ⟶ Y) [HasPushoutsAlong f]
+    [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] :
+    Under.pushout P Q f ⋙ Under.forget _ _ _ ≅
+      Under.forget _ _ _ ⋙ CategoryTheory.Under.pushout f :=
+  Iso.refl _
+
 end Pushout
 
 section Adjunction

Mathlib/RingTheory/Flat/Equalizer.lean

@@ -351,3 +351,18 @@ lemma Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply [Module.Flat R T]
       x ⊗ₜ (y * z.1) := rfl
 
 end Algebra
+
+namespace RingHom
+
+/--
+A property `P` of ring homomorphisms is said to have stable equalizers, if the equalizer
+of algebra maps between algebras with structure morphisms satisfying `P`, is preserved by
+arbitrary base change.
+-/
+def HasStableEqualizers (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop) : Prop :=
+  ∀ {R S A B : Type u} [CommRing R] [CommRing S] [CommRing A] [CommRing B]
+    [Algebra R A] [Algebra R S] [Algebra R B]
+    (f g : A →ₐ[R] B), P (algebraMap R A) → P (algebraMap R B) →
+    Function.Bijective (f.tensorEqualizer R S g)
+
+end RingHom