Compatibilities of properties of morphisms with respect to composition #
Given P : MorphismProperty C
, we define the predicate P.IsStableUnderComposition
which means that P f → P g → P (f ≫ g)
. We also introduce the type classes
W.ContainsIdentities
, W.IsMultiplicative
, and W.HasTwoOutOfThreeProperty
.
Typeclass expressing that a morphism property contain identities.
- id_mem : ∀ (X : C), W (CategoryTheory.CategoryStruct.id X)
for all
X : C
, the identity ofX
satisfies the morphism property
Instances
for all X : C
, the identity of X
satisfies the morphism property
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A morphism property satisfies IsStableUnderComposition
if the composition of
two such morphisms still falls in the class.
- comp_mem : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → P (CategoryTheory.CategoryStruct.comp f g)
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A morphism property is StableUnderInverse
if the inverse of a morphism satisfying
the property still falls in the class.
Instances For
Equations
- ⋯ = ⋯
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
- CategoryTheory.MorphismProperty.naturalityProperty app f = (CategoryTheory.CategoryStruct.comp (F₁.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (F₂.map f))
Instances For
Equations
- ⋯ = ⋯
A morphism property is multiplicative if it contains identities and is stable by composition.
- id_mem : ∀ (X : C), W (CategoryTheory.CategoryStruct.id X)
- comp_mem : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W g → W (CategoryTheory.CategoryStruct.comp f g)
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A class of morphisms W
has the two-out-of-three property if whenever two out
of three maps in f
, g
, f ≫ g
are in W
, then the third map is also in W
.
- comp_mem : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W g → W (CategoryTheory.CategoryStruct.comp f g)
- of_postcomp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W g → W (CategoryTheory.CategoryStruct.comp f g) → W f
- of_precomp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), W f → W (CategoryTheory.CategoryStruct.comp f g) → W g
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯