Theorems · Definition · category theory
CategoryTheory.Monad.algebraFunctorOfMonadHom
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{T₁ T₂ : CategoryTheory.Monad C} → (T₂ ⟶ T₁) → CategoryTheory.Functor T₁.Algebra T₂.AlgebraGiven a monad morphism from T₂ to T₁, we get a functor from the algebras of T₁ to algebras of
T₂.
- Defined in
- Mathlib.CategoryTheory.Monad.Algebra
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.NatTrans.appproof · cited by 7,406
- CategoryTheory.Monadstatement and proof · cited by 153
- CategoryTheory.Monad.Algebrastatement and proof · cited by 110
- CategoryTheory.Monad.Algebra.Aproof · cited by 81
- CategoryTheory.Monad.Algebra.Hom.fproof · cited by 48
- CategoryTheory.Monad.Algebra.aproof · cited by 45
- CategoryTheory.MonadHom.toNatTransproof · cited by 21
Cited by19
Results whose statement or proof uses this declaration.
- CategoryTheory.Monad.algebraFunctorOfMonadHomEqstatement and proof · cited by 5
- CategoryTheory.Monad.algebraEquivOfIsoMonadsproof · cited by 4
- CategoryTheory.Monad.algebraFunctorOfMonadHomCompstatement and proof · cited by 4
- CategoryTheory.Monad.algebraFunctorOfMonadHomIdstatement and proof · cited by 4
- CategoryTheory.Monad.algebraFunctorOfMonadHomEq.congr_simpstatement · cited by 0
- CategoryTheory.Monad.algebraEquivOfIsoMonads_counitIsostatement · cited by 0
- CategoryTheory.Monad.algebraEquivOfIsoMonads_functorstatement · cited by 0
- CategoryTheory.Monad.algebraEquivOfIsoMonads_inversestatement · cited by 0
- CategoryTheory.Monad.algebraEquivOfIsoMonads_unitIsostatement · cited by 0
- CategoryTheory.Monad.algebraFunctorOfMonadHomComp_hom_app_fstatement · cited by 0
- CategoryTheory.Monad.algebraFunctorOfMonadHomComp_inv_app_fstatement · cited by 0
- CategoryTheory.Monad.algebraFunctorOfMonadHomEq_hom_app_fstatement · cited by 0