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
Equations
  • One or more equations did not get rendered due to their size.
theorem CategoryTheory.MorphismProperty.le_def (C : Type u) [Category.{v, u} C] {P Q : MorphismProperty C} :
P Q ∀ {X Y : C} (f : X Y), P fQ f
theorem CategoryTheory.MorphismProperty.top_eq (C : Type u) [Category.{v, u} C] :
= fun (x x_1 : C) (x : x x_1) => True
theorem CategoryTheory.MorphismProperty.ext {C : Type u} [Category.{v, u} C] (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X Y), W f W' f) :
W = W'
theorem CategoryTheory.MorphismProperty.ext_iff {C : Type u} [Category.{v, u} C] {W W' : MorphismProperty C} :
W = W' ∀ ⦃X Y : C⦄ (f : X Y), W f W' f
@[simp]
theorem CategoryTheory.MorphismProperty.top_apply {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) :
f
theorem CategoryTheory.MorphismProperty.of_eq_top {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} (h : P = ) {X Y : C} (f : X Y) :
P f
@[simp]
theorem CategoryTheory.MorphismProperty.sSup_iff {C : Type u} [Category.{v, u} C] (S : Set (MorphismProperty C)) {X Y : C} (f : X Y) :
sSup S f ∃ (W : S), W f
@[simp]
theorem CategoryTheory.MorphismProperty.iSup_iff {C : Type u} [Category.{v, u} C] {ι : Sort u_2} (W : ιMorphismProperty C) {X Y : C} (f : X Y) :
iSup W f ∃ (i : ι), W i f

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

Equations

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

Equations

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

Equations
@[simp]
theorem CategoryTheory.MorphismProperty.inverseImage_iff {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty D) (F : Functor C D) {X Y : C} (f : X Y) :
P.inverseImage F f P (F.map f)

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

Equations
theorem CategoryTheory.MorphismProperty.map_mem_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty C) (F : Functor C D) {X Y : C} (f : X Y) (hf : P f) :
P.map F (F.map f)

The set in Set (Arrow C) which corresponds to P : MorphismProperty C.

Equations

The family of morphisms indexed by P.toSet which corresponds to P : MorphismProperty C, see MorphismProperty.ofHoms_homFamily.

Equations
@[simp]
theorem CategoryTheory.MorphismProperty.homFamily_arrow_mk {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) {X Y : C} (f : X Y) (hf : P f) :
theorem CategoryTheory.MorphismProperty.of_eq {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) {X Y : C} {f : X Y} (hf : P f) {X' Y' : C} {f' : X' Y'} (hX : X = X') (hY : Y = Y') (h : f' = CategoryStruct.comp (eqToHom ) (CategoryStruct.comp f (eqToHom hY))) :
P f'
inductive CategoryTheory.MorphismProperty.ofHoms {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X Y : ιC} (f : (i : ι) → X i Y i) :

The class of morphisms given by a family of morphisms f i : X i ⟶ Y i.

theorem CategoryTheory.MorphismProperty.ofHoms_iff {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X Y : ιC} (f : (i : ι) → X i Y i) {A B : C} (g : A B) :
ofHoms f g ∃ (i : ι), Arrow.mk g = Arrow.mk (f i)

A morphism property P satisfies P.RespectsRight Q if it is stable under post-composition with morphisms satisfying Q, i.e. whenever P holds for f and Q holds for i then P holds for f ≫ i.

Instances

    A morphism property P satisfies P.RespectsLeft Q if it is stable under pre-composition with morphisms satisfying Q, i.e. whenever P holds for f and Q holds for i then P holds for i ≫ f.

    Instances

      A morphism property P satisfies P.Respects Q if it is stable under composition on the left and right by morphisms satisfying Q.

      Instances
        @[reducible, inline]

        P respects isomorphisms, if it respects the morphism property isomorphisms C, i.e. it is stable under pre- and postcomposition with isomorphisms.

        Equations
        theorem CategoryTheory.MorphismProperty.RespectsIso.mk {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) (hprecomp : ∀ {X Y Z : C} (e : X Y) (f : Y Z), P fP (CategoryStruct.comp e.hom f)) (hpostcomp : ∀ {X Y Z : C} (e : Y Z) (f : X Y), P fP (CategoryStruct.comp f e.hom)) :
        theorem CategoryTheory.MorphismProperty.RespectsIso.precomp {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : X Y) [IsIso e] (f : Y Z) (hf : P f) :
        theorem CategoryTheory.MorphismProperty.RespectsIso.postcomp {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} (e : Y Z) [IsIso e] (f : X Y) (hf : P f) :

        The closure by isomorphisms of a MorphismProperty

        Equations
        theorem CategoryTheory.MorphismProperty.comma_iso_iff {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] {A : Type u_2} {B : Type u_3} [Category.{u_4, u_2} A] [Category.{u_5, u_3} B] {L : Functor A C} {R : Functor B C} {f g : Comma L R} (e : f g) :
        P f.hom P g.hom
        theorem CategoryTheory.MorphismProperty.arrow_mk_iso_iff {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] {W X Y Z : C} {f : W X} {g : Y Z} (e : Arrow.mk f Arrow.mk g) :
        P f P g
        @[simp]
        theorem CategoryTheory.MorphismProperty.map_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_3, u_1} D] (P : MorphismProperty C) (F : Functor C D) {E : Type u_2} [Category.{u_4, u_2} E] (G : Functor D E) :
        (P.map F).map G = P.map (F.comp G)
        def CategoryTheory.MorphismProperty.prod {C₁ : Type u_2} {C₂ : Type u_3} [Category.{u_4, u_2} C₁] [Category.{u_5, u_3} C₂] (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) :
        MorphismProperty (C₁ × C₂)

        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)
        def CategoryTheory.MorphismProperty.pi {J : Type w} {C : JType u} [(j : J) → Category.{v, u} (C j)] (W : (j : J) → MorphismProperty (C j)) :
        MorphismProperty ((j : J) → 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

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

        Equations

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

        Equations
        theorem CategoryTheory.NatTrans.isIso_app_iff_of_iso {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor C D} (α : F G) {X Y : C} (e : X Y) :
        IsIso (α.app X) IsIso (α.app Y)