Commit 2024-04-07 20:38 345dab21

View on Github →

feat(CategoryTheory): a functor between FinitaryPreExtensive categories reflects finite effective epi families if it reflects effective epis (#11491) We prove that a functor between FinitaryPreExtensive categories preserves (resp. reflects) finite effective epi families if it preserves (resp. reflects) effective epis.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/EffectiveEpi/Extensive.lean

added theorem CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily

Modified Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean

deleted theorem CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily

Modified Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean

Modified Mathlib/Topology/Category/Profinite/EffectiveEpi.lean