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 ifP f → P (e ≫ f)
andP f → P (f ≫ e)
, wheree
is an isomorphism.stable_under_composition
:P
is stable under composition ifP f → P g → P (f ≫ g)
.stable_under_base_change
:P
is stable under base change if in all pullback squares, the left map satisfiesP
if the right map satisfies it.
A morphism_property C
is a class of morphisms between objects in C
.
Equations
- category_theory.morphism_property C = Π ⦃X Y : C⦄, (X ⟶ Y) → Prop
Instances for category_theory.morphism_property
Equations
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.
Equations
- P.stable_under_composition = ∀ ⦃X Y Z : C⦄ (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (f ≫ g)
A morphism property is stable_under_inverse
if the inverse of a morphism satisfying
the property still falls in the class.
Equations
- P.stable_under_inverse = ∀ ⦃X Y : C⦄ (e : X ≅ Y), P e.hom → P e.inv
A morphism property is stable_under_base_change
if the base change of such a morphism
still falls in the class.
Equations
- P.stable_under_base_change = ∀ ⦃X Y Y' S : C⦄ ⦃f : X ⟶ S⦄ ⦃g : Y ⟶ S⦄ ⦃f' : Y' ⟶ Y⦄ ⦃g' : Y' ⟶ X⦄, category_theory.is_pullback f' g' g f → P g → P g'
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
- P.is_inverted_by F = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P f → category_theory.is_iso (F.map f)
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.