Effective epimorphic sieves #
We define the notion of effective epimorphic (pre)sieves and provide some API for relating the notion with the notions of effective epimorphism and effective epimorphic family.
More precisely, if f
is a morphism, then f
is an effective epi if and only if the sieve
it generates is effective epimorphic; see CategoryTheory.Sieve.effectiveEpimorphic_singleton
.
The analogous statement for a family of morphisms is in the theorem
CategoryTheory.Sieve.effectiveEpimorphic_family
.
A sieve is effective epimorphic if the associated cocone is a colimit cocone.
Instances For
A presieve is effective epimorphic if the cocone associated to the sieve it generates is a colimit cocone.
Instances For
The sieve of morphisms which factor through a given morphism f
.
This is equal to Sieve.generate (Presieve.singleton f)
, but has
more convenient definitional properties.
Equations
Instances For
Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sieve of morphisms which factor through a morphism in a given family.
This is equal to Sieve.generate (Presieve.ofArrows X π)
, but has
more convenient definitional properties.
Equations
Instances For
Implementation: This is a construction which will be used in the proof that the sieve generated by a family of arrows is effective epimorphic if and only if the family is an effective epi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation: This is a construction which will be used in the proof that the sieve generated by a family of arrows is effective epimorphic if and only if the family is an effective epi.
Equations
- One or more equations did not get rendered due to their size.