feat(Algebra/Category): P.Under ⊤ R has finite limits if P is stable under finite products and equalizers

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

@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.AlgebraicGeometry.Morphisms.Etale
+import Mathlib.AlgebraicGeometry.Morphisms.Finite
+import Mathlib.CategoryTheory.Limits.MorphismProperty
+import Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
+import Mathlib.CategoryTheory.MorphismProperty.Limits
+import Mathlib.RingTheory.Smooth.StandardSmoothCotangent
+import Mathlib.CategoryTheory.Limits.MorphismProperty
+
+/-!
+# Properties of `P.Under ⊤ R` for `R : CommRingCat`
+
+In this file we show properties of the category of commutative rings under `R` where
+the structure map satisfies some property `P`.
+
+## Main results
+
+- ``
+
+-/
+
+universe u
+
+open CategoryTheory Limits
+
+namespace RingHom
+
+variable {Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
+
+/-- A property of ring homomorphisms `Q` is said to have equalizers, if the equalizer of algebra
+maps between algebras satisfiying `Q` also satisfies `Q`. -/
+def HasEqualizers (Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop) : Prop :=
+  ∀ {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
+    (f g : S →ₐ[R] T), Q (algebraMap R S) → Q (algebraMap R T) →
+      Q (algebraMap R (AlgHom.equalizer f g))
+
+/-- A property of ring homomorphisms `Q` is said to have finite products, if a finite product of
+algebras satisfiying `Q` also satisfies `Q`. -/
+def HasFiniteProducts (Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop) : Prop :=
+  ∀ {R : Type u} [CommRing R] {ι : Type u} [_root_.Finite ι] (S : ι → Type u) [∀ i, CommRing (S i)]
+    [∀ i, Algebra R (S i)],
+    (∀ i, Q (algebraMap R (S i))) → Q (algebraMap R (Π i, S i))
+
+--lemma HasFiniteProducts.of_finite (h : HasFiniteProducts Q) {R : Type u} [CommRing R] {ι : Type u}
+--    [_root_.Finite ι] (S : ι → Type u) [∀ i, CommRing (S i)] [∀ i, Algebra R (S i)]
+--    (H : ∀ i, Q (algebraMap R (S i))) :
+--    Q (algebraMap R (Π i, S i)) := by
+--  sorry
+
+end RingHom
+
+namespace CommRingCat
+
+variable {Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
+
+open MorphismProperty
+
+variable (J : Type) [SmallCategory J] [FinCategory J]
+
+set_option backward.isDefEq.respectTransparency false in
+@[implicit_reducible]
+noncomputable def Under.createsFiniteProductsForget (hQi : RingHom.RespectsIso Q)
+    (hQp : RingHom.HasFiniteProducts Q) (R : CommRingCat.{u}) :
+    CreatesFiniteProducts (MorphismProperty.Under.forget (RingHom.toMorphismProperty Q) ⊤ R) := by
+  refine .mk' _ fun (J : Type u) _ ↦ ?_
+  have : (commaObj (Functor.fromPUnit R) (𝟭 _)
+      (RingHom.toMorphismProperty Q)).IsClosedUnderLimitsOfShape (Discrete J) := by
+    constructor
+    intro (A : Under R) ⟨(pres : LimitPresentation _ A), hpres⟩
+    let e : A ≅ CommRingCat.mkUnder R (Π i, pres.diag.obj ⟨i⟩) :=
+      (limit.isoLimitCone ⟨_, pres.isLimit⟩).symm ≪≫
+        HasLimit.isoOfNatIso (Discrete.natIso fun i ↦ eqToIso <| by simp) ≪≫
+        limit.isoLimitCone ⟨CommRingCat.Under.piFan <| fun i ↦ (pres.diag.obj ⟨i⟩),
+          CommRingCat.Under.piFanIsLimit <| fun i ↦ (pres.diag.obj ⟨i⟩)⟩
+    simp only [commaObj_iff, Functor.const_obj_obj, Functor.id_obj, ← Under.w e.inv]
+    have : (RingHom.toMorphismProperty Q).RespectsIso :=
+      RingHom.toMorphismProperty_respectsIso_iff.mp hQi
+    rw [MorphismProperty.cancel_right_of_respectsIso (P := RingHom.toMorphismProperty Q)]
+    exact hQp _ fun i ↦ hpres _
+  apply +allowSynthFailures (Comma.forgetCreatesLimitsOfShapeOfClosed _)
+
+lemma Under.hasFiniteProducts (hQi : RingHom.RespectsIso Q)
+    (hQp : RingHom.HasFiniteProducts Q) (R : CommRingCat.{u}) :
+    HasFiniteProducts ((RingHom.toMorphismProperty Q).Under ⊤ R) := by
+  refine ⟨fun n ↦ ⟨fun D ↦ ?_⟩⟩
+  have := CommRingCat.Under.createsFiniteProductsForget hQi hQp R
+  exact CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)
+
+set_option backward.isDefEq.respectTransparency false in
+@[implicit_reducible]
+noncomputable
+def Under.createsEqualizersForget (hQi : RingHom.RespectsIso Q)
+    (hQe : RingHom.HasEqualizers Q) (R : CommRingCat.{u}) :
+    CreatesLimitsOfShape WalkingParallelPair
+      (MorphismProperty.Under.forget (RingHom.toMorphismProperty Q) ⊤ R) := by
+  have :
+      (commaObj (Functor.fromPUnit R) (𝟭 _)
+        (RingHom.toMorphismProperty Q)).IsClosedUnderLimitsOfShape
+      WalkingParallelPair := by
+    constructor
+    intro (A : Under R) ⟨(pres : LimitPresentation _ A), hpres⟩
+    let e : A ≅
+        CommRingCat.mkUnder R
+          (AlgHom.equalizer (R := R)
+            (CommRingCat.toAlgHom (pres.diag.map .left))
+            (CommRingCat.toAlgHom (pres.diag.map .right))) :=
+      (limit.isoLimitCone ⟨_, pres.isLimit⟩).symm ≪≫
+        HasLimit.isoOfNatIso (diagramIsoParallelPair _) ≪≫ limit.isoLimitCone
+          ⟨CommRingCat.Under.equalizerFork (pres.diag.map .left) (pres.diag.map .right),
+            CommRingCat.Under.equalizerForkIsLimit
+              (pres.diag.map .left) (pres.diag.map .right)⟩
+    have := Under.w e.inv
+    simp only [commaObj_iff, Functor.const_obj_obj, Functor.id_obj]
+    rw [← this]
+    have : (RingHom.toMorphismProperty Q).RespectsIso :=
+      RingHom.toMorphismProperty_respectsIso_iff.mp hQi
+    rw [MorphismProperty.cancel_right_of_respectsIso (P := RingHom.toMorphismProperty Q)]
+    exact hQe _ _ (hpres .zero) (hpres .one)
+  apply Comma.forgetCreatesLimitsOfShapeOfClosed
+
+@[implicit_reducible]
+noncomputable
+def Under.createsFiniteLimitsForget (hQi : RingHom.RespectsIso Q)
+    (hQp : RingHom.HasFiniteProducts Q) (hQe : RingHom.HasEqualizers Q) (R : CommRingCat.{u}) :
+    CreatesFiniteLimits (Under.forget (RingHom.toMorphismProperty Q) ⊤ R) := by
+  have := CommRingCat.Under.createsFiniteProductsForget hQi hQp
+  have := CommRingCat.Under.createsEqualizersForget hQi hQe
+  apply createsFiniteLimitsOfCreatesEqualizersAndFiniteProducts
+
+lemma Under.hasEqualizers (hQi : RingHom.RespectsIso Q)
+    (hQe : RingHom.HasEqualizers Q) (R : CommRingCat.{u}) :
+    HasEqualizers ((RingHom.toMorphismProperty Q).Under ⊤ R) := by
+  refine ⟨fun D ↦ ?_⟩
+  have := CommRingCat.Under.createsEqualizersForget hQi hQe R
+  exact CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)
+
+lemma Under.hasFiniteLimits (hQi : RingHom.RespectsIso Q)
+    (hQp : RingHom.HasFiniteProducts Q) (hQe : RingHom.HasEqualizers Q) (R : CommRingCat.{u}) :
+    HasFiniteLimits ((RingHom.toMorphismProperty Q).Under ⊤ R) :=
+  have := CommRingCat.Under.hasFiniteProducts hQi hQp
+  have := CommRingCat.Under.hasEqualizers hQi hQe
+  hasFiniteLimits_of_hasEqualizers_and_finite_products
+
+set_option backward.isDefEq.respectTransparency false in
+lemma Under.property_limit_of_hasFiniteProducts_of_hasEqualizers
+    (hQi : RingHom.RespectsIso Q) (hQp : RingHom.HasFiniteProducts Q)
+    (hQe : RingHom.HasEqualizers Q)
+    {R : CommRingCat.{u}} (D : J ⥤ Under R) (h : ∀ j, Q (D.obj j).hom.hom) :
+    Q (limit D).hom.hom := by
+  have := CommRingCat.Under.hasFiniteLimits hQi hQp hQe
+  let D' : J ⥤ (RingHom.toMorphismProperty Q).Under ⊤ R :=
+    MorphismProperty.Comma.lift D h (by simp) (by simp)
+  let A := limit D'
+  have : CreatesFiniteLimits (Under.forget (RingHom.toMorphismProperty Q) ⊤ R) :=
+    CommRingCat.Under.createsFiniteLimitsForget hQi hQp hQe R
+  let e : (Under.forget _ _ R).obj A ≅ limit D :=
+    preservesLimitIso (Under.forget (RingHom.toMorphismProperty Q) ⊤ R) D'
+  have := CategoryTheory.Under.w e.hom
+  rw [← this, CommRingCat.hom_comp, hQi.cancel_right_isIso]
+  exact A.prop
+
+end CommRingCat

Mathlib/CategoryTheory/Limits/Comma.lean

@@ -215,6 +215,9 @@ namespace StructuredArrow
 
 variable {X : T} {G : A ⥤ T} (F : J ⥤ StructuredArrow X G)
 
+instance [G.Faithful] [G.Full] {Y : A} : HasInitial (StructuredArrow (G.obj Y) G) :=
+  StructuredArrow.mkIdInitial.hasInitial
+
 set_option backward.isDefEq.respectTransparency false in
 instance hasLimit [i₁ : HasLimit (F ⋙ proj X G)] [i₂ : PreservesLimit (F ⋙ proj X G) G] :
     HasLimit F := by
@@ -307,4 +310,10 @@ instance {X : T} : HasTerminal (Over X) := CostructuredArrow.hasTerminal
 
 end Over
 
+namespace Under
+
+instance {X : T} : HasInitial (Under X) := Under.mkIdInitial.hasInitial
+
+end Under
+
 end CategoryTheory

Mathlib/CategoryTheory/Limits/Constructions/Over/Basic.lean

@@ -48,4 +48,16 @@ instance hasLimits {B : C} [HasWidePullbacks.{w} C] : HasLimitsOfSize.{w, w} (Ov
   have := ConstructProducts.over_products_of_widePullbacks (B := B)
   apply has_limits_of_hasEqualizers_and_products
 
-end CategoryTheory.Over
+end Over
+
+namespace Under
+
+instance {B : C} [HasFiniteWidePushouts C] : HasFiniteColimits (Under B) := by
+  rw [← hasFiniteLimits_opposite_iff]
+  exact hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Over.opEquivOpUnder _).inverse
+
+instance {B : C} [HasWidePushouts.{w} C] : HasColimitsOfSize.{w, w} (Under B) := by
+  rw [← hasLimitsOfSize_opposite_iff]
+  exact hasLimits_of_hasLimits_createsLimits (Over.opEquivOpUnder _).inverse
+
+end CategoryTheory.Under

Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

@@ -5,7 +5,7 @@ Authors: Johan Commelin, Reid Barton, Bhavik Mehta
 -/
 module
 
-public import Mathlib.CategoryTheory.Limits.Creates
+public import Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
 public import Mathlib.CategoryTheory.Comma.Over.Basic
 public import Mathlib.CategoryTheory.IsConnected
 public import Mathlib.CategoryTheory.Filtered.Final
@@ -115,6 +115,29 @@ instance hasLimitsOfShape_of_isConnected {B : D} [IsConnected J] [HasLimitsOfSha
 
 end CostructuredArrow
 
+namespace StructuredArrow
+
+/-- The projection from `StructuredArrow K B` to `C` creates any connected colimit. -/
+instance [IsConnected J] {B : D} : CreatesColimitsOfShape J (StructuredArrow.proj B K) :=
+  letI : CreatesLimitsOfShape Jᵒᵖ (proj B K).op :=
+    inferInstanceAs <| CreatesLimitsOfShape Jᵒᵖ <|
+      (structuredArrowOpEquivalence K B).functor ⋙ CostructuredArrow.proj K.op (.op B)
+  createsColimitsOfShapeOfOp _ _
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The forgetful functor from `StructuredArrow K B` preserves any connected colimit. -/
+instance [IsConnected J] {B : D} : PreservesColimitsOfShape J (StructuredArrow.proj B K) := by
+  have : PreservesLimitsOfShape Jᵒᵖ (proj B K).op :=
+    inferInstanceAs <| PreservesLimitsOfShape Jᵒᵖ <|
+      (structuredArrowOpEquivalence K B).functor ⋙ CostructuredArrow.proj K.op (.op B)
+  apply preservesColimitsOfShape_of_op
+
+instance {B : D} [IsConnected J] [HasColimitsOfShape J C] :
+    HasColimitsOfShape J (StructuredArrow B K) where
+  has_colimit F := hasColimit_of_created F (StructuredArrow.proj B K)
+
+end StructuredArrow
+
 namespace Over
 
 /-- The forgetful functor from the over category creates any connected limit. -/
@@ -160,4 +183,23 @@ def isLimitConePost [IsCofilteredOrEmpty J] {F : J ⥤ C} {c : Cone F} (i : J) (
   isLimitOfReflects (Over.forget _)
     ((Functor.Initial.isLimitWhiskerEquiv (Over.forget i) c).symm hc)
 
-end CategoryTheory.Over
+end Over
+
+namespace Under
+
+/-- The forgetful functor from the under category creates any connected limit. -/
+instance createsColimitsOfShapeForgetOfIsConnected [IsConnected J] {B : C} :
+    CreatesColimitsOfShape J (forget B) :=
+  inferInstanceAs <| CreatesColimitsOfShape J (StructuredArrow.proj _ _)
+
+/-- The forgetful functor from the under category preserves any connected limit. -/
+instance preservesColimitsOfShape_forget_of_isConnected [IsConnected J] {B : C} :
+    PreservesColimitsOfShape J (forget B) :=
+  inferInstanceAs <| PreservesColimitsOfShape J (StructuredArrow.proj _ _)
+
+/-- The under category has any connected limit which the original category has. -/
+instance hasColimitsOfShape_of_isConnected {B : C} [IsConnected J] [HasColimitsOfShape J C] :
+    HasColimitsOfShape J (Under B) where
+  has_colimit F := hasColimit_of_created F (forget B)
+
+end CategoryTheory.Under