Left

📁 Source: Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean

Statistics

Metric	Count
Definitions constructLeftAdjoint, constructLeftAdjointEquiv, constructLeftAdjointObj, counitCoequalises, otherMap	5
Theorems constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_symm_apply, instIsReflexivePairMapAppCounitOtherMap, isRightAdjoint_square_lift, isRightAdjoint_square_lift_monadic, isRightAdjoint_triangle_lift, isRightAdjoint_triangle_lift_monadic	7
Total	12

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRightAdjoint_square_lift 📖	mathematical	—	Functor.IsRightAdjoint	—	Adjunction.isRightAdjoint Functor.isRightAdjoint_comp isRightAdjoint_triangle_lift
isRightAdjoint_square_lift_monadic 📖	mathematical	—	Functor.IsRightAdjoint	—	Adjunction.isRightAdjoint Functor.isRightAdjoint_comp isRightAdjoint_triangle_lift_monadic
isRightAdjoint_triangle_lift 📖	mathematical	—	Functor.IsRightAdjoint	—	—
isRightAdjoint_triangle_lift_monadic 📖	mathematical	—	Functor.IsRightAdjoint	—	instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison Functor.isRightAdjoint_comp Adjunction.isRightAdjoint Functor.map_id Category.id_comp Monad.adj_counit Monad.FreeCoequalizer.condition isRightAdjoint_triangle_lift Functor.isRightAdjoint_of_isEquivalence Functor.isEquivalence_inv

CategoryTheory.LiftLeftAdjoint

Definitions

Name	Category	Theorems
constructLeftAdjoint 📖	CompOp	—
constructLeftAdjointEquiv 📖	CompOp	2 math math: constructLeftAdjointEquiv_symm_apply, constructLeftAdjointEquiv_apply
constructLeftAdjointObj 📖	CompOp	2 math math: constructLeftAdjointEquiv_symm_apply, constructLeftAdjointEquiv_apply
counitCoequalises 📖	CompOp	2 math math: constructLeftAdjointEquiv_symm_apply, constructLeftAdjointEquiv_apply
otherMap 📖	CompOp	3 math math: constructLeftAdjointEquiv_symm_apply, constructLeftAdjointEquiv_apply, instIsReflexivePairMapAppCounitOtherMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
constructLeftAdjointEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct constructLeftAdjointObj CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike constructLeftAdjointEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit Equiv.symm CategoryTheory.Limits.Cofork.IsColimit.homIso CategoryTheory.Limits.Cofork.ofπ counitCoequalises CategoryTheory.Adjunction.homEquiv otherMap CategoryTheory.Limits.colimit.cocone CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.colimit.isColimit	—	—
constructLeftAdjointEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj constructLeftAdjointObj EquivLike.toFunLike Equiv.instEquivLike Equiv.symm constructLeftAdjointEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit otherMap CategoryTheory.Limits.Cofork.IsColimit.homIso CategoryTheory.Limits.colimit.cocone CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.colimit.isColimit CategoryTheory.Adjunction.homEquiv CategoryTheory.Limits.Cofork.ofπ counitCoequalises	—	—
instIsReflexivePairMapAppCounitOtherMap 📖	mathematical	—	CategoryTheory.IsReflexivePair CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit otherMap	—	CategoryTheory.IsReflexivePair.mk' CategoryTheory.Functor.map_comp CategoryTheory.Adjunction.right_triangle_components CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp_assoc CategoryTheory.Adjunction.unit_naturality_assoc CategoryTheory.Category.comp_id CategoryTheory.Adjunction.left_triangle_components

---

← Back to Index