Effective epimorphisms #
We define the notion of effective epimorphism and effective epimorphic family of morphisms.
A morphism is an effective epi if it is a joint coequalizer of all pairs of morphisms which it coequalizes.
A family of morphisms with fixed target is effective epimorphic if it is initial among families of morphisms with its sources and a general fixed target, coequalizing every pair of morphisms it coequalizes (here, the pair of morphisms coequalized can have different targets among the sources of the 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 are equivalent, see the file
CategoryTheory/EffectiveEpi/RegularEpi.lean
See nlab: Effective Epimorphism and
Stacks 00WP for the standard definitions. Note that
our notion of EffectiveEpi
is often called "strict epi" in the literature.
References #
- [Joh02]: Sketches of an Elephant, P. T. Johnstone: C2.1, Example 2.1.12.
- nlab: Effective Epimorphism and
- Stacks 00WP for the standard definitions.
This structure encodes the data required for a morphism to be an effective epimorphism.
- 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)
For every
W
with a morphisme : Y ⟶ W
that coequalizes every pair of morphismsg₁ g₂ : Z ⟶ Y
whichf
coequalizes,desc e h
is a morphismX ⟶ 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 (self.desc e ⋯) = e
...factorizing
e
throughf
... - 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 = self.desc e ⋯
...and as such, unique.
Instances For
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.
- effectiveEpi : Nonempty (CategoryTheory.EffectiveEpiStruct f)
f
is an effective epimorphism if there exists anEffectiveEpiStruct
forf
.
Instances
Some chosen EffectiveEpiStruct
associated to an effective epi.
Equations
- CategoryTheory.EffectiveEpi.getStruct f = ⋯.some
Instances For
Descend along an effective epi.
Equations
- CategoryTheory.EffectiveEpi.desc f e h = (CategoryTheory.EffectiveEpi.getStruct f).desc e ⋯
Instances For
This structure encodes the data required for a family of morphisms to be effective epimorphic.
- 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)
For every
W
with a family of morphismse a : Y a ⟶ W
that coequalizes every pair of morphismsg₁ : Z ⟶ Y a₁
,g₂ : Z ⟶ Y a₂
which the familyπ
coequalizes,desc e h
is a morphismX ⟶ 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) (self.desc e ⋯) = e a
...factorizing the components of
e
through the components ofπ
... - 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 = self.desc e ⋯
...and as such, unique.
Instances For
A family of morphisms π a : X a ⟶ B
indexed by α
is effective epimorphic
provided that the π a
exhibit B
as a colimit of the diagram of all "relations"
R → X a₁
, R ⟶ X a₂
for all a₁ a₂ : α
.
- effectiveEpiFamily : Nonempty (CategoryTheory.EffectiveEpiFamilyStruct X π)
π
is an effective epimorphic family if there exists anEffectiveEpiFamilyStruct
forπ
Instances
Some chosen EffectiveEpiFamilyStruct
associated to an effective epi family.
Equations
- CategoryTheory.EffectiveEpiFamily.getStruct X π = ⋯.some
Instances For
Descend along an effective epi family.
Equations
- CategoryTheory.EffectiveEpiFamily.desc X π e h = (CategoryTheory.EffectiveEpiFamily.getStruct X π).desc e ⋯
Instances For
An EffectiveEpiFamily
consisting of a single EffectiveEpi
Equations
- One or more equations did not get rendered due to their size.
Instances For
A single element EffectiveEpiFamily
consists of an EffectiveEpi
Equations
- One or more equations did not get rendered due to their size.
Instances For
A family of morphisms with the same target inducing an isomorphism from the coproduct to the target
is an EffectiveEpiFamily
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Any isomorphism is an effective epi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reindex the indexing type of an effective epi family struct.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reindex the indexing type of an effective epi family.