Structures · Category theory
CategoryTheory.MonadicRightAdjoint
A right adjoint functor R : D ⥤ C is monadic if the comparison functor Monad.comparison R
from D to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.
- Defined in
- Mathlib.CategoryTheory.Monad.Adjunction
- Shape
- One type argument · adds L, adj, eqv
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- CategoryTheory.monadicAdjunction
- CategoryTheory.monadicLeftAdjoint
- CategoryTheory.isRightAdjoint_triangle_lift_monadic
- CategoryTheory.instIsRightAdjointOfMonadicRightAdjoint
- CategoryTheory.monadicCreatesColimitOfPreservesColimit
- CategoryTheory.MonadicRightAdjoint.eqv
- CategoryTheory.comp_comparison_forget_hasLimit
- CategoryTheory.comp_comparison_hasLimit
- CategoryTheory.monadicCreatesLimits
- CategoryTheory.isRightAdjoint_square_lift_monadic
- CategoryTheory.MonadicRightAdjoint.L
- CategoryTheory.MonadicRightAdjoint.adj
- CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison
- CategoryTheory.monadicCreatesColimitsOfShapeOfPreservesColimitsOfShape
- CategoryTheory.Monad.createsGSplitCoequalizersOfMonadic
- CategoryTheory.monadicCreatesColimitsOfPreservesColimits
Ancestors0
No ancestors.