# Properties of morphisms #

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

• RespectsIso: P respects isomorphisms if P f → P (e ≫ f) and P f → P (f ≫ e), where e is an isomorphism.

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

Equations
• = (⦃X Y : C⦄ → (X Y)Prop)
Instances For
Equations
theorem CategoryTheory.MorphismProperty.le_def (C : Type u) :
P Q ∀ {X Y : C} (f : X Y), P fQ f
Equations
• = { default := }
theorem CategoryTheory.MorphismProperty.top_eq (C : Type u) :
= fun (x x_1 : C) (x : x x_1) => True
theorem CategoryTheory.MorphismProperty.ext_iff {C : Type u} {W' : } :
W = W' ∀ ⦃X Y : C⦄ (f : X Y), W f W' f
theorem CategoryTheory.MorphismProperty.ext {C : Type u} (W' : ) (h : ∀ ⦃X Y : C⦄ (f : X Y), W f W' f) :
W = W'
@[simp]
theorem CategoryTheory.MorphismProperty.top_apply {C : Type u} {X : C} {Y : C} (f : X Y) :
f

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
def CategoryTheory.MorphismProperty.inverseImage {C : Type u} {D : Type u_1} [] (F : ) :

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

Equations
• P.inverseImage F f = P (F.map f)
Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.inverseImage_iff {C : Type u} {D : Type u_1} [] (F : ) {X : C} {Y : C} (f : X Y) :
P.inverseImage F f P (F.map f)
def CategoryTheory.MorphismProperty.map {C : Type u} {D : Type u_1} [] (F : ) :

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

Equations
Instances For
theorem CategoryTheory.MorphismProperty.map_mem_map {C : Type u} {D : Type u_1} [] (F : ) {X : C} {Y : C} (f : X Y) (hf : P f) :
P.map F (F.map f)
theorem CategoryTheory.MorphismProperty.monotone_map {C : Type u} {D : Type u_1} [] (F : ) :
Monotone fun (x : ) => x.map F

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

• precomp : ∀ {X Y Z : C} (e : X Y) (f : Y Z), P fP
• postcomp : ∀ {X Y Z : C} (e : Y Z) (f : X Y), P fP
Instances
theorem CategoryTheory.MorphismProperty.RespectsIso.precomp {C : Type u} [self : P.RespectsIso] {X : C} {Y : C} {Z : C} (e : X Y) (f : Y Z) (hf : P f) :
P
theorem CategoryTheory.MorphismProperty.RespectsIso.postcomp {C : Type u} [self : P.RespectsIso] {X : C} {Y : C} {Z : C} (e : Y Z) (f : X Y) (hf : P f) :
P
instance CategoryTheory.MorphismProperty.RespectsIso.op {C : Type u} [h : P.RespectsIso] :
P.op.RespectsIso
Equations
• =
instance CategoryTheory.MorphismProperty.RespectsIso.unop {C : Type u} [h : P.RespectsIso] :
P.unop.RespectsIso
Equations
• =
instance CategoryTheory.MorphismProperty.RespectsIso.inf {C : Type u} [P.RespectsIso] [Q.RespectsIso] :
(P Q).RespectsIso

The intersection of two isomorphism respecting morphism properties respects isomorphisms.

Equations
• =

The closure by isomorphisms of a MorphismProperty

Equations
• P.isoClosure f = ∃ (Y₁ : C) (Y₂ : C) (f' : Y₁ Y₂) (_ : P f'),
Instances For
instance CategoryTheory.MorphismProperty.isoClosure_respectsIso {C : Type u} :
P.isoClosure.RespectsIso
Equations
• =
theorem CategoryTheory.MorphismProperty.monotone_isoClosure {C : Type u} :
Monotone CategoryTheory.MorphismProperty.isoClosure
theorem CategoryTheory.MorphismProperty.cancel_left_of_respectsIso {C : Type u} [hP : P.RespectsIso] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
P g
theorem CategoryTheory.MorphismProperty.cancel_right_of_respectsIso {C : Type u} [hP : P.RespectsIso] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
P f
theorem CategoryTheory.MorphismProperty.arrow_iso_iff {C : Type u} [P.RespectsIso] {f : } {g : } (e : f g) :
P f.hom P g.hom
theorem CategoryTheory.MorphismProperty.arrow_mk_iso_iff {C : Type u} [P.RespectsIso] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} :
P f P g
theorem CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso {C : Type u} (hP : ∀ (f g : ), (f g)P f.homP g.hom) :
P.RespectsIso
theorem CategoryTheory.MorphismProperty.isoClosure_eq_iff {C : Type u} :
P.isoClosure = P P.RespectsIso
theorem CategoryTheory.MorphismProperty.isoClosure_eq_self {C : Type u} [P.RespectsIso] :
P.isoClosure = P
@[simp]
theorem CategoryTheory.MorphismProperty.isoClosure_isoClosure {C : Type u} :
P.isoClosure.isoClosure = P.isoClosure
theorem CategoryTheory.MorphismProperty.isoClosure_le_iff {C : Type u} [Q.RespectsIso] :
P.isoClosure Q P Q
instance CategoryTheory.MorphismProperty.map_respectsIso {C : Type u} {D : Type u_1} [] (F : ) :
(P.map F).RespectsIso
Equations
• =
theorem CategoryTheory.MorphismProperty.map_le_iff {C : Type u} {D : Type u_1} [] {F : } [Q.RespectsIso] :
P.map F Q P Q.inverseImage F
@[simp]
theorem CategoryTheory.MorphismProperty.map_isoClosure {C : Type u} {D : Type u_1} [] (F : ) :
P.isoClosure.map F = P.map F
theorem CategoryTheory.MorphismProperty.map_id {C : Type u} [P.RespectsIso] :
P.map = P
@[simp]
theorem CategoryTheory.MorphismProperty.map_map {C : Type u} {D : Type u_1} [] (F : ) {E : Type u_2} [] (G : ) :
(P.map F).map G = P.map (F.comp G)
instance CategoryTheory.MorphismProperty.RespectsIso.inverseImage {C : Type u} {D : Type u_1} [] [P.RespectsIso] (F : ) :
(P.inverseImage F).RespectsIso
Equations
• =
theorem CategoryTheory.MorphismProperty.map_eq_of_iso {C : Type u} {D : Type u_1} [] {F : } {G : } (e : F G) :
P.map F = P.map G
theorem CategoryTheory.MorphismProperty.map_inverseImage_le {C : Type u} {D : Type u_1} [] (F : ) :
(P.inverseImage F).map F P.isoClosure
theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor {C : Type u} {D : Type u_1} [] [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} {D : Type u_1} [] [Q.RespectsIso] (E : C D) :
Q.inverseImage E.inverse = Q.map E.functor
theorem CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence {C : Type u} {D : Type u_1} [] [P.RespectsIso] (F : ) [F.IsEquivalence] :
(P.inverseImage F).map F = P
theorem CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence {C : Type u} {D : Type u_1} [] [P.RespectsIso] (F : ) [F.IsEquivalence] :
(P.map F).inverseImage F = P

The MorphismProperty C satisfied by isomorphisms in C.

Equations
Instances For

The MorphismProperty C satisfied by monomorphisms in C.

Equations
Instances For

The MorphismProperty C satisfied by epimorphisms in C.

Equations
Instances For
@[simp]
theorem CategoryTheory.MorphismProperty.isomorphisms.iff {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MorphismProperty.monomorphisms.iff {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.MorphismProperty.epimorphisms.iff {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.MorphismProperty.isomorphisms.infer_property {C : Type u} {X : C} {Y : C} (f : X Y) [hf : ] :
theorem CategoryTheory.MorphismProperty.monomorphisms.infer_property {C : Type u} {X : C} {Y : C} (f : X Y) [hf : ] :
theorem CategoryTheory.MorphismProperty.epimorphisms.infer_property {C : Type u} {X : C} {Y : C} (f : X Y) [hf : ] :
Equations
• =
Equations
• =
Equations
• =
@[deprecated CategoryTheory.MorphismProperty.cancel_left_of_respectsIso]
theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso {C : Type u} [hP : P.RespectsIso] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
P g

Alias of CategoryTheory.MorphismProperty.cancel_left_of_respectsIso.

@[deprecated CategoryTheory.MorphismProperty.cancel_right_of_respectsIso]
theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso {C : Type u} [hP : P.RespectsIso] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
P f

Alias of CategoryTheory.MorphismProperty.cancel_right_of_respectsIso.

@[deprecated CategoryTheory.MorphismProperty.arrow_iso_iff]
theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_iso_iff {C : Type u} [P.RespectsIso] {f : } {g : } (e : f g) :
P f.hom P g.hom

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} [P.RespectsIso] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : Y Z} :
P f P g

Alias of CategoryTheory.MorphismProperty.arrow_mk_iso_iff.

@[deprecated CategoryTheory.MorphismProperty.isoClosure_eq_self]
theorem CategoryTheory.MorphismProperty.RespectsIso.isoClosure_eq {C : Type u} [P.RespectsIso] :
P.isoClosure = P

Alias of CategoryTheory.MorphismProperty.isoClosure_eq_self.

def CategoryTheory.MorphismProperty.prod {C₁ : Type u_2} {C₂ : Type u_3} [] [] (W₁ : ) (W₂ : ) :

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) → ] (W : (j : 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
• = ∀ (j : J), W j (f j)
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
theorem CategoryTheory.NatTrans.isIso_app_iff_of_iso {C : Type u} {D : Type u_1} [] {F : } {G : } (α : F G) {X : C} {Y : C} (e : X Y) :