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.

class CategoryTheory.MorphismProperty.IsStableUnderBaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.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}, CategoryTheory.IsPullback f' g' g f → P g → P g'

class CategoryTheory.MorphismProperty.IsStableUnderCobaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.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'}, CategoryTheory.IsPushout g f f' g' → P f → P f'

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

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

Alternative constructor for IsStableUnderBaseChange.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

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

@[deprecated CategoryTheory.MorphismProperty.pullback_fst]

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

Alias of CategoryTheory.MorphismProperty.pullback_fst.

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

@[deprecated CategoryTheory.MorphismProperty.pullback_snd]

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

Alias of CategoryTheory.MorphismProperty.pullback_snd.

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

@[deprecated CategoryTheory.MorphismProperty.baseChange_obj]

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

Alias of CategoryTheory.MorphismProperty.baseChange_obj.

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

@[deprecated CategoryTheory.MorphismProperty.baseChange_map]

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

Alias of CategoryTheory.MorphismProperty.baseChange_map.

theorem CategoryTheory.MorphismProperty.pullback_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty 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 = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g') : P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)

@[deprecated CategoryTheory.MorphismProperty.pullback_map]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.pullback_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty 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 = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g') : P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)

Alias of CategoryTheory.MorphismProperty.pullback_map.

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

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

An alternative constructor for IsStableUnderCobaseChange.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

@[deprecated CategoryTheory.MorphismProperty.pushout_inl]

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

Alias of CategoryTheory.MorphismProperty.pushout_inl.

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

@[deprecated CategoryTheory.MorphismProperty.pushout_inr]

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

Alias of CategoryTheory.MorphismProperty.pushout_inr.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.

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

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.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)

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

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

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

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

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

def CategoryTheory.MorphismProperty.diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y} : P.diagonal f ↔ P (CategoryTheory.Limits.pullback.diagonal f)

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

def CategoryTheory.MorphismProperty.universally {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) : P.universally.RespectsIso

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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

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