Basic

📁 Source: Mathlib/Condensed/Basic.lean

Statistics

Metric	Count
Definitions Condensed, CondensedSet, instCategoryCondensed	3
Theorems comp_val, hom_ext, hom_ext_iff, id_val, hom_naturality_apply	5
Total	8

Condensed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_val 📖	mathematical	—	CategoryTheory.Sheaf.Hom.val CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.CategoryStruct.comp Condensed CategoryTheory.Category.toCategoryStruct instCategoryCondensed CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf.val	—	—
hom_ext 📖	—	CategoryTheory.NatTrans.app Opposite CompHaus CategoryTheory.Category.opposite CompHausLike.category CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Sheaf.Hom.val	—	—	CategoryTheory.Sheaf.hom_ext CategoryTheory.NatTrans.ext'
hom_ext_iff 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CompHaus CategoryTheory.Category.opposite CompHausLike.category CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Sheaf.Hom.val	—	hom_ext
id_val 📖	mathematical	—	CategoryTheory.Sheaf.Hom.val CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.CategoryStruct.id Condensed CategoryTheory.Category.toCategoryStruct instCategoryCondensed CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf.val	—	—

CondensedSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_naturality_apply 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CompHaus CategoryTheory.Category.opposite CompHausLike.category CategoryTheory.types CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality_apply

(root)

Definitions

Name	Category	Theorems
Condensed 📖	CompOp	25 math math: Condensed.hasExactColimitsOfShape, CondensedMod.isDiscrete_tfae, Condensed.discrete_map, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, Condensed.epi_iff_surjective_on_stonean, instFullCompHausCondensedTypeCompHausToCondensed', instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, Condensed.comp_val, Condensed.hasExactLimitsOfShape, instFaithfulCondensedTypeCondensedSetUlift, Condensed.epi_iff_locallySurjective_on_compHaus, instHasLimitsOfShapeCondensed, CondensedSet.isDiscrete_tfae, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, instFaithfulCompHausCondensedTypeCompHausToCondensed', CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, instHasFiniteLimitsCondensed, Condensed.underlying_obj, Condensed.underlying_map, Condensed.id_val, Condensed.discrete_obj, instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology, instFullCondensedTypeCondensedSetUlift
CondensedSet 📖	CompOp	22 math math: condensedSetToTopCat_obj_carrier, CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone, CondensedSet.instEpiTopCatAppCounitTopCatAdjunction, CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction, instIsRegularEpiCategoryCondensedSet, instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed, CondensedMod.isDiscrete_iff_isDiscrete_forget, instFullCompHausCondensedSetCompHausToCondensed, CondensedSet.epi_iff_surjective_on_stonean, CondensedSet.instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat, instHasLimitsCondensedSet, instFaithfulCondensedTypeCondensedSetUlift, CondensedSet.LocallyConstant.instFaithfulFunctor, CondensedSet.isDiscrete_tfae, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, instHasLimitsOfSizeCondensedSet, instFaithfulCompHausCondensedSetCompHausToCondensed, condensedSetToTopCat_map, CondensedSet.epi_iff_locallySurjective_on_compHaus, CondensedSet.LocallyConstant.instFullFunctor, CondensedSet.instFaithfulTopCatTopCatToCondensedSet, instFullCondensedTypeCondensedSetUlift
instCategoryCondensed 📖	CompOp	55 math math: Condensed.instAB4StarCondensedMod, condensedSetToTopCat_obj_carrier, CondensedMod.IsSolid.isIso_solidification_map, CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone, Condensed.instAB5CondensedMod, Condensed.hasExactColimitsOfShape, CondensedMod.isDiscrete_tfae, CondensedSet.instEpiTopCatAppCounitTopCatAdjunction, CondensedMod.LocallyConstant.instFullModuleCatFunctor, Condensed.discrete_map, CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, Condensed.epi_iff_surjective_on_stonean, instIsRegularEpiCategoryCondensedSet, instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed, instFullCompHausCondensedTypeCompHausToCondensed', instHasFiniteColimitsCondensedOfHasWeakSheafifyCompHausCoherentTopology, CondensedMod.isDiscrete_iff_isDiscrete_forget, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, instFullCompHausCondensedSetCompHausToCondensed, CondensedMod.epi_iff_surjective_on_stonean, CondensedSet.epi_iff_surjective_on_stonean, instHasLimitsCondensedMod, CondensedSet.instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat, instHasLimitsCondensedSet, Condensed.comp_val, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, Condensed.hasExactLimitsOfShape, instFaithfulCondensedTypeCondensedSetUlift, Condensed.epi_iff_locallySurjective_on_compHaus, CondensedSet.LocallyConstant.instFaithfulFunctor, instHasLimitsOfShapeCondensed, instHasLimitsOfSizeCondensedMod, CondensedSet.isDiscrete_tfae, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, instFaithfulCompHausCondensedTypeCompHausToCondensed', CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, instHasLimitsOfSizeCondensedSet, CondensedMod.epi_iff_locallySurjective_on_compHaus, instHasColimitsCondensedMod, instFaithfulCompHausCondensedSetCompHausToCondensed, CondensedMod.LocallyConstant.instFaithfulModuleCatFunctor, instHasFiniteLimitsCondensed, condensedSetToTopCat_map, Condensed.underlying_obj, Condensed.underlying_map, CondensedSet.epi_iff_locallySurjective_on_compHaus, CondensedSet.LocallyConstant.instFullFunctor, Condensed.id_val, Condensed.instAB4CondensedMod, CondensedSet.instFaithfulTopCatTopCatToCondensedSet, Condensed.discrete_obj, instHasColimitsOfShapeCondensedOfHasWeakSheafifyCompHausCoherentTopology, instFullCondensedTypeCondensedSetUlift

---

← Back to Index