Theorem Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'

Modification history

2024-05-23 09:04

Mathlib/Condensed/Explicit.lean

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

Deleted Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'View on Github →

2023-12-05 08:35

Mathlib/Condensed/Explicit.lean

feat(Condensed): Explicit descriptions of condensed sets (#6731) …

Added Profinite.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition'View on Github →