Documentation

Mathlib.CategoryTheory.MorphismProperty.Basic

Properties of morphisms #

We provide the basic framework for talking about properties of morphisms. The following meta-property is defined

A MorphismProperty C is a class of morphisms between objects in C.

Equations
Instances For
    @[simp]

    The morphism property in Cᵒᵖ associated to a morphism property in C

    Equations
    • P.op f = P f.unop
    Instances For

      The morphism property in C associated to a morphism property in Cᵒᵖ

      Equations
      • P.unop f = P f.op
      Instances For

        The inverse image of a MorphismProperty D by a functor C ⥤ D

        Equations
        • P.inverseImage F f = P (F.map f)
        Instances For
          @[simp]

          The image (up to isomorphisms) of a MorphismProperty C by a functor C ⥤ D

          Equations
          Instances For

            A morphism property RespectsIso if it still holds when composed with an isomorphism

            Instances
              theorem CategoryTheory.MorphismProperty.RespectsIso.precomp {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [self : P.RespectsIso] {X : C} {Y : C} {Z : C} (e : X Y) (f : Y Z) (hf : P f) :
              theorem CategoryTheory.MorphismProperty.RespectsIso.postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [self : P.RespectsIso] {X : C} {Y : C} {Z : C} (e : Y Z) (f : X Y) (hf : P f) :
              Equations
              • =
              Equations
              • =

              The intersection of two isomorphism respecting morphism properties respects isomorphisms.

              Equations
              • =

              The closure by isomorphisms of a MorphismProperty

              Equations
              Instances For
                theorem CategoryTheory.MorphismProperty.monotone_isoClosure {C : Type u} [CategoryTheory.Category.{v, u} C] :
                Monotone CategoryTheory.MorphismProperty.isoClosure
                theorem CategoryTheory.MorphismProperty.arrow_mk_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} (e : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) :
                P f P g
                @[deprecated CategoryTheory.MorphismProperty.cancel_left_of_respectsIso]

                Alias of CategoryTheory.MorphismProperty.cancel_left_of_respectsIso.

                @[deprecated CategoryTheory.MorphismProperty.cancel_right_of_respectsIso]

                Alias of CategoryTheory.MorphismProperty.cancel_right_of_respectsIso.

                @[deprecated CategoryTheory.MorphismProperty.arrow_iso_iff]

                Alias of CategoryTheory.MorphismProperty.arrow_iso_iff.

                @[deprecated CategoryTheory.MorphismProperty.arrow_mk_iso_iff]
                theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} (e : CategoryTheory.Arrow.mk f CategoryTheory.Arrow.mk g) :
                P f P g

                Alias of CategoryTheory.MorphismProperty.arrow_mk_iso_iff.

                @[deprecated CategoryTheory.MorphismProperty.isoClosure_eq_self]

                Alias of CategoryTheory.MorphismProperty.isoClosure_eq_self.

                If W₁ and W₂ are morphism properties on two categories C₁ and C₂, this is the induced morphism property on C₁ × C₂.

                Equations
                • W₁.prod W₂ f = (W₁ f.1 W₂ f.2)
                Instances For
                  def CategoryTheory.MorphismProperty.pi {J : Type w} {C : JType u} [(j : J) → CategoryTheory.Category.{v, u} (C j)] (W : (j : J) → CategoryTheory.MorphismProperty (C j)) :

                  If W j are morphism properties on categories C j for all j, this is the induced morphism property on the category ∀ j, C j.

                  Equations
                  Instances For

                    The morphism property on J ⥤ C which is defined objectwise from W : MorphismProperty C.

                    Equations
                    • W.functorCategory J f = ∀ (j : J), W (f.app j)
                    Instances For

                      Given W : MorphismProperty C, this is the morphism property on Arrow C of morphisms whose left and right parts are in W.

                      Equations
                      • W.arrow f = (W f.left W f.right)
                      Instances For