# mathlibdocumentation

category_theory.morphism_property

# Properties of morphisms #

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

• respects_iso: P respects isomorphisms if P f → P (e ≫ f) and P f → P (f ≫ e), where e is an isomorphism.
• stable_under_composition: P is stable under composition if P f → P g → P (f ≫ g).
• stable_under_base_change: P is stable under base change if in all pullback squares, the left map satisfies P if the right map satisfies it.
def category_theory.morphism_property (C : Type u)  :
Type (max u v)

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

Equations
• = Π ⦃X Y : C⦄, (X Y) → Prop
Instances for category_theory.morphism_property
@[protected, instance]
@[protected, instance]
Equations

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

Equations

A morphism property is stable_under_composition if the composition of two such morphisms still falls in the class.

Equations

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

Equations

A morphism property is stable_under_base_change if the base change of such a morphism still falls in the class.

Equations
theorem category_theory.morphism_property.stable_under_composition.respects_iso {C : Type u} (hP : P.stable_under_composition) (hP' : ∀ {X Y : C} (e : X Y), P e.hom) :
theorem category_theory.morphism_property.respects_iso.cancel_left_is_iso {C : Type u} (hP : P.respects_iso) {X Y Z : C} (f : X Y) (g : Y Z)  :
P (f g) P g
theorem category_theory.morphism_property.respects_iso.cancel_right_is_iso {C : Type u} (hP : P.respects_iso) {X Y Z : C} (f : X Y) (g : Y Z)  :
P (f g) P f
theorem category_theory.morphism_property.respects_iso.arrow_mk_iso_iff {C : Type u} (hP : P.respects_iso) {W X Y Z : C} {f : W X} {g : Y Z}  :
P f P g
theorem category_theory.morphism_property.respects_iso.of_respects_arrow_iso {C : Type u} (hP : ∀ (f g : , (f g)P f.homP g.hom) :
theorem category_theory.morphism_property.stable_under_base_change.mk {C : Type u} (hP₁ : P.respects_iso) (hP₂ : ∀ (X Y S : C) (f : X S) (g : Y S), ) :
theorem category_theory.morphism_property.stable_under_base_change.fst {C : Type u} (hP : P.stable_under_base_change) {X Y S : C} (f : X S) (g : Y S) (H : P g) :
theorem category_theory.morphism_property.stable_under_base_change.snd {C : Type u} (hP : P.stable_under_base_change) {X Y S : C} (f : X S) (g : Y S) (H : P f) :
theorem category_theory.morphism_property.stable_under_base_change.base_change_map {C : Type u} (hP : P.stable_under_base_change) {S S' : C} (f : S' S) {X Y : category_theory.over S} (g : X Y) (H : P g.left) :
P
theorem category_theory.morphism_property.stable_under_base_change.pullback_map {C : Type u} (hP : P.stable_under_base_change) (hP' : P.stable_under_composition) {S X X' Y Y' : C} {f : X S} {g : Y S} {f' : X' S} {g' : Y' S} {i₁ : X X'} {i₂ : Y Y'} (h₁ : P i₁) (h₂ : P i₂) (e₁ : f = i₁ f') (e₂ : g = i₂ g') :
P g' i₁ i₂ (𝟙 S) _ _)
def category_theory.morphism_property.is_inverted_by {C : Type u} {D : Type u_1} (F : C D) :
Prop

If P : morphism_property C and F : C ⥤ D, then P.is_inverted_by F means that all morphisms in P are mapped by F to isomorphisms in D.

Equations
• = ∀ ⦃X Y : C⦄ (f : X Y), P f
@[simp]
def category_theory.morphism_property.naturality_property {C : Type u} {D : Type u_1} {F₁ F₂ : 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
theorem category_theory.morphism_property.naturality_property.is_stable_under_composition {C : Type u} {D : Type u_1} {F₁ F₂ : C D} (app : Π (X : C), F₁.obj X F₂.obj X) :
theorem category_theory.morphism_property.naturality_property.is_stable_under_inverse {C : Type u} {D : Type u_1} {F₁ F₂ : C D} (app : Π (X : C), F₁.obj X F₂.obj X) :