Commit 2024-07-16 01:36 58023b55

View on Github →

feat:(Condensed): the functor from TopCat to CondensedSet is a faithful right adjoint. (#14455) Also adds some lemmas which improve automation in condensed mathematics.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Condensed/Basic.lean

added theorem Condensed.comp_val

added theorem Condensed.hom_ext

added theorem Condensed.id_val

added theorem CondensedSet.hom_naturality_apply

Modified Mathlib/Condensed/Module.lean

added theorem CondensedMod.hom_naturality_apply

Created Mathlib/Condensed/TopCatAdjunction.lean

added def CondensedSet.toTopCat

added def CondensedSet.toTopCatMap

added def CondensedSet.topCatAdjunctionCounit

added def CondensedSet.topCatAdjunctionCounitEquiv

added theorem CondensedSet.topCatAdjunctionCounit_bijective

added def CondensedSet.topCatAdjunctionUnit

added def condensedSetToTopCat

Modified Mathlib/Condensed/TopComparison.lean