Commit 2023-06-01 17:10 4be56bf8

View on Github →

feat: CategoryTheory.Sites.Coherent -- define the coherent coverage and Grothendieck topology (#4505) As a requirement, we also define the notion of "effective epi" for morphisms and families of morphisms. We also define an analogous notion for (pre)sieves, and provide some API for the relationship between these notions.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Coherent.lean

added def CategoryTheory.coherentCoverage

added def CategoryTheory.coherentTopology

added theorem CategoryTheory.isSheaf_coherent

Created Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.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.Sieve.EffectiveEpimorphic

added theorem CategoryTheory.Sieve.effectiveEpimorphic_family

added theorem CategoryTheory.Sieve.effectiveEpimorphic_singleton

added def CategoryTheory.Sieve.generateFamily

added theorem CategoryTheory.Sieve.generateFamily_eq

added def CategoryTheory.Sieve.generateSingleton

added theorem CategoryTheory.Sieve.generateSingleton_eq

added def CategoryTheory.effectiveEpiFamilyStructOfIsColimit

added def CategoryTheory.effectiveEpiStructOfIsColimit

added def CategoryTheory.isColimitOfEffectiveEpiFamilyStruct

added def CategoryTheory.isColimitOfEffectiveEpiStruct