mathlib documentation

category_theory.morphism_property

Properties of morphisms #

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

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

Equations
Instances for category_theory.morphism_property
@[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

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

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

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.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 (category_theory.limits.pullback.map 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.

Equations
theorem category_theory.morphism_property.is_inverted_by.of_comp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [category_theory.category C₁] [category_theory.category C₂] [category_theory.category C₃] (W : category_theory.morphism_property C₁) (F : C₁ C₂) (hF : W.is_inverted_by F) (G : C₂ C₃) :
@[simp]

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

The morphism_property C satisfied by isomorphisms in C.

Equations

The morphism_property C satisfied by monomorphisms in C.

Equations

The morphism_property C satisfied by epimorphisms in C.

Equations
@[nolint]

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

Equations
Instances for category_theory.morphism_property.functors_inverting

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

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
@[protected]

Surjectiveness (in a concrete category) as a morphism_property

Equations
@[protected]

Bijectiveness (in a concrete category) as a morphism_property

Equations