Solid

📁 Source: Mathlib/Condensed/Solid.lean

Statistics

Metric	Count
Definitions finFree, profiniteFree, profiniteSolid, profiniteSolidCounit, profiniteSolidIsPointwiseRightKanExtension, profiniteSolidification, IsSolid	7
Theorems instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, isIso_solidification_map	2
Total	9

Condensed

Definitions

Name	Category	Theorems
finFree 📖	CompOp	1 math math: instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit
profiniteFree 📖	CompOp	1 math math: CondensedMod.IsSolid.isIso_solidification_map
profiniteSolid 📖	CompOp	2 math math: CondensedMod.IsSolid.isIso_solidification_map, instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit
profiniteSolidCounit 📖	CompOp	1 math math: instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit
profiniteSolidIsPointwiseRightKanExtension 📖	CompOp	—
profiniteSolidification 📖	CompOp	1 math math: CondensedMod.IsSolid.isIso_solidification_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit 📖	mathematical	—	CategoryTheory.Functor.IsRightKanExtension FintypeCat CondensedMod Profinite FintypeCat.instCategory instCategoryCondensed ModuleCat ModuleCat.moduleCategory CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str profiniteSolid FintypeCat.toProfinite finFree profiniteSolidCounit	—	CategoryTheory.Functor.instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit

CondensedMod

Definitions

Name	Category	Theorems
IsSolid 📖	CompData	—

CondensedMod.IsSolid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_solidification_map 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.types CategoryTheory.Functor.obj Opposite CondensedMod CategoryTheory.Category.opposite instCategoryCondensed ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Opposite.op Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str Condensed.profiniteSolid Condensed.profiniteFree CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app Condensed.profiniteSolidification	—	—

---

← Back to Index