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.

  • id_mem (X : C) : W (CategoryStruct.id X)

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

Instances
    instance CategoryTheory.MorphismProperty.Pi.containsIdentities {J : Type w} {C : JType u} [(j : J) → Category.{v, u} (C j)] (W : (j : J) → MorphismProperty (C j)) [∀ (j : J), (W j).ContainsIdentities] :

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

    Instances
      theorem CategoryTheory.MorphismProperty.comp_mem {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [W.IsStableUnderComposition] {X Y Z : C} (f : X Y) (g : Y Z) (hf : W f) (hg : W g) :

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

      Equations
      Instances For
        def CategoryTheory.MorphismProperty.naturalityProperty {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F₁ F₂ : Functor C D} (app : (X : C) → F₁.obj X F₂.obj X) :

        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

          A morphism property is multiplicative if it contains identities and is stable by composition.

          Instances

            A class of morphisms W has the of-postcomp property wrt. W' if whenever g is in W' and f ≫ g is in W, also f is in W.

            Instances

              A class of morphisms W has the of-precomp property wrt. W' if whenever f is in W' and f ≫ g is in W, also g is in W.

              Instances

                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.of_postcomp {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {W' : MorphismProperty C} [W.HasOfPostcompProperty W'] {X Y Z : C} (f : X Y) (g : Y Z) (hg : W' g) (hfg : W (CategoryStruct.comp f g)) :
                  W f
                  theorem CategoryTheory.MorphismProperty.of_precomp {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {W' : MorphismProperty C} [W.HasOfPrecompProperty W'] {X Y Z : C} (f : X Y) (g : Y Z) (hf : W' f) (hfg : W (CategoryStruct.comp f g)) :
                  W g
                  theorem CategoryTheory.MorphismProperty.postcomp_iff {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {W' : MorphismProperty C} [W.RespectsRight W'] [W.HasOfPostcompProperty W'] {X Y Z : C} (f : X Y) (g : Y Z) (hg : W' g) :
                  theorem CategoryTheory.MorphismProperty.precomp_iff {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) {W' : MorphismProperty C} [W.RespectsLeft W'] [W.HasOfPrecompProperty W'] {X Y Z : C} (f : X Y) (g : Y Z) (hf : W' f) :