Documentation

Mathlib.CategoryTheory.MorphismProperty.Composition

Compatibilities of properties of morphisms with respect to composition #

Given P : MorphismProperty C, we define the predicate P.IsStableUnderComposition which means that P f → P g → P (f ≫ g). We also introduce the type classes W.ContainsIdentities, W.IsMultiplicative, and W.HasTwoOutOfThreeProperty.

Typeclass expressing that a morphism property contain identities.

Instances

    for all X : C, the identity of X satisfies the morphism property

    instance CategoryTheory.MorphismProperty.ContainsIdentities.op {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities] :
    W.op.ContainsIdentities
    Equations
    • =
    Equations
    • =
    Equations
    • =
    instance CategoryTheory.MorphismProperty.ContainsIdentities.inf {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} [P.ContainsIdentities] [Q.ContainsIdentities] :
    (P Q).ContainsIdentities
    Equations
    • =
    instance CategoryTheory.MorphismProperty.Prod.containsIdentities {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_3, u_1} C₁] [CategoryTheory.Category.{u_4, u_2} C₂] (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) [W₁.ContainsIdentities] [W₂.ContainsIdentities] :
    (W₁.prod W₂).ContainsIdentities
    Equations
    • =
    instance CategoryTheory.MorphismProperty.Pi.containsIdentities {J : Type w} {C : JType u} [(j : J) → CategoryTheory.Category.{v, u} (C j)] (W : (j : J) → CategoryTheory.MorphismProperty (C j)) [∀ (j : J), (W j).ContainsIdentities] :
    (CategoryTheory.MorphismProperty.pi W).ContainsIdentities
    Equations
    • =
    theorem CategoryTheory.MorphismProperty.of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [P.RespectsIso] {X : C} {Y : C} (f : X Y) [CategoryTheory.IsIso f] :
    P f

    A morphism property satisfies IsStableUnderComposition if the composition of two such morphisms still falls in the class.

    Instances
      theorem CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem {C : Type u} :
      ∀ {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} [self : P.IsStableUnderComposition] {X Y Z : C} (f : X Y) (g : Y Z), P fP gP (CategoryTheory.CategoryStruct.comp f g)
      theorem CategoryTheory.MorphismProperty.comp_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.IsStableUnderComposition] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (hf : W f) (hg : W g) :
      instance CategoryTheory.MorphismProperty.IsStableUnderComposition.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] :
      P.op.IsStableUnderComposition
      Equations
      • =
      instance CategoryTheory.MorphismProperty.IsStableUnderComposition.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} [P.IsStableUnderComposition] :
      P.unop.IsStableUnderComposition
      Equations
      • =
      instance CategoryTheory.MorphismProperty.IsStableUnderComposition.inf {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] [Q.IsStableUnderComposition] :
      (P Q).IsStableUnderComposition
      Equations
      • =

      A morphism property is StableUnderInverse if the inverse of a morphism satisfying the property still falls in the class.

      Equations
      • P.StableUnderInverse = ∀ ⦃X Y : C⦄ (e : X Y), P e.homP e.inv
      Instances For
        theorem CategoryTheory.MorphismProperty.StableUnderInverse.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} (h : P.StableUnderInverse) :
        P.op.StableUnderInverse
        instance CategoryTheory.MorphismProperty.IsStableUnderComposition.inverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.MorphismProperty D} [P.IsStableUnderComposition] (F : CategoryTheory.Functor C D) :
        (P.inverseImage F).IsStableUnderComposition
        Equations
        • =

        Given app : Π X, F₁.obj X ⟶ F₂.obj X where F₁ and F₂ are two functors, this is the morphism_property C satisfied by the morphisms in C with respect to whom app is natural.

        Equations
        Instances For
          Equations
          • =
          Equations
          • =
          Equations
          • =
          instance CategoryTheory.MorphismProperty.IsMultiplicative.inf {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {Q : CategoryTheory.MorphismProperty C} [P.IsMultiplicative] [Q.IsMultiplicative] :
          (P Q).IsMultiplicative
          Equations
          • =

          A class of morphisms W has the two-out-of-three property if whenever two out of three maps in f, g, f ≫ g are in W, then the third map is also in W.

          Instances
            theorem CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.of_postcomp {C : Type u} :
            ∀ {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} [self : W.HasTwoOutOfThreeProperty] {X Y Z : C} (f : X Y) (g : Y Z), W gW (CategoryTheory.CategoryStruct.comp f g)W f
            theorem CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.of_precomp {C : Type u} :
            ∀ {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} [self : W.HasTwoOutOfThreeProperty] {X Y Z : C} (f : X Y) (g : Y Z), W fW (CategoryTheory.CategoryStruct.comp f g)W g
            theorem CategoryTheory.MorphismProperty.of_postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasTwoOutOfThreeProperty] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (hg : W g) (hfg : W (CategoryTheory.CategoryStruct.comp f g)) :
            W f
            theorem CategoryTheory.MorphismProperty.of_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasTwoOutOfThreeProperty] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (hf : W f) (hfg : W (CategoryTheory.CategoryStruct.comp f g)) :
            W g
            theorem CategoryTheory.MorphismProperty.postcomp_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasTwoOutOfThreeProperty] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (hg : W g) :
            theorem CategoryTheory.MorphismProperty.precomp_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.HasTwoOutOfThreeProperty] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (hf : W f) :
            instance CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyInverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty D) [W.HasTwoOutOfThreeProperty] :
            (W.inverseImage F).HasTwoOutOfThreeProperty
            Equations
            • =