Commit 2023-11-30 10:58 a12664fb

View on Github →

feat(CategoryTheory): Preregular and FinitaryPreExtensive implies Precoherent (#8643) We prove some results about effective epimorphisms which allow us to deduce that a category which is FinitaryPreExtensive and Preregular is also Precoherent.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

Modified Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

deleted def CategoryTheory.EffectiveEpiFamilyStruct_of_isIso_desc

deleted def CategoryTheory.EffectiveEpiFamily_descStruct

deleted def CategoryTheory.EffectiveEpiStructId

deleted def CategoryTheory.EffectiveEpiStruct_ofFamily

deleted def CategoryTheory.EffectiveEpi_familyStruct

modified def CategoryTheory.effectiveEpiFamilyStructId

added def CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc

added theorem CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux

added def CategoryTheory.effectiveEpiFamilyStructOfIsIsoDesc

added def CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi

added def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi'

added def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi

added def CategoryTheory.effectiveEpiStructDescOfEffectiveEpiFamily

added def CategoryTheory.effectiveEpiStructOfEffectiveEpiFamilySingleton

added def CategoryTheory.effectiveEpiStructOfIsIso

modified theorem CategoryTheory.effectiveEpi_iff_effectiveEpiFamily

Modified Mathlib/CategoryTheory/Sites/RegularExtensive.lean

added theorem CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily

modified theorem CategoryTheory.extensive_regular_generate_coherent