Theorem CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily

Modification history

2024-04-07 20:38
Mathlib/CategoryTheory/EffectiveEpi/Extensive.lean
feat(CategoryTheory): a functor between `FinitaryPreExtensive` categories reflects finite effective epi families if it reflects effective epis (#11491) …
Modified CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamilyView on Github →
2024-02-10 10:41
Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean
chore(CategoryTheory/Sites): reorganise the material related to the coherent, regular and extensive topologies (#9944) …
Modified CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamilyView on Github →
2024-02-04 21:28
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
chore(Topology/Category): `[Fintype _]` -> `[Finite _]` (#10257)
Modified CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamilyView on Github →
2023-11-30 10:58
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
feat(CategoryTheory): `Preregular` and `FinitaryPreExtensive` implies `Precoherent` (#8643) …
Added CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamilyView on Github →