# mathlib3documentation

category_theory.morphism_property

# Properties of morphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.
• stable_under_cobase_change: P is stable under cobase change if in all pushout squares, the right map satisfies P if the left 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
Instances for category_theory.morphism_property
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]

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

Equations
Instances for category_theory.morphism_property.op
@[simp]

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

Equations
def category_theory.morphism_property.inverse_image {C : Type u} {D : Type u_1} (F : C D) :

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

Equations
• = λ (X Y : C) (f : X Y), P (F.map f)

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

A morphism property is stable_under_cobase_change if the cobase change of such a morphism still falls in the class.

Equations
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.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.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) _ _)
theorem category_theory.morphism_property.stable_under_cobase_change.mk {C : Type u} (hP₁ : P.respects_iso) (hP₂ : (A B A' : C) (f : A A') (g : A B), ) :
theorem category_theory.morphism_property.stable_under_cobase_change.inl {C : Type u} (hP : P.stable_under_cobase_change) {A B A' : C} (f : A A') (g : A B) (H : P g) :
theorem category_theory.morphism_property.stable_under_cobase_change.inr {C : Type u} (hP : P.stable_under_cobase_change) {A B A' : C} (f : A A') (g : A B) (H : P f) :
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
theorem category_theory.morphism_property.is_inverted_by.of_comp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} (F : C₁ C₂) (hF : W.is_inverted_by F) (G : C₂ C₃) :
@[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) :

The morphism_property C satisfied by isomorphisms in C.

Equations
• = λ (X Y : C) (f : X Y),

The morphism_property C satisfied by monomorphisms in C.

Equations
• = λ (X Y : C) (f : X Y),

The morphism_property C satisfied by epimorphisms in C.

Equations
• = λ (X Y : C) (f : X Y),
@[simp]
theorem category_theory.morphism_property.isomorphisms.iff {C : Type u} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.morphism_property.monomorphisms.iff {C : Type u} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.morphism_property.epimorphisms.iff {C : Type u} {X Y : C} (f : X Y) :
@[nolint]
def category_theory.morphism_property.functors_inverting {C : Type u} (D : Type u_1)  :
Type (max v u_2 u u_1)

The full subcategory of C ⥤ D consisting of functors inverting morphisms in W

Equations
Instances for category_theory.morphism_property.functors_inverting
@[protected, instance]

A constructor for W.functors_inverting D

Equations
theorem category_theory.morphism_property.is_inverted_by.iff_of_iso {C : Type u} {D : Type u_1} {F₁ F₂ : C D} (e : F₁ F₂) :

For P : morphism_property C, P.diagonal is a morphism property that holds for f : X ⟶ Y whenever P holds for X ⟶ Y xₓ Y.

Equations
theorem category_theory.morphism_property.diagonal_iff {C : Type u} {X Y : C} {f : X Y} :

P.universally holds for a morphism f : X ⟶ Y iff P holds for all X ×[Y] Y' ⟶ Y'.

Equations
@[protected]

Injectiveness (in a concrete category) as a morphism_property

Equations
• = λ (X Y : C) (f : X Y),
@[protected]

Surjectiveness (in a concrete category) as a morphism_property

Equations
• = λ (X Y : C) (f : X Y),
@[protected]

Bijectiveness (in a concrete category) as a morphism_property

Equations
• = λ (X Y : C) (f : X Y),