Commit 2023-12-05 08:35 c5eb45f0

View on Github →

feat(Condensed): Explicit descriptions of condensed sets (#6731) We prove the characterisation of condensed sets as finite-product preserving presheaves satisfying the equalizer condition on CompHaus/Profinite, and just finite-product preserving presheaves on Stonean.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

Created Mathlib/Condensed/Explicit.lean

added theorem CategoryTheory.isSheaf_coherent_iff_regular_and_extensive

added theorem CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'

added theorem CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition

added theorem CondensedSet.equalizerCondition

added theorem Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'

added theorem Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition

added theorem Stonean.isSheaf_iff_preservesFiniteProducts'

added theorem Stonean.isSheaf_iff_preservesFiniteProducts