Adjunctions

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

Statistics

Metric	Count
Definitions adj₁, adj₂	2
Theorems adj₁_counit, adj₁_unit, adj₂_counit, adj₂_unit, instIsLeftAdjointForgetContinuousMapCarrier, instIsRightAdjointForgetContinuousMapCarrier	6
Total	8

TopCat

Definitions

Name	Category	Theorems
adj₁ 📖	CompOp	2 math math: adj₁_unit, adj₁_counit
adj₂ 📖	CompOp	2 math math: adj₂_counit, adj₂_unit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adj₁_counit 📖	mathematical	—	CategoryTheory.Adjunction.counit CategoryTheory.types TopCat instCategory discrete CategoryTheory.forget ContinuousMap carrier str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier adj₁ CategoryTheory.Functor.comp CategoryTheory.Functor.id ofHom CategoryTheory.Functor.obj	—	—
adj₁_unit 📖	mathematical	—	CategoryTheory.Adjunction.unit CategoryTheory.types TopCat instCategory discrete CategoryTheory.forget ContinuousMap carrier str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier adj₁ CategoryTheory.Functor.id CategoryTheory.Functor.comp	—	—
adj₂_counit 📖	mathematical	—	CategoryTheory.Adjunction.counit TopCat instCategory CategoryTheory.types CategoryTheory.forget ContinuousMap carrier str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier trivial adj₂ CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.obj	—	—
adj₂_unit 📖	mathematical	—	CategoryTheory.Adjunction.unit TopCat instCategory CategoryTheory.types CategoryTheory.forget ContinuousMap carrier str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier trivial adj₂ CategoryTheory.Functor.id CategoryTheory.Functor.comp ofHom CategoryTheory.Functor.obj	—	—
instIsLeftAdjointForgetContinuousMapCarrier 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint TopCat instCategory CategoryTheory.types CategoryTheory.forget ContinuousMap carrier str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	—	—
instIsRightAdjointForgetContinuousMapCarrier 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.types TopCat instCategory CategoryTheory.forget ContinuousMap carrier str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	—	—

---

← Back to Index