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
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'
@[simp]
theorem CategoryTheory.MorphismProperty.top_apply {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) :
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] {ι : Type 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
  • P.op f = P f.unop

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

Equations
  • P.unop f = P f.op

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

Equations
  • P.inverseImage F f = P (F.map f)
@[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
def CategoryTheory.MorphismProperty.homFamily {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) (f : P.toSet) :
(↑f).left (↑f).right

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

Equations
  • P.homFamily f = (↑f).hom
theorem CategoryTheory.MorphismProperty.homFamily_apply {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) (f : P.toSet) :
P.homFamily f = (↑f).hom
@[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) :
P.homFamily Arrow.mk f, hf = f
@[simp]
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
      class CategoryTheory.MorphismProperty.Respects {C : Type u} [Category.{v, u} C] (P Q : MorphismProperty C) extends P.RespectsLeft Q, P.RespectsRight Q :

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

      Instances
        instance CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight {C : Type u} [Category.{v, u} C] (P Q : MorphismProperty C) [P.RespectsLeft Q] [P.RespectsRight Q] :
        P.Respects Q
        instance CategoryTheory.MorphismProperty.instRespectsRightOppositeOpOfRespectsLeft {C : Type u} [Category.{v, u} C] (P Q : MorphismProperty C) [P.RespectsLeft Q] :
        P.op.RespectsRight Q.op
        instance CategoryTheory.MorphismProperty.instRespectsLeftOppositeOpOfRespectsRight {C : Type u} [Category.{v, u} C] (P Q : MorphismProperty C) [P.RespectsRight Q] :
        P.op.RespectsLeft Q.op
        instance CategoryTheory.MorphismProperty.RespectsLeft.inf {C : Type u} [Category.{v, u} C] (P₁ P₂ Q : MorphismProperty C) [P₁.RespectsLeft Q] [P₂.RespectsLeft Q] :
        (P₁ P₂).RespectsLeft Q
        instance CategoryTheory.MorphismProperty.RespectsRight.inf {C : Type u} [Category.{v, u} C] (P₁ P₂ Q : MorphismProperty C) [P₁.RespectsRight Q] [P₂.RespectsRight Q] :
        (P₁ P₂).RespectsRight Q
        @[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)) :
        P.RespectsIso
        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) :
        instance CategoryTheory.MorphismProperty.RespectsIso.op {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] :
        P.op.RespectsIso
        instance CategoryTheory.MorphismProperty.RespectsIso.unop {C : Type u} [Category.{v, u} C] (P : MorphismProperty Cᵒᵖ) [P.RespectsIso] :
        P.unop.RespectsIso

        The closure by isomorphisms of a MorphismProperty

        Equations
        theorem CategoryTheory.MorphismProperty.cancel_left_of_respectsIso {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [hP : P.RespectsIso] {X Y Z : C} (f : X Y) (g : Y Z) [IsIso f] :
        theorem CategoryTheory.MorphismProperty.cancel_right_of_respectsIso {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [hP : P.RespectsIso] {X Y Z : C} (f : X Y) (g : Y Z) [IsIso g] :
        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_iso_iff {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] {f g : Arrow C} (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
        theorem CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) (hP : ∀ (f g : Arrow C), (f g)P f.homP g.hom) :
        P.RespectsIso
        theorem CategoryTheory.MorphismProperty.isoClosure_eq_iff {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) :
        P.isoClosure = P P.RespectsIso
        theorem CategoryTheory.MorphismProperty.isoClosure_eq_self {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] :
        P.isoClosure = P
        @[simp]
        theorem CategoryTheory.MorphismProperty.isoClosure_isoClosure {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) :
        P.isoClosure.isoClosure = P.isoClosure
        theorem CategoryTheory.MorphismProperty.isoClosure_le_iff {C : Type u} [Category.{v, u} C] (P Q : MorphismProperty C) [Q.RespectsIso] :
        P.isoClosure Q P Q
        instance CategoryTheory.MorphismProperty.map_respectsIso {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty C) (F : Functor C D) :
        (P.map F).RespectsIso
        theorem CategoryTheory.MorphismProperty.map_le_iff {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty C) {F : Functor C D} (Q : MorphismProperty D) [Q.RespectsIso] :
        P.map F Q P Q.inverseImage F
        @[simp]
        theorem CategoryTheory.MorphismProperty.map_isoClosure {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty C) (F : Functor C D) :
        P.isoClosure.map F = P.map F
        theorem CategoryTheory.MorphismProperty.map_id {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) [P.RespectsIso] :
        P.map (Functor.id C) = P
        @[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)
        instance CategoryTheory.MorphismProperty.RespectsIso.inverseImage {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty D) [P.RespectsIso] (F : Functor C D) :
        (P.inverseImage F).RespectsIso
        theorem CategoryTheory.MorphismProperty.map_eq_of_iso {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty C) {F G : Functor C D} (e : F G) :
        P.map F = P.map G
        theorem CategoryTheory.MorphismProperty.map_inverseImage_le {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty D) (F : Functor C D) :
        (P.inverseImage F).map F P.isoClosure
        theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty D) [P.RespectsIso] (E : C D) :
        P.inverseImage E.functor = P.map E.inverse
        theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (Q : MorphismProperty C) [Q.RespectsIso] (E : C D) :
        Q.inverseImage E.inverse = Q.map E.functor
        theorem CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty D) [P.RespectsIso] (F : Functor C D) [F.IsEquivalence] :
        (P.inverseImage F).map F = P
        theorem CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (P : MorphismProperty C) [P.RespectsIso] (F : Functor C D) [F.IsEquivalence] :
        (P.map F).inverseImage F = P
        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
        • W.functorCategory J f = ∀ (j : J), W (f.app j)

        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)
        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)