Relation of morphism properties with limits

The following predicates are introduces for morphism properties P:

• StableUnderBaseChange: P is stable under base change if in all pullback squares, the left map satisfies P if the right map satisfies it.
• StableUnderCobaseChange: 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.

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

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

Equations

• P.StableUnderBaseChange = ∀ ⦃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'

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

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

Equations

• P.StableUnderCobaseChange = ∀ ⦃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.StableUnderBaseChange.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] (hP₁ : P.RespectsIso) (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P CategoryTheory.Limits.pullback.fst) : P.StableUnderBaseChange

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : P.StableUnderBaseChange) : P.RespectsIso

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

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

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

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

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : P.StableUnderBaseChange) [P.IsStableUnderComposition] {S : C} {X : C} {X' : C} {Y : C} {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) ⋯ ⋯)

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

theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : P.StableUnderCobaseChange) : P.RespectsIso

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

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

theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : P.StableUnderCobaseChange) : P.op.StableUnderBaseChange

theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} (hP : P.StableUnderCobaseChange) : P.unop.StableUnderBaseChange

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (hP : P.StableUnderBaseChange) : P.op.StableUnderCobaseChange

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} (hP : P.StableUnderBaseChange) : P.unop.StableUnderCobaseChange

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 : CategoryTheory.Functor J C} {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) (hW₀ : 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.IsStableUnderFiniteProducts.isStableUnderProductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} [self : W.IsStableUnderFiniteProducts] (J : Type) [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 : C} {Y : C} {f : X ⟶ Y} : P.diagonal f ↔ P (CategoryTheory.Limits.pullback.diagonal f)

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

theorem CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] (hP' : P.RespectsIso) (hP'' : P.StableUnderBaseChange) : P.diagonal.IsStableUnderComposition

theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} (hP : P.StableUnderBaseChange) (hP' : P.RespectsIso) : P.diagonal.StableUnderBaseChange

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'

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

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

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_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} : P.universally = P ↔ P.StableUnderBaseChange

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

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