Commit 2024-03-19 13:54 6d4365db

View on Github →

chore(CategoryTheory): split the file CategoryTheory/Sites/EffectiveEpimorphic/Basic.lean (#11458) Adds no new material, just splits the file into smaller chunks and removes a couple of useless lemmas.

depends on: #11457

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/EffectiveEpi/Basic.lean

added def CategoryTheory.EffectiveEpi.desc

added theorem CategoryTheory.EffectiveEpi.fac

added def CategoryTheory.EffectiveEpi.getStruct

added theorem CategoryTheory.EffectiveEpi.uniq

added def CategoryTheory.EffectiveEpiFamily.desc

added theorem CategoryTheory.EffectiveEpiFamily.fac

added def CategoryTheory.EffectiveEpiFamily.getStruct

added theorem CategoryTheory.EffectiveEpiFamily.hom_ext

added theorem CategoryTheory.EffectiveEpiFamily.uniq

added structure CategoryTheory.EffectiveEpiFamilyStruct

added structure CategoryTheory.EffectiveEpiStruct

added def CategoryTheory.effectiveEpiFamilyStructOfIsIsoDesc

added def CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi

added def CategoryTheory.effectiveEpiStructOfEffectiveEpiFamilySingleton

added def CategoryTheory.effectiveEpiStructOfIsIso

added theorem CategoryTheory.effectiveEpi_iff_effectiveEpiFamily

Created Mathlib/CategoryTheory/EffectiveEpi/Comp.lean

added def CategoryTheory.effectiveEpiFamilyStructCompIso

added theorem CategoryTheory.effectiveEpiFamilyStructCompIso_aux

added def CategoryTheory.effectiveEpiFamilyStructIsoComp

added theorem CategoryTheory.effectiveEpiFamilyStructIsoComp_aux

added def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi'

added def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi

Created Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean

added def CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc

added theorem CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux

added def CategoryTheory.effectiveEpiStructDescOfEffectiveEpiFamily

added def CategoryTheory.effectiveEpiStructIsColimitDescOfEffectiveEpiFamily

Created Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean

added def CategoryTheory.effectiveEpiFamilyStructOfEquivalence

added theorem CategoryTheory.effectiveEpiFamilyStructOfEquivalence_aux

Created Mathlib/CategoryTheory/EffectiveEpi/RegularEpi.lean

added theorem CategoryTheory.effectiveEpiOfKernelPair

added def CategoryTheory.effectiveEpiStructOfRegularEpi

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

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

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

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

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

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

modified theorem CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi

modified theorem CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi

Modified Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

deleted def CategoryTheory.EffectiveEpi.desc

deleted theorem CategoryTheory.EffectiveEpi.fac

deleted def CategoryTheory.EffectiveEpi.getStruct

deleted theorem CategoryTheory.EffectiveEpi.uniq

deleted def CategoryTheory.EffectiveEpiFamily.desc

deleted theorem CategoryTheory.EffectiveEpiFamily.fac

deleted def CategoryTheory.EffectiveEpiFamily.getStruct

deleted theorem CategoryTheory.EffectiveEpiFamily.hom_ext

deleted theorem CategoryTheory.EffectiveEpiFamily.uniq

deleted structure CategoryTheory.EffectiveEpiFamilyStruct

deleted structure CategoryTheory.EffectiveEpiStruct

deleted def CategoryTheory.effectiveEpiFamilyStructCompIso

deleted theorem CategoryTheory.effectiveEpiFamilyStructCompIso_aux

deleted def CategoryTheory.effectiveEpiFamilyStructId

deleted def CategoryTheory.effectiveEpiFamilyStructIsoComp

deleted theorem CategoryTheory.effectiveEpiFamilyStructIsoComp_aux

deleted def CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc

deleted theorem CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux

deleted def CategoryTheory.effectiveEpiFamilyStructOfEquivalence

deleted theorem CategoryTheory.effectiveEpiFamilyStructOfEquivalence_aux

deleted def CategoryTheory.effectiveEpiFamilyStructOfIsIsoDesc

deleted def CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi

deleted theorem CategoryTheory.effectiveEpiOfKernelPair

deleted def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi'

deleted def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi

deleted def CategoryTheory.effectiveEpiStructDescOfEffectiveEpiFamily

deleted def CategoryTheory.effectiveEpiStructIsColimitDescOfEffectiveEpiFamily

deleted def CategoryTheory.effectiveEpiStructOfEffectiveEpiFamilySingleton

deleted def CategoryTheory.effectiveEpiStructOfIsIso

deleted def CategoryTheory.effectiveEpiStructOfRegularEpi

deleted theorem CategoryTheory.effectiveEpi_iff_effectiveEpiFamily

deleted theorem CategoryTheory.effectiveEpi_iff_epi

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