Properties of morphisms #
We provide the basic framework for talking about properties of morphisms. The following meta-property is defined
RespectsLeft P Q
:P
respects the propertyQ
on the left ifP f → P (i ≫ f)
wherei
satisfiesQ
.RespectsRight P Q
:P
respects the propertyQ
on the right ifP f → P (f ≫ i)
wherei
satisfiesQ
.Respects
:P
respectsQ
ifP
respectsQ
both on the left and on the right.
A MorphismProperty C
is a class of morphisms between objects in C
.
Instances For
The morphism property in Cᵒᵖ
associated to a morphism property in C
Instances For
The morphism property in C
associated to a morphism property in Cᵒᵖ
Instances For
The inverse image of a MorphismProperty D
by a functor C ⥤ D
Instances For
The image (up to isomorphisms) of a MorphismProperty C
by a functor C ⥤ D
Equations
Instances For
The set in Set (Arrow C)
which corresponds to P : MorphismProperty C
.
Instances For
The family of morphisms indexed by P.toSet
which corresponds
to P : MorphismProperty C
, see MorphismProperty.ofHoms_homFamily
.
Equations
Instances For
The class of morphisms given by a family of morphisms f i : X i ⟶ Y i
.
- mk {C : Type u} [Category.{v, u} C] {ι : Type u_2} {X Y : ι → C} {f : (i : ι) → X i ⟶ Y i} (i : ι) : ofHoms f (f i)
Instances For
A morphism property P
satisfies P.RespectsRight Q
if it is stable under post-composition
with morphisms satisfying Q
, i.e. whenever P
holds for f
and Q
holds for i
then P
holds for f ≫ i
.
Instances
A morphism property P
satisfies P.RespectsLeft Q
if it is stable under
pre-composition with morphisms satisfying Q
, i.e. whenever P
holds for f
and Q
holds for i
then P
holds for i ≫ f
.
Instances
A morphism property P
satisfies P.Respects Q
if it is stable under composition on the
left and right by morphisms satisfying Q
.
Instances
P
respects isomorphisms, if it respects the morphism property isomorphisms C
, i.e.
it is stable under pre- and postcomposition with isomorphisms.
Instances For
The closure by isomorphisms of a MorphismProperty
Equations
Instances For
If W₁
and W₂
are morphism properties on two categories C₁
and C₂
,
this is the induced morphism property on C₁ × C₂
.
Equations
- W₁.prod W₂ f = (W₁ f.1 ∧ W₂ f.2)
Instances For
If W j
are morphism properties on categories C j
for all j
, this is the
induced morphism property on the category ∀ j, C j
.
Instances For
The morphism property on J ⥤ C
which is defined objectwise
from W : MorphismProperty C
.
Equations
Instances For
Given W : MorphismProperty C
, this is the morphism property on Arrow C
of morphisms
whose left and right parts are in W
.