diff --git a/Mathlib/Algebra/Category/Ring/Under/Property.lean b/Mathlib/Algebra/Category/Ring/Under/Property.lean
new file mode 100644
index 00000000000000..00b6c4c0bd68e1
--- /dev/null
+++ b/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
diff --git a/Mathlib/CategoryTheory/Limits/Comma.lean b/Mathlib/CategoryTheory/Limits/Comma.lean
index 608ea1f9d9ab61..eb96984ed717f6 100644
--- a/Mathlib/CategoryTheory/Limits/Comma.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Over/Basic.lean b/Mathlib/CategoryTheory/Limits/Constructions/Over/Basic.lean
index dffa5d9d8e6c02..a7e4295e6cdf07 100644
--- a/Mathlib/CategoryTheory/Limits/Constructions/Over/Basic.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean b/Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean
index be3afb7e07be3d..fc04268734e34b 100644
--- a/Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Limits/MorphismProperty.lean b/Mathlib/CategoryTheory/Limits/MorphismProperty.lean
index f18e6287591f8b..14ba72737e2e6c 100644
--- a/Mathlib/CategoryTheory/Limits/MorphismProperty.lean
+++ b/Mathlib/CategoryTheory/Limits/MorphismProperty.lean
@@ -132,6 +132,44 @@ end
 
 section
 
+variable {A : Type*} [Category* A] {L : A ⥤ T}
+
+instance StructuredArrow.closedUnderColimitsOfShape_discrete_empty [L.Faithful] [L.Full] {Y : A}
+    [P.ContainsIdentities] [P.RespectsIso] :
+    (P.structuredArrowObj L (X := L.obj Y)).IsClosedUnderColimitsOfShape (Discrete PEmpty.{1}) where
+  colimitsOfShape_le := by
+    rintro X ⟨p⟩
+    let e : X ≅ StructuredArrow.mk (𝟙 (L.obj Y)) :=
+      p.isColimit.coconePointUniqueUpToIso ((IsColimit.precomposeInvEquiv
+        (Functor.emptyExt _ _) _).2 StructuredArrow.mkIdInitial)
+    rw [MorphismProperty.structuredArrowObj_iff,
+      P.structuredArrow_iso_iff e]
+    simpa using P.id_mem (L.obj Y)
+
+set_option backward.isDefEq.respectTransparency false in
+lemma StructuredArrow.isClosedUnderLimitsOfShape {J : Type*} [Category* J]
+    {P : MorphismProperty T} [P.RespectsIso] [PreservesLimitsOfShape J L] [HasLimitsOfShape J A]
+    (c : ∀ (D : J ⥤ T) [HasLimit D], Cone D)
+    (hc : ∀ (D : J ⥤ T) [HasLimit D], IsLimit (c D))
+    (H : ∀ (D : J ⥤ T) [HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
+      (∀ j, P (s.app j)) → P ((hc D).lift (Cone.mk X s))) (X : T) :
+    (P.structuredArrowObj L (X := X)).IsClosedUnderLimitsOfShape J where
+  limitsOfShape_le Y := by
+    intro ⟨d⟩
+    let hd : IsLimit ((CategoryTheory.StructuredArrow.proj X L ⋙ L).mapCone d.cone) :=
+      isLimitOfPreserves _ d.isLimit
+    have heq : Y.hom = hd.lift { pt := X, π := { app j := (d.diag.obj j).hom } } := by
+      refine hd.hom_ext fun j ↦ ?_
+      simp only [Functor.const_obj_obj, IsLimit.fac]
+      simp
+    rw [P.structuredArrowObj_iff, heq, ← (hc _).lift_comp_conePointUniqueUpToIso_hom hd,
+      P.cancel_right_of_respectsIso]
+    exact H _ _ d.prop_diag_obj
+
+end
+
+section
+
 variable {X : T}
 
 instance Over.closedUnderLimitsOfShape_discrete_empty [P.ContainsIdentities] [P.RespectsIso] :
@@ -159,6 +197,28 @@ instance Over.closedUnderLimitsOfShape_pullback [HasPullbacks T]
 
 end
 
+section
+
+variable {X : T}
+
+instance Under.closedUnderColimitsOfShape_discrete_empty [P.ContainsIdentities] [P.RespectsIso] :
+    (P.underObj (X := X)).IsClosedUnderColimitsOfShape (Discrete PEmpty.{1}) :=
+  StructuredArrow.closedUnderColimitsOfShape_discrete_empty (L := 𝟭 _) P
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Let `P` be stable under composition and cobase change. If `P` satisfies cancellation on the
+left, the subcategory of `Under X` defined by `P` is closed under pushouts. -/
+instance Under.closedUnderColimitsOfShape_pushout [HasPushouts T]
+    [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] :
+    (P.underObj (X := X)).IsClosedUnderColimitsOfShape WalkingSpan := by
+  rw [ObjectProperty.isClosedUnderColimitsOfShape_iff_op, ←
+    ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff _ _ (Over.opEquivOpUnder _),
+    MorphismProperty.inverseImage_op_underObj,
+    ObjectProperty.isClosedUnderLimitsOfShape_iff_of_equivalence _ walkingSpanOpEquiv]
+  infer_instance
+
+end
+
 namespace MorphismProperty.Over
 
 variable (X : T)
@@ -228,4 +288,60 @@ instance {X Y : T} (f : X ⟶ Y) : PreservesFiniteLimits (pullback P ⊤ f) wher
 
 end MorphismProperty.Over
 
+namespace MorphismProperty.Under
+
+variable (X : T)
+
+noncomputable instance [P.ContainsIdentities] [P.RespectsIso] :
+    CreatesColimitsOfShape (Discrete PEmpty.{1}) (Under.forget P ⊤ X) := by
+  apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed
+  · exact inferInstanceAs (HasColimitsOfShape _ (Under X))
+  · apply Under.closedUnderColimitsOfShape_discrete_empty _
+
+set_option backward.isDefEq.respectTransparency false in
+variable {X} in
+instance [P.ContainsIdentities] (Y : P.Under ⊤ X) :
+    Unique (Under.mk ⊤ (𝟙 X) (P.id_mem X) ⟶ Y) where
+  default := Under.homMk Y.hom (by simp)
+  uniq a := by ext; simp [← Under.w a]
+
+/-- `X ⟶ X` is the initial object of `P.Under ⊤ X`. -/
+def mkIdInitial [P.ContainsIdentities] :
+    IsInitial (Under.mk ⊤ (𝟙 X) (P.id_mem X)) :=
+  .ofUnique _
+
+instance [P.ContainsIdentities] : HasInitial (P.Under ⊤ X) :=
+  (Under.mkIdInitial P X).hasInitial
+
+/-- If `P` is stable under composition, cobase change and satisfies pre-cancellation,
+`Under.forget P ⊤ X` creates pushouts. -/
+noncomputable instance createsLimitsOfShape_walkingCospan [HasPushouts T]
+    [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] :
+    CreatesColimitsOfShape WalkingSpan (Under.forget P ⊤ X) := by
+  apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed
+  · exact inferInstanceAs (HasColimitsOfShape WalkingSpan (Under X))
+  · apply Under.closedUnderColimitsOfShape_pushout
+
+/-- If `P` is stable under composition, cobase change and satisfies pre-cancellation,
+`P.Under ⊤ X` has pushouts. -/
+instance (priority := 900) [HasPushouts T] [P.IsStableUnderComposition]
+    [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] : HasPushouts (P.Under ⊤ X) := by
+  apply +allowSynthFailures hasColimitsOfShape_of_closedUnderColimitsOfShape
+  · exact inferInstanceAs (HasColimitsOfShape WalkingSpan (Under X))
+  · apply Under.closedUnderColimitsOfShape_pushout
+
+variable [HasPushouts T] [P.IsStableUnderComposition] [P.ContainsIdentities]
+  [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P]
+
+noncomputable instance : CreatesFiniteColimits (Under.forget P ⊤ X) :=
+  createsFiniteColimitsOfCreatesInitialAndPushouts _
+
+instance [HasFiniteWidePushouts T] : HasFiniteColimits (P.Under ⊤ X) :=
+  hasFiniteColimits_of_hasColimits_of_createsFiniteColimits (Under.forget P ⊤ X)
+
+instance : PreservesFiniteColimits (Under.forget P ⊤ X) :=
+  preservesFiniteColimits_of_preservesInitial_and_pushouts (Under.forget P ⊤ X)
+
+end MorphismProperty.Under
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Limits/Opposites.lean b/Mathlib/CategoryTheory/Limits/Opposites.lean
index 0de70d2d51197b..c3e0cbc600ad75 100644
--- a/Mathlib/CategoryTheory/Limits/Opposites.lean
+++ b/Mathlib/CategoryTheory/Limits/Opposites.lean
@@ -18,7 +18,7 @@ We construct limits and colimits in the opposite categories.
 @[expose] public section
 
 
-universe v₁ v₂ u₁ u₂
+universe w v₁ v₂ u₁ u₂
 
 noncomputable section
 
@@ -509,12 +509,26 @@ theorem hasColimits_of_hasLimits_op [HasLimitsOfSize.{v₂, u₂} Cᵒᵖ] :
     HasColimitsOfSize.{v₂, u₂} C :=
   { has_colimits_of_shape := fun _ _ => hasColimitsOfShape_of_hasLimitsOfShape_op }
 
+lemma hasColimitsOfSize_opposite_iff :
+    HasColimitsOfSize.{v₂, u₂} Cᵒᵖ ↔ HasLimitsOfSize.{v₂, u₂} C :=
+  ⟨fun _ ↦ hasLimits_of_hasColimits_op, fun _ ↦ inferInstance⟩
+
+lemma hasLimitsOfSize_opposite_iff :
+    HasLimitsOfSize.{v₂, u₂} Cᵒᵖ ↔ HasColimitsOfSize.{v₂, u₂} C :=
+  ⟨fun _ ↦ hasColimits_of_hasLimits_op, fun _ ↦ inferInstance⟩
+
 instance hasFiniteColimits_opposite [HasFiniteLimits C] : HasFiniteColimits Cᵒᵖ :=
   ⟨fun _ _ _ => hasColimitsOfShape_op_of_hasLimitsOfShape⟩
 
 instance hasFiniteLimits_opposite [HasFiniteColimits C] : HasFiniteLimits Cᵒᵖ :=
   ⟨fun _ _ _ => hasLimitsOfShape_op_of_hasColimitsOfShape⟩
 
+lemma hasFiniteLimits_opposite_iff : HasFiniteLimits Cᵒᵖ ↔ HasFiniteColimits C :=
+  ⟨fun _ ↦ ⟨fun _ _ _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op⟩, fun _ ↦ inferInstance⟩
+
+lemma hasFiniteColimits_opposite_iff : HasFiniteColimits Cᵒᵖ ↔ HasFiniteLimits C :=
+  ⟨fun _ ↦ ⟨fun _ _ _ ↦ hasLimitsOfShape_of_hasColimitsOfShape_op⟩, fun _ ↦ inferInstance⟩
+
 lemma hasColimit_op_iff_hasLimit {F : J ⥤ C} : HasColimit F.op ↔ HasLimit F :=
   ⟨fun _ ↦ hasLimit_of_hasColimit_op F, fun _ ↦ inferInstance⟩
 
@@ -533,4 +547,70 @@ lemma hasLimit_leftOp_iff_hasColimit {F : J ⥤ Cᵒᵖ} : HasLimit F.leftOp ↔
 lemma hasLimit_rightOp_iff_hasColimit {F : Jᵒᵖ ⥤ C} : HasLimit F.rightOp ↔ HasColimit F :=
   ⟨fun _ ↦ hasColimit_of_hasLimit_rightOp F, fun _ ↦ inferInstance⟩
 
+lemma hasLimitsOfShape_opposite_iff : HasLimitsOfShape J Cᵒᵖ ↔ HasColimitsOfShape Jᵒᵖ C := by
+  refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
+  have : HasLimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
+  exact hasColimitsOfShape_of_hasLimitsOfShape_op
+
+lemma hasColimitsOfShape_opposite_iff : HasColimitsOfShape J Cᵒᵖ ↔ HasLimitsOfShape Jᵒᵖ C := by
+  refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
+  have : HasColimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
+  exact hasLimitsOfShape_of_hasColimitsOfShape_op
+
+lemma hasLimitsOfShape_opposite_opposite_iff :
+    HasLimitsOfShape Jᵒᵖ Cᵒᵖ ↔ HasColimitsOfShape J C := by
+  refine ⟨fun _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op, fun _ ↦ ?_⟩
+  have : HasColimitsOfShape Jᵒᵖᵒᵖ C := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
+  exact hasLimitsOfShape_op_of_hasColimitsOfShape
+
+lemma hasColimitsOfShape_opposite_opposite_iff :
+    HasColimitsOfShape Jᵒᵖ Cᵒᵖ ↔ HasLimitsOfShape J C := by
+  refine ⟨fun _ ↦ hasLimitsOfShape_of_hasColimitsOfShape_op, fun _ ↦ ?_⟩
+  have : HasLimitsOfShape Jᵒᵖᵒᵖ C := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
+  exact hasColimitsOfShape_op_of_hasLimitsOfShape
+
+instance [HasWidePullbacks.{w} C] : HasWidePushouts.{w} Cᵒᵖ := by
+  intro ι
+  rw [hasColimitsOfShape_opposite_iff]
+  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm
+
+instance [HasWidePushouts.{w} C] : HasWidePullbacks.{w} Cᵒᵖ := by
+  intro ι
+  rw [hasLimitsOfShape_opposite_iff]
+  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm
+
+lemma hasWidePullbacks_opposite_iff :
+    HasWidePullbacks.{w} Cᵒᵖ ↔ HasWidePushouts.{w} C := by
+  refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
+  rw [← hasLimitsOfShape_opposite_opposite_iff]
+  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm
+
+lemma hasWidePushouts_opposite_iff :
+    HasWidePushouts.{w} Cᵒᵖ ↔ HasWidePullbacks.{w} C := by
+  refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
+  rw [← hasColimitsOfShape_opposite_opposite_iff]
+  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm
+
+instance [HasFiniteWidePullbacks C] : HasFiniteWidePushouts Cᵒᵖ := by
+  refine ⟨fun J _ ↦ ?_⟩
+  rw [hasColimitsOfShape_opposite_iff]
+  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm
+
+instance [HasFiniteWidePushouts C] : HasFiniteWidePullbacks Cᵒᵖ := by
+  refine ⟨fun J _ ↦ ?_⟩
+  rw [hasLimitsOfShape_opposite_iff]
+  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm
+
+lemma hasFiniteWidePullbacks_opposite_iff :
+    HasFiniteWidePullbacks Cᵒᵖ ↔ HasFiniteWidePushouts C := by
+  refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
+  rw [← hasLimitsOfShape_opposite_opposite_iff]
+  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm
+
+lemma hasFiniteWidePushouts_opposite_iff :
+    HasFiniteWidePushouts Cᵒᵖ ↔ HasFiniteWidePullbacks C := by
+  refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
+  rw [← hasColimitsOfShape_opposite_opposite_iff]
+  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm
+
 end CategoryTheory.Limits
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean b/Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean
index 98e5c63fb67bfa..67d93ec1b09e3f 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean
@@ -101,6 +101,14 @@ attribute [instance_reducible, instance] CreatesFiniteProducts.creates
 
 noncomputable section
 
+/-- The condition of `CreatesFiniteProducts` can be checked for finite types in an arbitrary
+universe. -/
+@[implicit_reducible]
+def CreatesFiniteProducts.mk' (F : C ⥤ D)
+    (H : ∀ (J : Type w) [Fintype J], CreatesLimitsOfShape (Discrete J) F) :
+    CreatesFiniteProducts F where
+  creates _ _ := createsLimitsOfShapeOfEquiv (Discrete.equivalence Equiv.ulift.{w}) F
+
 instance (priority := 100) createsLimitsOfShapeOfCreatesFiniteProducts (F : C ⥤ D)
     [CreatesFiniteProducts F] (J : Type w) [Finite J] : CreatesLimitsOfShape (Discrete J) F :=
   createsLimitsOfShapeOfEquiv
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Comma.lean b/Mathlib/CategoryTheory/MorphismProperty/Comma.lean
index 71d9e0b12f0d68..4017e2aeb34d49 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/Comma.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/Comma.lean
@@ -6,6 +6,7 @@ Authors: Christian Merten
 module
 
 public import Mathlib.CategoryTheory.Comma.Over.Basic
+public import Mathlib.CategoryTheory.ObjectProperty.Opposite
 public import Mathlib.CategoryTheory.MorphismProperty.Composition
 public import Mathlib.CategoryTheory.MorphismProperty.Factorization
 
@@ -51,10 +52,19 @@ lemma costructuredArrow_iso_iff (P : MorphismProperty T) [P.RespectsIso]
     P f.hom ↔ P g.hom :=
   P.comma_iso_iff e
 
+lemma structuredArrow_iso_iff (P : MorphismProperty T) [P.RespectsIso]
+    {L : A ⥤ T} {X : T} {f g : StructuredArrow X L} (e : f ≅ g) :
+    P f.hom ↔ P g.hom :=
+  P.comma_iso_iff e
+
 lemma over_iso_iff (P : MorphismProperty T) [P.RespectsIso] {X : T} {f g : Over X} (e : f ≅ g) :
     P f.hom ↔ P g.hom :=
   P.comma_iso_iff e
 
+lemma under_iso_iff (P : MorphismProperty T) [P.RespectsIso] {X : T} {f g : Under X} (e : f ≅ g) :
+    P f.hom ↔ P g.hom :=
+  P.comma_iso_iff e
+
 section
 
 variable {W : MorphismProperty T} {X : T}
@@ -122,6 +132,14 @@ def underObj (W : MorphismProperty T) {X : T} : ObjectProperty (Under X) := fun
 instance [W.RespectsIso] : (W.underObj (X := X)).IsClosedUnderIsomorphisms :=
   inferInstanceAs <| (W.commaObj _ _).IsClosedUnderIsomorphisms
 
+@[simp]
+lemma inverseImage_op_overObj (W : MorphismProperty T) {X : T} :
+    W.overObj.op.inverseImage (Under.opEquivOpOver X).functor = W.op.underObj := rfl
+
+@[simp]
+lemma inverseImage_op_underObj (W : MorphismProperty T) {X : T} :
+    W.underObj.op.inverseImage (Over.opEquivOpUnder X).functor = W.op.overObj := rfl
+
 end
 
 variable (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B)