mathlib documentation


Properties of morphisms #

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

def category_theory.morphism_property (C : Type u) [category_theory.category C] :
Type (max u v)

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

Instances for category_theory.morphism_property

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


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


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


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

theorem category_theory.morphism_property.stable_under_base_change.pullback_map {C : Type u} [category_theory.category C] [category_theory.limits.has_pullbacks C] {P : category_theory.morphism_property C} (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 ( f g f' g' i₁ i₂ (𝟙 S) _ _)

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.

def category_theory.morphism_property.naturality_property {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {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.