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.

source

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

source

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

source

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

P ≤ P.pullbacks

source

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

Monotone pullbacks

source

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

source

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

source

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

P ≤ P.pushouts

source

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

Monotone pushouts

source

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

P.pushouts.RespectsIso

source

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

P.pullbacks.RespectsIso

source

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 : MorphismPropety C is such that any object in C maps to the target of some morphism in P, then P.pushouts contains the isomorphisms.

source

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'

Instances

source

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

P.pullbacks.IsStableUnderBaseChange

source

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'

Instances

source

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

P.pushouts.IsStableUnderCobaseChange

source

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'

source

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

P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P

source

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

P.pullbacks ≤ P

source

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.

source

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

(MorphismProperty.isomorphisms C).IsStableUnderBaseChange

source

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

(MorphismProperty.monomorphisms C).IsStableUnderBaseChange

source

@[instance 900]

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

P.RespectsIso

source

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)

source

@[deprecated CategoryTheory.MorphismProperty.pullback_fst (since := "2024-11-06")]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.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)

Alias of CategoryTheory.MorphismProperty.pullback_fst.

source

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)

source

@[deprecated CategoryTheory.MorphismProperty.pullback_snd (since := "2024-11-06")]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.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)

Alias of CategoryTheory.MorphismProperty.pullback_snd.

source

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

P ((Over.pullback f).obj X).hom

source

@[deprecated CategoryTheory.MorphismProperty.baseChange_obj (since := "2024-11-06")]

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

P ((Over.pullback f).obj X).hom

Alias of CategoryTheory.MorphismProperty.baseChange_obj.

source

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

P ((Over.pullback f).map g).left

source

@[deprecated CategoryTheory.MorphismProperty.baseChange_map (since := "2024-11-06")]

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

P ((Over.pullback f).map g).left

Alias of CategoryTheory.MorphismProperty.baseChange_map.

source

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) ⋯ ⋯)

source

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

P.HasOfPostcompProperty (MorphismProperty.monomorphisms C)

source

@[deprecated CategoryTheory.MorphismProperty.pullback_map (since := "2024-11-06")]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.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) ⋯ ⋯)

Alias of CategoryTheory.MorphismProperty.pullback_map.

source

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'

source

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

P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P

source

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

P.pushouts ≤ P

source

@[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

source

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.

source

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

(MorphismProperty.isomorphisms C).IsStableUnderCobaseChange

source

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

(MorphismProperty.epimorphisms C).IsStableUnderCobaseChange

source

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

P.RespectsIso

source

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)

source

@[deprecated CategoryTheory.MorphismProperty.pushout_inl (since := "2024-11-06")]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.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)

Alias of CategoryTheory.MorphismProperty.pushout_inl.

source

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)

source

@[deprecated CategoryTheory.MorphismProperty.pushout_inr (since := "2024-11-06")]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.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)

Alias of CategoryTheory.MorphismProperty.pushout_inr.

source

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

P.HasOfPrecompProperty (MorphismProperty.epimorphisms C)

source

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

P.op.IsStableUnderBaseChange

source

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

P.unop.IsStableUnderBaseChange

source

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

P.op.IsStableUnderCobaseChange

source

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

P.unop.IsStableUnderCobaseChange

source

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

(P ⊓ Q).IsStableUnderBaseChange

source

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

(P ⊓ Q).IsStableUnderCobaseChange

source

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 })

source

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 φ

source

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

source

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

source

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)

source

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 φ

Instances

source

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

source

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

source

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)

source

@[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.

source

@[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.

source

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₂.ι })

source

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 φ

source

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

source

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

source

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'

source

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

source

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)

source

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 φ

Instances

source

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

source

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

source

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)

source

@[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.

source

@[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.

source

theorem 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

source

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)

source

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

source

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

source

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

source

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

W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1})

source

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

W ≤ coproducts.{w, v, u} W

source

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

Monotone coproducts.{w, v, u}

source

@[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)

source

@[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)

source

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

source

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

source

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

Instances

source

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

Instances

source

@[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.

source

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