Commit 2024-07-19 14:02 5768a1b3

View on Github →

feat(LightCondensed): the functor from TopCat to LightCondSet is a faithful right adjoint (#14506)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Condensed/Light/Basic.lean

added theorem LightCondSet.hom_naturality_apply

added theorem LightCondensed.comp_val

added theorem LightCondensed.hom_ext

added theorem LightCondensed.id_val

Modified Mathlib/Condensed/Light/Module.lean

added theorem LightCondMod.hom_naturality_apply

Created Mathlib/Condensed/Light/TopCatAdjunction.lean

added def LightCondSet.toTopCat

added def LightCondSet.toTopCatMap

added def LightCondSet.topCatAdjunctionCounit

added def LightCondSet.topCatAdjunctionCounitEquiv

added theorem LightCondSet.topCatAdjunctionCounit_bijective

added def LightCondSet.topCatAdjunctionUnit

added def lightCondSetToTopCat

Modified Mathlib/Condensed/Light/TopComparison.lean