Relation of morphism properties with limits

The following predicates are introduces for morphism properties P:

• IsStableUnderBaseChange: P is stable under base change if in all pullback squares, the left map satisfies P if the right map satisfies it.
• IsStableUnderCobaseChange: P is stable under cobase change if in all pushout squares, the right map satisfies P if the left map satisfies it.

We define P.universally for the class of morphisms which satisfy P after any base change.

We also introduce properties IsStableUnderProductsOfShape, IsStableUnderLimitsOfShape, IsStableUnderFiniteProducts, and similar properties for colimits and coproducts.

def CategoryTheory.MorphismProperty.pullbacks {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : MorphismProperty C

Given a class of morphisms P, this is the class of pullbacks of morphisms in P.

Equations

• P.pullbacks q = ∃ (X : C) (Y : C) (p : X ⟶ Y) (f : A ⟶ X) (g : B ⟶ Y) (_ : P p), CategoryTheory.IsPullback f q p g

theorem CategoryTheory.MorphismProperty.pullbacks_mk {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) {A B X Y : C} {f : A ⟶ X} {q : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : IsPullback f q p g) (hp : P p) : P.pullbacks q

theorem CategoryTheory.MorphismProperty.le_pullbacks {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P ≤ P.pullbacks

theorem CategoryTheory.MorphismProperty.pullbacks_monotone {C : Type u} [Category.{v, u} C] : Monotone pullbacks

def CategoryTheory.MorphismProperty.pushouts {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : MorphismProperty C

Given a class of morphisms P, this is the class of pushouts of morphisms in P.

Equations

• P.pushouts q = ∃ (A : C) (B : C) (p : A ⟶ B) (f : A ⟶ X) (g : B ⟶ Y) (_ : P p), CategoryTheory.IsPushout f p q g

theorem CategoryTheory.MorphismProperty.pushouts_mk {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) {A B X Y : C} {f : A ⟶ X} {q : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : IsPushout f q p g) (hq : P q) : P.pushouts p

theorem CategoryTheory.MorphismProperty.le_pushouts {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P ≤ P.pushouts

theorem CategoryTheory.MorphismProperty.pushouts_monotone {C : Type u} [Category.{v, u} C] : Monotone pushouts

instance CategoryTheory.MorphismProperty.instRespectsIsoPushouts {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.pushouts.RespectsIso

instance CategoryTheory.MorphismProperty.instRespectsIsoPullbacks {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.pullbacks.RespectsIso

theorem CategoryTheory.MorphismProperty.isomorphisms_le_pushouts {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) (h : ∀ (X : C), ∃ (A : C) (B : C) (p : A ⟶ B) (_ : P p) (x : B ⟶ X), IsIso p) : isomorphisms C ≤ P.pushouts

If P : MorphismProperty C is such that any object in C maps to the target of some morphism in P, then P.pushouts contains the isomorphisms.

class CategoryTheory.MorphismProperty.IsStableUnderBaseChange {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : Prop

A morphism property is IsStableUnderBaseChange if the base change of such a morphism still falls in the class.

• of_isPullback {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g) : P g'

instance CategoryTheory.MorphismProperty.instIsStableUnderBaseChangePullbacks {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.pullbacks.IsStableUnderBaseChange

class CategoryTheory.MorphismProperty.IsStableUnderCobaseChange {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : Prop

A morphism property is IsStableUnderCobaseChange if the cobase change of such a morphism still falls in the class.

• of_isPushout {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f) : P f'

instance CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangePushouts {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.pushouts.IsStableUnderCobaseChange

theorem CategoryTheory.MorphismProperty.of_isPullback {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f) (hg : P g) : P g'

theorem CategoryTheory.MorphismProperty.isStableUnderBaseChange_iff_pullbacks_le {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P

theorem CategoryTheory.MorphismProperty.pullbacks_le {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.IsStableUnderBaseChange] : P.pullbacks ≤ P

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk' {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.RespectsIso] (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : Limits.HasPullback f g], P g → P (Limits.pullback.fst f g)) : P.IsStableUnderBaseChange

Alternative constructor for IsStableUnderBaseChange.

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms (C : Type u) [Category.{v, u} C] : (MorphismProperty.isomorphisms C).IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.monomorphisms (C : Type u) [Category.{v, u} C] : (MorphismProperty.monomorphisms C).IsStableUnderBaseChange

@[instance 900]

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] : P.RespectsIso

theorem CategoryTheory.MorphismProperty.pullback_fst {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Limits.HasPullback f g] (H : P g) : P (Limits.pullback.fst f g)

theorem CategoryTheory.MorphismProperty.pullback_snd {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [Limits.HasPullback f g] (H : P f) : P (Limits.pullback.snd f g)

theorem CategoryTheory.MorphismProperty.baseChange_obj {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) [∀ {W : C} (h : W ⟶ S), Limits.HasPullback h f] (X : Over S) (H : P X.hom) : P ((Over.pullback f).obj X).hom

theorem CategoryTheory.MorphismProperty.baseChange_map {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) [∀ {W : C} (h : W ⟶ S), Limits.HasPullback h f] {X Y : Over S} (g : X ⟶ Y) (H : P g.left) : P ((Over.pullback f).map g).left

theorem CategoryTheory.MorphismProperty.pullback_map {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [Limits.HasPullbacks C] [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'} {i₂ : Y ⟶ Y'} (h₁ : P i₁) (h₂ : P i₂) (e₁ : f = CategoryStruct.comp i₁ f') (e₂ : g = CategoryStruct.comp i₂ g') : P (Limits.pullback.map f g f' g' i₁ i₂ (CategoryStruct.id S) ⋯ ⋯)

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.hasOfPostcompProperty_monomorphisms {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] : P.HasOfPostcompProperty (MorphismProperty.monomorphisms C)

theorem CategoryTheory.MorphismProperty.of_isPushout {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderCobaseChange] {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : IsPushout g f f' g') (hf : P f) : P f'

theorem CategoryTheory.MorphismProperty.isStableUnderCobaseChange_iff_pushouts_le {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} : P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P

theorem CategoryTheory.MorphismProperty.pushouts_le {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderCobaseChange] : P.pushouts ≤ P

@[simp]

theorem CategoryTheory.MorphismProperty.pushouts_le_iff {C : Type u} [Category.{v, u} C] {P Q : MorphismProperty C} [Q.IsStableUnderCobaseChange] : P.pushouts ≤ Q ↔ P ≤ Q

theorem CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk' {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.RespectsIso] (hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : Limits.HasPushout f g], P f → P (Limits.pushout.inr f g)) : P.IsStableUnderCobaseChange

An alternative constructor for IsStableUnderCobaseChange.

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.isomorphisms {C : Type u} [Category.{v, u} C] : (MorphismProperty.isomorphisms C).IsStableUnderCobaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.epimorphisms (C : Type u) [Category.{v, u} C] : (MorphismProperty.epimorphisms C).IsStableUnderCobaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.respectsIso {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderCobaseChange] : P.RespectsIso

theorem CategoryTheory.MorphismProperty.pushout_inl {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderCobaseChange] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [Limits.HasPushout f g] (H : P g) : P (Limits.pushout.inl f g)

theorem CategoryTheory.MorphismProperty.pushout_inr {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderCobaseChange] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [Limits.HasPushout f g] (H : P f) : P (Limits.pushout.inr f g)

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.hasOfPrecompProperty_epimorphisms {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderCobaseChange] : P.HasOfPrecompProperty (MorphismProperty.epimorphisms C)

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.op {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderCobaseChange] : P.op.IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.unop {C : Type u} [Category.{v, u} C] {P : MorphismProperty Cᵒᵖ} [P.IsStableUnderCobaseChange] : P.unop.IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.op {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] : P.op.IsStableUnderCobaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.unop {C : Type u} [Category.{v, u} C] {P : MorphismProperty Cᵒᵖ} [P.IsStableUnderBaseChange] : P.unop.IsStableUnderCobaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf {C : Type u} [Category.{v, u} C] {P Q : MorphismProperty C} [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] : (P ⊓ Q).IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.inf {C : Type u} [Category.{v, u} C] {P Q : MorphismProperty C} [P.IsStableUnderCobaseChange] [Q.IsStableUnderCobaseChange] : (P ⊓ Q).IsStableUnderCobaseChange

instance CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop {C : Type u} [Category.{v, u} C] : ⊤.IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeTop {C : Type u} [Category.{v, u} C] : ⊤.IsStableUnderCobaseChange

inductive CategoryTheory.MorphismProperty.limitsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [Category.{u_2, u_1} J] : MorphismProperty C

The class of morphisms in C that are limits of shape J of natural transformations involving morphisms in W.

• mk {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] (X₁ X₂ : Functor J C) (c₁ : Limits.Cone X₁) (c₂ : Limits.Cone X₂) : ∀ (x : Limits.IsLimit c₁) (h₂ : Limits.IsLimit c₂) (f : X₁ ⟶ X₂), W.functorCategory J f → W.limitsOfShape J (h₂.lift { pt := c₁.pt, π := CategoryStruct.comp c₁.π f })

theorem CategoryTheory.MorphismProperty.limitsOfShape.mk' {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] (X₁ X₂ : Functor J C) (c₁ : Limits.Cone X₁) (c₂ : Limits.Cone X₂) (h₁ : Limits.IsLimit c₁) (h₂ : Limits.IsLimit c₂) (f : X₁ ⟶ X₂) (hf : W.functorCategory J f) (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ (j : J), CategoryStruct.comp φ (c₂.π.app j) = CategoryStruct.comp (c₁.π.app j) (f.app j)) : W.limitsOfShape J φ

theorem CategoryTheory.MorphismProperty.limitsOfShape_monotone {C : Type u} [Category.{v, u} C] {W₁ W₂ : MorphismProperty C} (h : W₁ ≤ W₂) (J : Type u_2) [Category.{u_3, u_2} J] : W₁.limitsOfShape J ≤ W₂.limitsOfShape J

instance CategoryTheory.MorphismProperty.instRespectsIsoLimitsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [Category.{u_2, u_1} J] : (W.limitsOfShape J).RespectsIso

theorem CategoryTheory.MorphismProperty.limitsOfShape_limMap {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] {X Y : Functor J C} (f : X ⟶ Y) [Limits.HasLimit X] [Limits.HasLimit Y] (hf : W.functorCategory J f) : W.limitsOfShape J (Limits.limMap f)

class CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [Category.{u_2, u_1} J] : Prop

The property that a morphism property W is stable under limits indexed by a category J.

• condition (X₁ X₂ : Functor J C) (c₁ : Limits.Cone X₁) (c₂ : Limits.Cone X₂) : ∀ (x : Limits.IsLimit c₁) (h₂ : Limits.IsLimit c₂) (f : X₁ ⟶ X₂), W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ (j : J), CategoryStruct.comp φ (c₂.π.app j) = CategoryStruct.comp (c₁.π.app j) (f.app j)), W φ

theorem CategoryTheory.MorphismProperty.isStableUnderLimitsOfShape_iff_limitsOfShape_le {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [Category.{u_2, u_1} J] : W.IsStableUnderLimitsOfShape J ↔ W.limitsOfShape J ≤ W

theorem CategoryTheory.MorphismProperty.limitsOfShape_le {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] [W.IsStableUnderLimitsOfShape J] : W.limitsOfShape J ≤ W

theorem CategoryTheory.MorphismProperty.limMap {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] [W.IsStableUnderLimitsOfShape J] {X Y : Functor J C} (f : X ⟶ Y) [Limits.HasLimit X] [Limits.HasLimit Y] (hf : W.functorCategory J f) : W (Limits.limMap f)

@[deprecated CategoryTheory.MorphismProperty.limitsOfShape_le (since := "2025-05-11")]

theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.limitsOfShape_le {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] [W.IsStableUnderLimitsOfShape J] : W.limitsOfShape J ≤ W

Alias of CategoryTheory.MorphismProperty.limitsOfShape_le.

@[deprecated CategoryTheory.MorphismProperty.limMap (since := "2025-05-11")]

theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.limMap {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] [W.IsStableUnderLimitsOfShape J] {X Y : Functor J C} (f : X ⟶ Y) [Limits.HasLimit X] [Limits.HasLimit Y] (hf : W.functorCategory J f) : W (Limits.limMap f)

Alias of CategoryTheory.MorphismProperty.limMap.

inductive CategoryTheory.MorphismProperty.colimitsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [Category.{u_2, u_1} J] : MorphismProperty C

The class of morphisms in C that are colimits of shape J of natural transformations involving morphisms in W.

• mk {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] (X₁ X₂ : Functor J C) (c₁ : Limits.Cocone X₁) (c₂ : Limits.Cocone X₂) (h₁ : Limits.IsColimit c₁) (h₂ : Limits.IsColimit c₂) (f : X₁ ⟶ X₂) : W.functorCategory J f → W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := CategoryStruct.comp f c₂.ι })

theorem CategoryTheory.MorphismProperty.colimitsOfShape.mk' {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] (X₁ X₂ : Functor J C) (c₁ : Limits.Cocone X₁) (c₂ : Limits.Cocone X₂) (h₁ : Limits.IsColimit c₁) (h₂ : Limits.IsColimit c₂) (f : X₁ ⟶ X₂) (hf : W.functorCategory J f) (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) φ = CategoryStruct.comp (f.app j) (c₂.ι.app j)) : W.colimitsOfShape J φ

theorem CategoryTheory.MorphismProperty.colimitsOfShape_monotone {C : Type u} [Category.{v, u} C] {W₁ W₂ : MorphismProperty C} (h : W₁ ≤ W₂) (J : Type u_2) [Category.{u_3, u_2} J] : W₁.colimitsOfShape J ≤ W₂.colimitsOfShape J

theorem CategoryTheory.MorphismProperty.colimitsOfShape_le_of_final {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {J : Type u_1} [Category.{u_4, u_1} J] {J' : Type u_2} [Category.{u_3, u_2} J'] (F : Functor J J') [F.Final] : W.colimitsOfShape J' ≤ W.colimitsOfShape J

theorem CategoryTheory.MorphismProperty.colimitsOfShape_eq_of_equivalence {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {J : Type u_1} [Category.{u_4, u_1} J] {J' : Type u_2} [Category.{u_3, u_2} J'] (e : J ≌ J') : W.colimitsOfShape J = W.colimitsOfShape J'

instance CategoryTheory.MorphismProperty.instRespectsIsoColimitsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [Category.{u_2, u_1} J] : (W.colimitsOfShape J).RespectsIso

theorem CategoryTheory.MorphismProperty.colimitsOfShape_colimMap {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] {X Y : Functor J C} (f : X ⟶ Y) [Limits.HasColimit X] [Limits.HasColimit Y] (hf : W.functorCategory J f) : W.colimitsOfShape J (Limits.colimMap f)

theorem CategoryTheory.MorphismProperty.colimitsOfShape.of_isColimit {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_2} [Preorder J] [OrderBot J] {F : Functor J C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) (h : ∀ (j : J), W (F.map (homOfLE ⋯))) : W.colimitsOfShape J (c.ι.app ⊥)

class CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [Category.{u_2, u_1} J] : Prop

The property that a morphism property W is stable under colimits indexed by a category J.

• condition (X₁ X₂ : Functor J C) (c₁ : Limits.Cocone X₁) (c₂ : Limits.Cocone X₂) (h₁ : Limits.IsColimit c₁) : ∀ (h₁✝ : Limits.IsColimit c₂) (f : X₁ ⟶ X₂), W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt) (hφ : ∀ (j : J), CategoryStruct.comp (c₁.ι.app j) φ = CategoryStruct.comp (f.app j) (c₂.ι.app j)), W φ

theorem CategoryTheory.MorphismProperty.isStableUnderColimitsOfShape_iff_colimitsOfShape_le {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [Category.{u_2, u_1} J] : W.IsStableUnderColimitsOfShape J ↔ W.colimitsOfShape J ≤ W

theorem CategoryTheory.MorphismProperty.colimitsOfShape_le {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] [W.IsStableUnderColimitsOfShape J] : W.colimitsOfShape J ≤ W

theorem CategoryTheory.MorphismProperty.colimMap {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] [W.IsStableUnderColimitsOfShape J] {X Y : Functor J C} (f : X ⟶ Y) [Limits.HasColimit X] [Limits.HasColimit Y] (hf : W.functorCategory J f) : W (Limits.colimMap f)

@[deprecated CategoryTheory.MorphismProperty.colimMap (since := "2025-05-11")]

theorem CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.colimMap {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] [W.IsStableUnderColimitsOfShape J] {X Y : Functor J C} (f : X ⟶ Y) [Limits.HasColimit X] [Limits.HasColimit Y] (hf : W.functorCategory J f) : W (Limits.colimMap f)

Alias of CategoryTheory.MorphismProperty.colimMap.

@[deprecated CategoryTheory.MorphismProperty.colimitsOfShape_le (since := "2025-05-11")]

theorem CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.colimitsOfShape_le {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {J : Type u_1} [Category.{u_2, u_1} J] [W.IsStableUnderColimitsOfShape J] : W.colimitsOfShape J ≤ W

Alias of CategoryTheory.MorphismProperty.colimitsOfShape_le.

instance CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.isomorphisms (C : Type u) [Category.{v, u} C] (J : Type u_1) [Category.{u_2, u_1} J] : (MorphismProperty.isomorphisms C).IsStableUnderColimitsOfShape J

class CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

The condition that a property of morphisms is stable by filtered colimits.

• isStableUnderColimitsOfShape (J : Type w') [Category.{w, w'} J] [IsFiltered J] : W.IsStableUnderColimitsOfShape J

instance CategoryTheory.MorphismProperty.instIsStableUnderFilteredColimitsIsomorphisms {C : Type u} [Category.{v, u} C] : IsStableUnderFilteredColimits.{w, w', v, u} (isomorphisms C)

def CategoryTheory.MorphismProperty.coproducts {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : MorphismProperty C

Given W : MorphismProperty C, this is class of morphisms that are isomorphic to a coproduct of a family (indexed by some J : Type w) of maps in W.

Equations

• CategoryTheory.MorphismProperty.coproducts.{?u.10, ?u.9, ?u.8} W = ⨆ (J : Type ?u.10), W.colimitsOfShape (CategoryTheory.Discrete J)

theorem CategoryTheory.MorphismProperty.colimitsOfShape_le_coproducts {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type w) : W.colimitsOfShape (Discrete J) ≤ coproducts.{w, v, u} W

theorem CategoryTheory.MorphismProperty.coproducts_iff {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {X Y : C} (f : X ⟶ Y) : coproducts.{w, v, u} W f ↔ ∃ (J : Type w), W.colimitsOfShape (Discrete J) f

theorem CategoryTheory.MorphismProperty.coproducts_of_small {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {X Y : C} (f : X ⟶ Y) {J : Type w'} (hf : W.colimitsOfShape (Discrete J) f) [Small.{w, w'} J] : coproducts.{w, v, u} W f

theorem CategoryTheory.MorphismProperty.le_colimitsOfShape_punit {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1})

theorem CategoryTheory.MorphismProperty.le_coproducts {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : W ≤ coproducts.{w, v, u} W

theorem CategoryTheory.MorphismProperty.coproducts_monotone {C : Type u} [Category.{v, u} C] : Monotone coproducts.{w, v, u}

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) : Prop

The property that a morphism property W is stable under products indexed by a type J.

Equations

• W.IsStableUnderProductsOfShape J = W.IsStableUnderLimitsOfShape (CategoryTheory.Discrete J)

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) : Prop

The property that a morphism property W is stable under coproducts indexed by a type J.

Equations

• W.IsStableUnderCoproductsOfShape J = W.IsStableUnderColimitsOfShape (CategoryTheory.Discrete J)

theorem CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [W.RespectsIso] (hW : ∀ (X₁ X₂ : J → C) [inst : Limits.HasProduct X₁] [inst_1 : Limits.HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (Limits.Pi.map f)) : W.IsStableUnderProductsOfShape J

theorem CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape.mk {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u_1) [W.RespectsIso] (hW : ∀ (X₁ X₂ : J → C) [inst : Limits.HasCoproduct X₁] [inst_1 : Limits.HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (Limits.Sigma.map f)) : W.IsStableUnderCoproductsOfShape J

class CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

The condition that a property of morphisms is stable by finite products.

• isStableUnderProductsOfShape (J : Type) [Finite J] : W.IsStableUnderProductsOfShape J

class CategoryTheory.MorphismProperty.IsStableUnderFiniteCoproducts {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

The condition that a property of morphisms is stable by finite coproducts.

• isStableUnderCoproductsOfShape (J : Type) [Finite J] : W.IsStableUnderCoproductsOfShape J

@[deprecated CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts.isStableUnderProductsOfShape "This is now an instance." (since := "2025-05-11")]

theorem CategoryTheory.MorphismProperty.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts {C : Type u} {inst✝ : Category.{v, u} C} {W : MorphismProperty C} [self : W.IsStableUnderFiniteProducts] (J : Type) [Finite J] : W.IsStableUnderProductsOfShape J

Alias of CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts.isStableUnderProductsOfShape.

@[deprecated CategoryTheory.MorphismProperty.IsStableUnderFiniteCoproducts.isStableUnderCoproductsOfShape "This is now an instance." (since := "2025-05-11")]

theorem CategoryTheory.MorphismProperty.isStableUnderCoproductsOfShape_of_isStableUnderFiniteCoproducts {C : Type u} {inst✝ : Category.{v, u} C} {W : MorphismProperty C} [self : W.IsStableUnderFiniteCoproducts] (J : Type) [Finite J] : W.IsStableUnderCoproductsOfShape J

Alias of CategoryTheory.MorphismProperty.IsStableUnderFiniteCoproducts.isStableUnderCoproductsOfShape.

class CategoryTheory.MorphismProperty.IsStableUnderCoproducts {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : Prop

The condition that a property of morphisms is stable by coproducts.

• isStableUnderCoproductsOfShape (J : Type w) : W.IsStableUnderCoproductsOfShape J

theorem CategoryTheory.MorphismProperty.coproducts_le {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [IsStableUnderCoproducts.{w, v, u} W] : coproducts.{w, v, u} W ≤ W

@[simp]

theorem CategoryTheory.MorphismProperty.coproducts_eq_self {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [IsStableUnderCoproducts.{w, v, u} W] : coproducts.{w, v, u} W = W

@[simp]

theorem CategoryTheory.MorphismProperty.coproducts_le_iff {C : Type u} [Category.{v, u} C] {P Q : MorphismProperty C} [IsStableUnderCoproducts.{w, v, u} Q] : coproducts.{w, v, u} P ≤ Q ↔ P ≤ Q

def CategoryTheory.MorphismProperty.diagonal {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (P : MorphismProperty C) : MorphismProperty C

For P : MorphismProperty C, P.diagonal is a morphism property that holds for f : X ⟶ Y whenever P holds for X ⟶ Y xₓ Y.

Equations

• P.diagonal f = P (CategoryTheory.Limits.pullback.diagonal f)

theorem CategoryTheory.MorphismProperty.diagonal_iff {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {P : MorphismProperty C} {X Y : C} {f : X ⟶ Y} : P.diagonal f ↔ P (Limits.pullback.diagonal f)

instance CategoryTheory.MorphismProperty.RespectsIso.diagonal {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {P : MorphismProperty C} [P.RespectsIso] : P.diagonal.RespectsIso

instance CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {P : MorphismProperty C} [P.IsStableUnderComposition] [P.RespectsIso] [P.IsStableUnderBaseChange] : P.diagonal.IsStableUnderComposition

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] [P.RespectsIso] : P.diagonal.IsStableUnderBaseChange

theorem CategoryTheory.MorphismProperty.diagonal_isomorphisms {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] : (isomorphisms C).diagonal = monomorphisms C

theorem CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {Q : MorphismProperty C} [Q.IsStableUnderBaseChange] : P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal

If P is multiplicative and stable under base change, having the of-postcomp property w.r.t. Q is equivalent to Q implying P on the diagonal.

def CategoryTheory.MorphismProperty.universally {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : MorphismProperty C

P.universally holds for a morphism f : X ⟶ Y iff P holds for all X ×[Y] Y' ⟶ Y'.

Equations

• P.universally f = ∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), CategoryTheory.IsPullback f' i₁ i₂ f → P f'

instance CategoryTheory.MorphismProperty.universally_respectsIso {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.universally.RespectsIso

instance CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.universally.IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.IsStableUnderComposition.universally {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] (P : MorphismProperty C) [hP : P.IsStableUnderComposition] : P.universally.IsStableUnderComposition

theorem CategoryTheory.MorphismProperty.universally_le {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : P.universally ≤ P

theorem CategoryTheory.MorphismProperty.universally_inf {C : Type u} [Category.{v, u} C] (P Q : MorphismProperty C) : (P ⊓ Q).universally = P.universally ⊓ Q.universally

theorem CategoryTheory.MorphismProperty.universally_eq_iff {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} : P.universally = P ↔ P.IsStableUnderBaseChange

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} [hP : P.IsStableUnderBaseChange] : P.universally = P

theorem CategoryTheory.MorphismProperty.universally_mono {C : Type u} [Category.{v, u} C] : Monotone universally

theorem CategoryTheory.MorphismProperty.universally_mk' {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] {X Y : C} (g : X ⟶ Y) (H : ∀ {T : C} (f : T ⟶ Y) [inst : Limits.HasPullback f g], P (Limits.pullback.fst f g)) : P.universally g

class CategoryTheory.MorphismProperty.HasPullbacks {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : Prop

P has pullbacks if for every f satisfying P, pullbacks of arbitrary morphisms along f exist.

• hasPullback {X Y S : C} {f : X ⟶ S} (g : Y ⟶ S) : P f → Limits.HasPullback f g

instance CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [Limits.HasPullbacks C] : P.HasPullbacks

theorem CategoryTheory.MorphismProperty.hasPullback {C : Type u} {inst✝ : Category.{v, u} C} {P : MorphismProperty C} [self : P.HasPullbacks] {X Y S : C} {f : X ⟶ S} (g : Y ⟶ S) : P f → Limits.HasPullback f g

Alias of CategoryTheory.MorphismProperty.HasPullbacks.hasPullback.