Documentation

Mathlib.CategoryTheory.MorphismProperty.Limits

Relation of morphism properties with limits #

The following predicates are introduces for morphism properties P:

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

We also introduce properties IsStableUnderProductsOfShape, IsStableUnderLimitsOfShape, IsStableUnderFiniteProducts.

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

Equations
Instances For

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

    Equations
    Instances For
      theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] [P.RespectsIso] (hP₂ : ∀ (X Y S : C) (f : X S) (g : Y S), P gP (CategoryTheory.Limits.pullback.fst f g)) :
      P.StableUnderBaseChange
      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) :
      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) :
      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') :
      theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPushouts C] [P.RespectsIso] (hP₂ : ∀ (A B A' : C) (f : A A') (g : A B), P fP (CategoryTheory.Limits.pushout.inr f g)) :
      P.StableUnderCobaseChange
      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) :
      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) :
      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

      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.
      Instances For
        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]

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

        Equations
        Instances For
          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₂ : JC) (f : (j : J) → X₁ j X₂ j), (∀ (j : J), W (f j))W (CategoryTheory.Limits.Pi.map f)) :
          W.IsStableUnderProductsOfShape J

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

          • isStableUnderProductsOfShape : ∀ (J : Type) [inst : Finite J], W.IsStableUnderProductsOfShape J
          Instances
            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

            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
            Instances For
              theorem CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] [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) [P.RespectsIso] :
              P.diagonal.StableUnderBaseChange

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

              Equations
              Instances For
                Equations
                • =
                theorem CategoryTheory.MorphismProperty.universally_mono {C : Type u} [CategoryTheory.Category.{v, u} C] :
                Monotone CategoryTheory.MorphismProperty.universally