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 are equivalent, see effectiveEpiStructOfRegularEpi,
regularEpiOfEffectiveEpi, and effectiveEpiOfKernelPair.
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 #
- [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.1, Example 2.1.12.
- nlab: Effective Epimorphism and
- Stacks 00WP for the standard definitions.
TODO #
- Find sufficient conditions on functors to preserve/reflect effective epis.
def
CategoryTheory.Sieve.EffectiveEpimorphic
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
(S : CategoryTheory.Sieve X)
:
A sieve is effective epimorphic if the associated cocone is a colimit cocone.
Equations
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Presieve.EffectiveEpimorphic
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
(S : CategoryTheory.Presieve X)
:
A presieve is effective epimorphic if the cocone associated to the sieve it generates is a colimit cocone.
Equations
Instances For
def
CategoryTheory.Sieve.generateSingleton
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
:
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
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Sieve.generateSingleton_eq
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
:
structure
CategoryTheory.EffectiveEpiStruct
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
:
Type (max u_1 u_2)
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)
- 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 (_ : ∀ {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 = self.desc 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)
Instances For
class
CategoryTheory.EffectiveEpi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
:
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)
Instances
noncomputable def
CategoryTheory.EffectiveEpi.getStruct
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
[CategoryTheory.EffectiveEpi f]
:
Some chosen EffectiveEpiStruct associated to an effective epi.
Equations
Instances For
noncomputable def
CategoryTheory.EffectiveEpi.desc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{W : C}
(f : Y ⟶ X)
[CategoryTheory.EffectiveEpi f]
(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)
:
X ⟶ W
Descend along an effective epi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.EffectiveEpi.fac_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{W : C}
(f : Y ⟶ X)
[CategoryTheory.EffectiveEpi f]
(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)
{Z : C}
(h : W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp f
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.EffectiveEpi.desc f 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))
h) = CategoryTheory.CategoryStruct.comp e h
@[simp]
theorem
CategoryTheory.EffectiveEpi.fac
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{W : C}
(f : Y ⟶ X)
[CategoryTheory.EffectiveEpi f]
(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.EffectiveEpi.desc f 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
theorem
CategoryTheory.EffectiveEpi.uniq
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{W : C}
(f : Y ⟶ X)
[CategoryTheory.EffectiveEpi f]
(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)
(hm : CategoryTheory.CategoryStruct.comp f m = e)
:
m = CategoryTheory.EffectiveEpi.desc f 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)
instance
CategoryTheory.epiOfEffectiveEpi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
[CategoryTheory.EffectiveEpi f]
:
Equations
- (_ : CategoryTheory.Epi f) = (_ : CategoryTheory.Epi f)
def
CategoryTheory.isColimitOfEffectiveEpiStruct
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
(Hf : CategoryTheory.EffectiveEpiStruct f)
:
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
noncomputable def
CategoryTheory.effectiveEpiStructOfIsColimit
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
(Hf : CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateSingleton f).arrows))
:
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
theorem
CategoryTheory.Sieve.effectiveEpimorphic_singleton
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : Y ⟶ X)
:
def
CategoryTheory.Sieve.generateFamily
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
:
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
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Sieve.generateFamily_eq
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
:
structure
CategoryTheory.EffectiveEpiFamilyStruct
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
:
Type (max (max u_1 u_2) u_3)
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)
- 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 (_ : ∀ {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 = self.desc 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₂))
Instances For
class
CategoryTheory.EffectiveEpiFamily
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
:
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₂ : α.
- effectiveEpiFamily : Nonempty (CategoryTheory.EffectiveEpiFamilyStruct X π)
Instances
noncomputable def
CategoryTheory.EffectiveEpiFamily.getStruct
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
:
Some chosen EffectiveEpiFamilyStruct associated to an effective epi family.
Equations
Instances For
noncomputable def
CategoryTheory.EffectiveEpiFamily.desc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{W : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
(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₂))
:
B ⟶ W
Descend along an effective epi family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.EffectiveEpiFamily.fac_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{W : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
(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 : α)
{Z : C}
(h : W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (π a)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.EffectiveEpiFamily.desc X π 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₂)))
h) = CategoryTheory.CategoryStruct.comp (e a) h
@[simp]
theorem
CategoryTheory.EffectiveEpiFamily.fac
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{W : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
(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.EffectiveEpiFamily.desc X π 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
def
CategoryTheory.effectiveEpiFamilyStructId
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{α : Unit → C}
:
CategoryTheory.EffectiveEpiFamilyStruct α fun (x : Unit) => CategoryTheory.CategoryStruct.id (α ())
The effective epi family structure on the identity
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpiFamilyUnitIdToCategoryStruct
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
:
CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) => CategoryTheory.CategoryStruct.id X
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.EffectiveEpiFamily.uniq
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{W : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
(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)
(hm : ∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a)
:
m = CategoryTheory.EffectiveEpiFamily.desc X π 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₂))
theorem
CategoryTheory.EffectiveEpiFamily.hom_ext
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{W : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
(m₁ : B ⟶ W)
(m₂ : B ⟶ W)
(h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m₁ = CategoryTheory.CategoryStruct.comp (π a) m₂)
:
m₁ = m₂
instance
CategoryTheory.epiCoproductDescOfEffectiveEpiFamily
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
[CategoryTheory.Limits.HasCoproduct X]
:
Equations
def
CategoryTheory.isColimitOfEffectiveEpiFamilyStruct
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
(H : CategoryTheory.EffectiveEpiFamilyStruct X π)
:
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
noncomputable def
CategoryTheory.effectiveEpiFamilyStructOfIsColimit
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
(H : CategoryTheory.Limits.IsColimit (CategoryTheory.Presieve.cocone (CategoryTheory.Sieve.generateFamily X π).arrows))
:
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
theorem
CategoryTheory.Sieve.effectiveEpimorphic_family
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
:
noncomputable def
CategoryTheory.effectiveEpiStructDescOfEffectiveEpiFamily
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.Limits.HasCoproduct X]
[CategoryTheory.EffectiveEpiFamily X π]
:
Given an EffectiveEpiFamily X π such that the coproduct of X exists, Sigma.desc π is an
EffectiveEpi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpiSigmaObjDesc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.Limits.HasCoproduct X]
[CategoryTheory.EffectiveEpiFamily X π]
:
Equations
theorem
CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
{X : α → C}
{π : (a : α) → X a ⟶ B}
[CategoryTheory.Limits.HasCoproduct X]
[∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)]
[∀ {Z : C} (g : Z ⟶ ∐ X),
CategoryTheory.Limits.HasCoproduct fun (a : α) => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)]
[∀ {Z : C} (g : Z ⟶ ∐ X),
CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun (a : α) => CategoryTheory.Limits.pullback.fst)]
{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₂))
{Z : C}
{g₁ : Z ⟶ ∐ fun (b : α) => X b}
{g₂ : Z ⟶ ∐ fun (b : α) => X b}
(hg : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc π) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc π))
:
This is an auxiliary lemma used twice in the definition of EffectiveEpiFamilyOfEffectiveEpiDesc.
It is the h hypothesis of EffectiveEpi.desc and EffectiveEpi.fac.
noncomputable def
CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.Limits.HasCoproduct X]
[CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π)]
[∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)]
[∀ {Z : C} (g : Z ⟶ ∐ X),
CategoryTheory.Limits.HasCoproduct fun (a : α) => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)]
[∀ {Z : C} (g : Z ⟶ ∐ X),
CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun (a : α) => CategoryTheory.Limits.pullback.fst)]
:
If a coproduct interacts well enough with pullbacks, then a family whose domains are the terms of
the coproduct is effective epimorphic whenever Sigma.desc induces an effective epimorphism from
the coproduct itself.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.EffectiveEpi f]
:
CategoryTheory.EffectiveEpiFamilyStruct (fun (x : Unit) => X) fun (x : Unit) =>
match x with
| PUnit.unit => f
An EffectiveEpiFamily consisting of a single EffectiveEpi
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpiFamily
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.EffectiveEpi f]
:
CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) =>
match x with
| PUnit.unit => f
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
CategoryTheory.effectiveEpiStructOfEffectiveEpiFamilySingleton
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) =>
match x with
| PUnit.unit => f]
:
A single element EffectiveEpiFamily constists of an EffectiveEpi
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) =>
match x with
| PUnit.unit => f]
:
Equations
- (_ : CategoryTheory.EffectiveEpi f) = (_ : CategoryTheory.EffectiveEpi f)
theorem
CategoryTheory.effectiveEpi_iff_effectiveEpiFamily
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
:
CategoryTheory.EffectiveEpi f ↔ CategoryTheory.EffectiveEpiFamily (fun (x : Unit) => X) fun (x : Unit) =>
match x with
| PUnit.unit => f
noncomputable def
CategoryTheory.effectiveEpiFamilyStructOfIsIsoDesc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.Limits.HasCoproduct X]
[CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)]
:
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
instance
CategoryTheory.instEffectiveEpiFamily_1
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.Limits.HasCoproduct X]
[CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)]
:
Equations
- (_ : CategoryTheory.EffectiveEpiFamily X π) = (_ : CategoryTheory.EffectiveEpiFamily X π)
noncomputable def
CategoryTheory.effectiveEpiStructOfIsIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
:
The identity is an effective epi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpi_1
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
:
Equations
- (_ : CategoryTheory.EffectiveEpi f) = (_ : CategoryTheory.EffectiveEpi f)
noncomputable def
CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
{Y : C}
(f : X ⟶ B)
(g : Y ⟶ X)
(i : X ⟶ Y)
(hi : CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.id X)
[CategoryTheory.EffectiveEpi f]
:
A split epi followed by an effective epi is an effective epi. This version takes an explicit section
to the split epi, and is mainly used to define effectiveEpiStructCompOfEffectiveEpiSplitEpi,
which takes a IsSplitEpi instance instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
{Y : C}
(f : X ⟶ B)
(g : Y ⟶ X)
[CategoryTheory.IsSplitEpi g]
[CategoryTheory.EffectiveEpi f]
:
A split epi followed by an effective epi is an effective epi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpiCompToCategoryStruct
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
{Y : C}
(f : X ⟶ B)
(g : Y ⟶ X)
[CategoryTheory.IsSplitEpi g]
[CategoryTheory.EffectiveEpi f]
:
Equations
def
CategoryTheory.effectiveEpiStructOfRegularEpi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.RegularEpi f]
:
The data of an EffectiveEpi structure on a RegularEpi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpi_2
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.RegularEpi f]
:
Equations
- (_ : CategoryTheory.EffectiveEpi f) = (_ : CategoryTheory.EffectiveEpi f)
theorem
CategoryTheory.effectiveEpiOfKernelPair
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.Limits.HasPullback f f]
(hc : CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.Cofork.ofπ f
(_ :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f)))
:
A morphism which is a coequalizer for its kernel pair is an effective epi.
noncomputable instance
CategoryTheory.regularEpiOfEffectiveEpi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.Limits.HasPullback f f]
[CategoryTheory.EffectiveEpi f]
:
An effective epi which has a kernel pair is a regular epi.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.effectiveEpi_iff_epi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
(h : ∀ {α : Type} [inst : Fintype α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B),
CategoryTheory.EffectiveEpiFamily X π ↔ CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π))
{X : C}
{Y : C}
(f : X ⟶ Y)
: