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) : CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π) ↔ CategoryTheory.EffectiveEpiFamily X π

instance CategoryTheory.instReflectsFiniteEffectiveEpiFamilies {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] [CategoryTheory.Functor.ReflectsEffectiveEpis F] : CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies F

Equations

• ⋯ = ⋯

instance CategoryTheory.instPreservesFiniteEffectiveEpiFamilies {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] [CategoryTheory.Functor.PreservesEffectiveEpis F] : CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies F

Equations

• ⋯ = ⋯