Commit 2024-05-23 09:04 fda1d3c3

View on Github →

feat(Condensed): prove the explicit sheaf condition for a general target category (#12870)

depends on: #12909

Estimated changes

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

added theorem CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts

added theorem CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts

deleted theorem CategoryTheory.isSheaf_iff_preservesFiniteProducts

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

added theorem CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensive

added theorem CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_comp

added theorem CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp

added theorem CategoryTheory.Presheaf.isSheaf_coherent_of_projective_comp

added theorem CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp

added theorem CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition

added theorem CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective

Modified Mathlib/Condensed/Explicit.lean

deleted theorem CategoryTheory.isSheaf_coherent_iff_regular_and_extensive

deleted theorem CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'

deleted theorem CompHaus.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition

added theorem Condensed.equalizerCondition

added theorem Condensed.equalizerCondition_profinite

deleted theorem CondensedSet.equalizerCondition

deleted theorem Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'

deleted theorem Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition

deleted theorem Stonean.isSheaf_iff_preservesFiniteProducts'

deleted theorem Stonean.isSheaf_iff_preservesFiniteProducts