Adjunctions

📁 Source: Mathlib/Topology/Category/Stonean/Adjunctions.lean

Statistics

Metric	Count
Definitions stoneCechAdjunction, stoneCechEquivalence, stoneCechObj, typeToStonean	4
Theorems preservesLimits	1
Total	5

Stonean

Definitions

Name	Category	Theorems
stoneCechAdjunction 📖	CompOp	—
stoneCechEquivalence 📖	CompOp	—
stoneCechObj 📖	CompOp	—

Stonean.forget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits Stonean CompHausLike.category ExtremallyDisconnected TopCat.carrier TopCat.str CategoryTheory.types CategoryTheory.forget ContinuousMap CompHausLike.toTop ContinuousMap.instFunLike CompHausLike.concreteCategory	—	CategoryTheory.Adjunction.rightAdjoint_preservesLimits

(root)

Definitions

Name	Category	Theorems
typeToStonean 📖	CompOp	—

---

← Back to Index