Effective epimorphisms #
We define the notion of effective epimorphic (pre)sieves, morphisms and family of morphisms and provide some API for relating the three notions.
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
.
We have defined the notion of effective epi for morphisms and families of morphisms in such a way that avoids requiring the existence of pullbacks. However, if the relevant pullbacks exist then these definitions should be equivalent (project: formalize this!). See nlab: Effective Epimorphism and Stacks 00WP for the standard definitions.
References #
- [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.1, Example 2.1.12.
- nlab: Effective Epimorphism and
- Stacks 00WP for the standard definitions.
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.
Instances For
- desc : {W : C} → (e : Y ⟶ W) → (∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) → (X ⟶ W)
- fac : ∀ {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e), CategoryTheory.CategoryStruct.comp f (CategoryTheory.EffectiveEpiStruct.desc s e (_ : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)) = e
- uniq : ∀ {W : C} (e : Y ⟶ W) (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = CategoryTheory.EffectiveEpiStruct.desc s e (_ : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
This structure encodes the data required for a morphism to be an effective epimorphism.
Instances For
- effectiveEpi : Nonempty (CategoryTheory.EffectiveEpiStruct f)
A morphism f : Y ⟶ X
is an effective epimorphism provided that f
exhibits X
as a colimit
of the diagram of all "relations" R ⇉ Y
.
If f
has a kernel pair, then this is equivalent to showing that the corresponding cofork is
a colimit.
Instances
Some chosen EffectiveEpiStruct
associated to an effective epi.
Instances For
Descend along an effective epi.
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.
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.
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.
Instances For
- desc : {W : C} → (e : (a : α) → X a ⟶ W) → (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) → (B ⟶ W)
- fac : ∀ {W : C} (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (a : α), CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.EffectiveEpiFamilyStruct.desc s e (_ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))) = e a
- uniq : ∀ {W : C} (e : (a : α) → X a ⟶ W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = CategoryTheory.EffectiveEpiFamilyStruct.desc s e (_ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
This structure encodes the data required for a family of morphisms to be effective epimorphic.
Instances For
- effectiveEpiFamily : Nonempty (CategoryTheory.EffectiveEpiFamilyStruct X π)
A family of morphisms f a : X a ⟶ B
indexed by α
is effective epimorphic
provided that the f a
exhibit B
as a colimit of the diagram of all "relations"
R → X a₁
, R ⟶ X a₂
for all a₁ a₂ : α
.
Instances
Some chosen EffectiveEpiFamilyStruct
associated to an effective epi family.
Instances For
Descend along an effective epi family.
Instances For
The effective epi family structure on the identity
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.
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.
Instances For
Given an EffectiveEpiFamily X π
such that the coproduct of X
exists, Sigma.desc π
is an
EffectiveEpi
.
Instances For
An EffectiveEpiFamily
consisting of a single EffectiveEpi
Instances For
A family of morphisms with the same target inducing an isomorphism from the coproduct to the target
is an EffectiveEpiFamily
.