Commit 2024-06-07 13:10 8f1a3577

View on Github →

feat(Condensed): functor from light profinite sets to light condensed sets (#13502)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

added def CategoryTheory.Sheaf.Subcanonical.yoneda

added def CategoryTheory.Sheaf.Subcanonical.yonedaCompSheafToPresheaf

added def CategoryTheory.Sheaf.Subcanonical.yonedaFullyFaithful

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

Modified Mathlib/Condensed/Functors.lean

modified def compHausToCondensed'

Created Mathlib/Condensed/Light/Functors.lean

added def lightProfiniteToLightCondSet