Commit 2024-10-16 04:43 66d4c59d

View on Github →

feat(Condensed): colimit characterization of discrete condensed sets (#15566) This PR provides the necessary API to prove that a condensed set X is discrete if and only if for every profinite set S = limᵢSᵢ, X(S) ≅ colimᵢX(Sᵢ), and the analogous result for light condensed sets.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Condensed/Discrete/Colimit.lean

added def Condensed.finYoneda

added def Condensed.fintypeCatAsCofan

added def Condensed.fintypeCatAsCofanIsColimit

added theorem Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply

added theorem Condensed.isColimitLocallyConstantPresheaf_desc_apply

added def Condensed.isoFinYoneda

added def Condensed.isoFinYonedaComponents

added theorem Condensed.isoFinYonedaComponents_hom_apply

added theorem Condensed.isoFinYonedaComponents_inv_comp

added def Condensed.isoLocallyConstantOfIsColimit

added theorem Condensed.isoLocallyConstantOfIsColimit_inv

added def Condensed.lanCondensedSet

added def Condensed.lanPresheafExt

added theorem Condensed.lanPresheafExt_hom

added theorem Condensed.lanPresheafExt_inv

added def Condensed.lanPresheafIso

added theorem Condensed.lanPresheafIso_hom

added def Condensed.lanPresheafNatIso

added theorem Condensed.lanPresheafNatIso_hom_app

added def Condensed.lanSheafProfinite

added def Condensed.locallyConstantIsoFinYoneda

added def LightCondensed.finYoneda

added def LightCondensed.fintypeCatAsCofan

added def LightCondensed.fintypeCatAsCofanIsColimit

added theorem LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply

added theorem LightCondensed.isColimitLocallyConstantPresheaf_desc_apply

added def LightCondensed.isoFinYoneda

added def LightCondensed.isoFinYonedaComponents

added theorem LightCondensed.isoFinYonedaComponents_hom_apply

added theorem LightCondensed.isoFinYonedaComponents_inv_comp

added def LightCondensed.isoLocallyConstantOfIsColimit

added theorem LightCondensed.isoLocallyConstantOfIsColimit_inv

added def LightCondensed.lanLightCondSet

added def LightCondensed.lanPresheafExt

added theorem LightCondensed.lanPresheafExt_hom

added theorem LightCondensed.lanPresheafExt_inv

added def LightCondensed.lanPresheafIso

added theorem LightCondensed.lanPresheafIso_hom

added def LightCondensed.lanPresheafNatIso

added theorem LightCondensed.lanPresheafNatIso_hom_app

added def LightCondensed.locallyConstantIsoFinYoneda