Preserving and reflecting effective epis on extensive categories #
We prove that a functor between FinitaryPreExtensive categories preserves (resp. reflects) finite
effective epi families if it preserves (resp. reflects) effective epis.
theorem
CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.FinitaryPreExtensive C]
{α : Type}
[Finite α]
{B : C}
(X : α → C)
(π : (a : α) → X a ⟶ B)
:
instance
CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.FinitaryPreExtensive C]
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.FinitaryPreExtensive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesFiniteCoproducts F]
[F.ReflectsEffectiveEpis]
:
F.ReflectsFiniteEffectiveEpiFamilies
Equations
- ⋯ = ⋯
instance
CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.FinitaryPreExtensive C]
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.FinitaryPreExtensive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesFiniteCoproducts F]
[F.PreservesEffectiveEpis]
:
F.PreservesFiniteEffectiveEpiFamilies
Equations
- ⋯ = ⋯