Loogle!

Result

Found 183 declarations mentioning CategoryTheory.Monad.Algebra.

• CategoryTheory.Monad.Algebra 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : Type (max u₁ v₁)
• CategoryTheory.Monad.Algebra.A 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) : C
• CategoryTheory.Monad.Algebra.eilenbergMoore 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} : CategoryTheory.Category.{v₁, max u₁ v₁} T.Algebra
• CategoryTheory.Monad.Algebra.instCategoryStruct 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} : CategoryTheory.CategoryStruct.{v₁, max u₁ v₁} T.Algebra
• CategoryTheory.Monad.instInhabitedAlgebra 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) [Inhabited C] : Inhabited T.Algebra
• CategoryTheory.Monad.Algebra.Hom 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A B : T.Algebra) : Type v₁
• CategoryTheory.Monad.Algebra.Hom.id 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : T.Algebra) : A.Hom A
• CategoryTheory.Monad.forget 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor T.Algebra C
• CategoryTheory.Monad.free 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor C T.Algebra
• CategoryTheory.Monad.Algebra.Hom.instInhabited 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : T.Algebra) : Inhabited (A.Hom A)
• CategoryTheory.Monad.forget_faithful 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.forget.Faithful
• CategoryTheory.Monad.forget_reflects_iso 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.forget.ReflectsIsomorphisms
• CategoryTheory.Monad.instIsRightAdjointAlgebraForget 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.forget.IsRightAdjoint
• CategoryTheory.Monad.adj 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.free ⊣ T.forget
• CategoryTheory.Monad.Algebra.id_eq_id 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : T.Algebra) : CategoryTheory.Monad.Algebra.Hom.id A = CategoryTheory.CategoryStruct.id A
• CategoryTheory.Monad.forget_obj 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (A : T.Algebra) : T.forget.obj A = A.A
• CategoryTheory.Monad.algebraEquivOfIsoMonads 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : T₁.Algebra ≌ T₂.Algebra
• CategoryTheory.Monad.algebraFunctorOfMonadHom 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁) : CategoryTheory.Functor T₁.Algebra T₂.Algebra
• CategoryTheory.Monad.Algebra.a 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) : T.obj self.A ⟶ self.A
• CategoryTheory.Monad.Algebra.Hom.comp 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {P Q R : T.Algebra} (f : P.Hom Q) (g : Q.Hom R) : P.Hom R
• CategoryTheory.Monad.Algebra.Hom.f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra} (self : A.Hom B) : A.A ⟶ B.A
• CategoryTheory.Monad.free_obj_A 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : (T.free.obj X).A = T.obj X
• CategoryTheory.Monad.Algebra.id_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : T.Algebra) : (CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.A
• CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_A 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁) (A : T₁.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).A = A.A
• CategoryTheory.Monad.algebra_epi_of_epi 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X Y : T.Algebra} (f : X ⟶ Y) [h : CategoryTheory.Epi f.f] : CategoryTheory.Epi f
• CategoryTheory.Monad.algebra_iso_of_iso 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {A B : T.Algebra} (f : A ⟶ B) [CategoryTheory.IsIso f.f] : CategoryTheory.IsIso f
• CategoryTheory.Monad.algebra_mono_of_mono 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X Y : T.Algebra} (f : X ⟶ Y) [h : CategoryTheory.Mono f.f] : CategoryTheory.Mono f
• CategoryTheory.Monad.algebra_equiv_of_iso_monads_comp_forget 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ⟶ T₂) : (CategoryTheory.Monad.algebraFunctorOfMonadHom h).comp T₁.forget = T₂.forget
• CategoryTheory.Monad.algebraFunctorOfMonadHomId 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} : CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁) ≅ CategoryTheory.Functor.id T₁.Algebra
• CategoryTheory.Monad.Algebra.Hom.ext 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : T.Algebra} {x y : A.Hom B} (f : x.f = y.f) : x = y
• CategoryTheory.Monad.Algebra.Hom.ext_iff 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : T.Algebra} {x y : A.Hom B} : x = y ↔ x.f = y.f
• CategoryTheory.Monad.algebraEquivOfIsoMonads_functor 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : (CategoryTheory.Monad.algebraEquivOfIsoMonads h).functor = CategoryTheory.Monad.algebraFunctorOfMonadHom h.inv
• CategoryTheory.Monad.algebraEquivOfIsoMonads_inverse 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : (CategoryTheory.Monad.algebraEquivOfIsoMonads h).inverse = CategoryTheory.Monad.algebraFunctorOfMonadHom h.hom
• CategoryTheory.Monad.forget_map 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X✝ Y✝ : T.Algebra} (f : X✝ ⟶ Y✝) : T.forget.map f = f.f
• CategoryTheory.Monad.Algebra.comp_eq_comp 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A A' A'' : T.Algebra} (f : A ⟶ A') (g : A' ⟶ A'') : CategoryTheory.Monad.Algebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
• CategoryTheory.Monad.algebraFunctorOfMonadHomEq 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f g : T₁ ⟶ T₂} (h : f = g) : CategoryTheory.Monad.algebraFunctorOfMonadHom f ≅ CategoryTheory.Monad.algebraFunctorOfMonadHom g
• CategoryTheory.Monad.free_obj_a 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : (T.free.obj X).a = T.μ.app X
• CategoryTheory.Monad.Algebra.Hom.ext' 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X Y : T.Algebra) (f g : X ⟶ Y) (h : f.f = g.f) : f = g
• CategoryTheory.Monad.Algebra.Hom.ext'_iff 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {X Y : T.Algebra} {f g : X ⟶ Y} : f = g ↔ f.f = g.f
• CategoryTheory.Monad.Algebra.unit 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) : CategoryTheory.CategoryStruct.comp (T.η.app self.A) self.a = CategoryTheory.CategoryStruct.id self.A
• CategoryTheory.Monad.Algebra.unit_assoc 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) {Z : C} (h : self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.η.app self.A) (CategoryTheory.CategoryStruct.comp self.a h) = h
• CategoryTheory.Monad.Algebra.comp_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A A' A'' : T.Algebra} (f : A ⟶ A') (g : A' ⟶ A'') : (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
• CategoryTheory.Monad.algebraFunctorOfMonadHomComp 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) : CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g) ≅ (CategoryTheory.Monad.algebraFunctorOfMonadHom g).comp (CategoryTheory.Monad.algebraFunctorOfMonadHom f)
• CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_a 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁) (A : T₁.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).a = CategoryTheory.CategoryStruct.comp (h.app A.A) A.a
• CategoryTheory.Monad.Algebra.Hom.h 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra} (self : A.Hom B) : CategoryTheory.CategoryStruct.comp (T.map self.f) B.a = CategoryTheory.CategoryStruct.comp A.a self.f
• CategoryTheory.Monad.Algebra.Hom.mk 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra} (f : A.A ⟶ B.A) (h : CategoryTheory.CategoryStruct.comp (T.map f) B.a = CategoryTheory.CategoryStruct.comp A.a f := by cat_disch) : A.Hom B
• CategoryTheory.Monad.free_map_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (T.free.map f).f = T.map f
• CategoryTheory.Monad.Algebra.isoMk 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra} (h : A.A ≅ B.A) (w : CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom := by cat_disch) : A ≅ B
• CategoryTheory.Monad.Algebra.Hom.h_assoc 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra} (self : A.Hom B) {Z : C} (h : B.A ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.map self.f) (CategoryTheory.CategoryStruct.comp B.a h) = CategoryTheory.CategoryStruct.comp A.a (CategoryTheory.CategoryStruct.comp self.f h)
• CategoryTheory.Monad.Algebra.assoc 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) : CategoryTheory.CategoryStruct.comp (T.μ.app self.A) self.a = CategoryTheory.CategoryStruct.comp (T.map self.a) self.a
• CategoryTheory.Monad.Algebra.isoMk_hom_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra} (h : A.A ≅ B.A) (w : CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom := by cat_disch) : (CategoryTheory.Monad.Algebra.isoMk h w).hom.f = h.hom
• CategoryTheory.Monad.Algebra.isoMk_inv_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra} (h : A.A ≅ B.A) (w : CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom := by cat_disch) : (CategoryTheory.Monad.Algebra.isoMk h w).inv.f = h.inv
• CategoryTheory.Monad.Algebra.mk 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : C) (a : T.obj A ⟶ A) (unit : CategoryTheory.CategoryStruct.comp (T.η.app A) a = CategoryTheory.CategoryStruct.id A := by cat_disch) (assoc : CategoryTheory.CategoryStruct.comp (T.μ.app A) a = CategoryTheory.CategoryStruct.comp (T.map a) a := by cat_disch) : T.Algebra
• CategoryTheory.Monad.Algebra.assoc_assoc 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) {Z : C} (h : self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.μ.app self.A) (CategoryTheory.CategoryStruct.comp self.a h) = CategoryTheory.CategoryStruct.comp (T.map self.a) (CategoryTheory.CategoryStruct.comp self.a h)
• CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁) {X✝ Y✝ : T₁.Algebra} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).map f).f = f.f
• CategoryTheory.Monad.algebraFunctorOfMonadHomEq_hom_app_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f g : T₁ ⟶ T₂} (h : f = g) (X : T₂.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).hom
• CategoryTheory.Monad.algebraFunctorOfMonadHomEq_inv_app_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f g : T₁ ⟶ T₂} (h : f = g) (X : T₂.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).inv
• CategoryTheory.Monad.algebraFunctorOfMonadHomId_hom_app_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : T₁.Algebra) : (CategoryTheory.Monad.algebraFunctorOfMonadHomId.hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).hom
• CategoryTheory.Monad.algebraFunctorOfMonadHomId_inv_app_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : T₁.Algebra) : (CategoryTheory.Monad.algebraFunctorOfMonadHomId.inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).inv
• CategoryTheory.Monad.algebraEquivOfIsoMonads_unitIso 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : (CategoryTheory.Monad.algebraEquivOfIsoMonads h).unitIso = CategoryTheory.Monad.algebraFunctorOfMonadHomId.symm ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomEq ⋯ ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomComp h.hom h.inv
• CategoryTheory.Monad.algebraFunctorOfMonadHomComp_hom_app_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) (X : T₃.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomComp f g).hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g)).obj X).A).hom
• CategoryTheory.Monad.algebraFunctorOfMonadHomComp_inv_app_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) (X : T₃.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomComp f g).inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g)).obj X).A).inv
• CategoryTheory.Monad.algebraEquivOfIsoMonads_counitIso 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : (CategoryTheory.Monad.algebraEquivOfIsoMonads h).counitIso = (CategoryTheory.Monad.algebraFunctorOfMonadHomComp h.inv h.hom).symm ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomEq ⋯ ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomId
• CategoryTheory.Monad.adj_unit 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.adj.unit = { app := fun X => T.η.app X, naturality := ⋯ }
• CategoryTheory.Monad.adj_counit 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.adj.counit = { app := fun Y => { f := Y.a, h := ⋯ }, naturality := ⋯ }
• CategoryTheory.algebraEquivUnder 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.coprodMonad X).Algebra ≌ CategoryTheory.Under X
• CategoryTheory.algebraToUnder 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor (CategoryTheory.coprodMonad X).Algebra (CategoryTheory.Under X)
• CategoryTheory.underToAlgebra 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.coprodMonad X).Algebra
• CategoryTheory.underToAlgebra_obj_A 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) : ((CategoryTheory.underToAlgebra X).obj f).A = f.right
• CategoryTheory.algebraEquivUnder_functor 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).functor = CategoryTheory.algebraToUnder X
• CategoryTheory.algebraEquivUnder_inverse 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).inverse = CategoryTheory.underToAlgebra X
• CategoryTheory.underToAlgebra_obj_a 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (f : CategoryTheory.Under X) : ((CategoryTheory.underToAlgebra X).obj f).a = CategoryTheory.Limits.coprod.desc f.hom (CategoryTheory.CategoryStruct.id f.right)
• CategoryTheory.algebraToUnder_obj 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (A : (CategoryTheory.coprodMonad X).Algebra) : (CategoryTheory.algebraToUnder X).obj A = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)
• CategoryTheory.underToAlgebra_map_f 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {X✝ Y✝ : CategoryTheory.Under X} (g : X✝ ⟶ Y✝) : ((CategoryTheory.underToAlgebra X).map g).f = CategoryTheory.Under.Hom.right g
• CategoryTheory.algebraEquivUnder_counitIso 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).counitIso = CategoryTheory.NatIso.ofComponents (fun f => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl (((CategoryTheory.underToAlgebra X).comp (CategoryTheory.algebraToUnder X)).obj f).right) ⋯) ⋯
• CategoryTheory.algebraToUnder_map 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] {X✝ Y✝ : (CategoryTheory.coprodMonad X).Algebra} (f : X✝ ⟶ Y✝) : (CategoryTheory.algebraToUnder X).map f = CategoryTheory.Under.homMk f.f ⋯
• CategoryTheory.algebraEquivUnder_unitIso 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.algebraEquivUnder X).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Monad.Algebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.coprodMonad X).Algebra).obj A).A) ⋯) ⋯
• CategoryTheory.Under.costar_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] (X✝ : C) : ((CategoryTheory.Under.costar X).obj X✝).hom = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ X✝)))
• CategoryTheory.instMonadicRightAdjointAlgebraForget 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.MonadicRightAdjoint T.forget
• CategoryTheory.Adjunction.adjToMonadIso 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.adj.toMonad ≅ T
• CategoryTheory.Monad.comparison 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.Functor D h.toMonad.Algebra
• CategoryTheory.instFaithfulAlgebraToMonadComparison 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} [R.Faithful] (h : L ⊣ R) : (CategoryTheory.Monad.comparison h).Faithful
• CategoryTheory.MonadicRightAdjoint.mk 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} (L : CategoryTheory.Functor C D) (adj : L ⊣ R) (eqv : (CategoryTheory.Monad.comparison adj).IsEquivalence) : CategoryTheory.MonadicRightAdjoint R
• CategoryTheory.Reflective.comparison_full 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [R.Full] {L : CategoryTheory.Functor C D} (adj : L ⊣ R) : (CategoryTheory.Monad.comparison adj).Full
• CategoryTheory.Monad.comparison_obj_A 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D) : ((CategoryTheory.Monad.comparison h).obj X).A = R.obj X
• CategoryTheory.Monad.comparisonForget 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : (CategoryTheory.Monad.comparison h).comp h.toMonad.forget ≅ R
• CategoryTheory.instIsEquivalenceAlgebraToMonadMonadicAdjunctionComparison 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] : (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R)).IsEquivalence
• CategoryTheory.MonadicRightAdjoint.eqv 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {R : CategoryTheory.Functor D C} [self : CategoryTheory.MonadicRightAdjoint R] : (CategoryTheory.Monad.comparison CategoryTheory.MonadicRightAdjoint.adj).IsEquivalence
• CategoryTheory.Reflective.comparison_essSurj 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] : (CategoryTheory.Monad.comparison (CategoryTheory.reflectorAdjunction R)).EssSurj
• CategoryTheory.instEssSurjAlgebraToMonadAdjComparison 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : (CategoryTheory.Monad.comparison T.adj).EssSurj
• CategoryTheory.instFullAlgebraToMonadAdjComparison 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : (CategoryTheory.Monad.comparison T.adj).Full
• CategoryTheory.Monad.left_comparison 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : L.comp (CategoryTheory.Monad.comparison h) = h.toMonad.free
• CategoryTheory.Monad.comparison_obj_a 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (X : D) : ((CategoryTheory.Monad.comparison h).obj X).a = R.map (h.counit.app X)
• CategoryTheory.Adjunction.adjToMonadIso_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : (CategoryTheory.Adjunction.adjToMonadIso T).hom.app X = CategoryTheory.CategoryStruct.id (T.obj X)
• CategoryTheory.Adjunction.adjToMonadIso_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : (CategoryTheory.Adjunction.adjToMonadIso T).inv.app X = CategoryTheory.CategoryStruct.id (T.obj X)
• CategoryTheory.Monad.comparisonForget_inv_app 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x✝ : D) : (CategoryTheory.Monad.comparisonForget h).inv.app x✝ = CategoryTheory.CategoryStruct.id (R.obj x✝)
• CategoryTheory.Reflective.instIsIsoAppUnitReflectorAdjunctionA 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor D C} [CategoryTheory.Reflective R] (X : (CategoryTheory.reflectorAdjunction R).toMonad.Algebra) : CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction R).unit.app X.A)
• CategoryTheory.Monad.comparison_map_f 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Monad.comparison h).map f).f = R.map f
• CategoryTheory.Monad.comparisonForget_hom_app 📋 Mathlib.CategoryTheory.Monad.Adjunction
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) (x✝ : D) : (CategoryTheory.Monad.comparisonForget h).hom.app x✝ = CategoryTheory.CategoryStruct.id (((CategoryTheory.Monad.comparison h).comp h.toMonad.forget).obj x✝)
• CategoryTheory.Monad.forgetCreatesLimits 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} : CategoryTheory.CreatesLimitsOfSize.{u_1, u_2, v₁, v₁, max u₁ v₁, u₁} T.forget
• CategoryTheory.Monad.forgetCreatesColimits 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} [CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor] : CategoryTheory.CreatesColimitsOfSize.{v, u, v₁, v₁, max u₁ v₁, u₁} T.forget
• CategoryTheory.Monad.forgetCreatesColimitsOfShape 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor] : CategoryTheory.CreatesColimitsOfShape J T.forget
• CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) [CategoryTheory.Limits.HasLimit (D.comp T.forget)] : CategoryTheory.Limits.HasLimit D
• CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor] (D : CategoryTheory.Functor J T.Algebra) [CategoryTheory.Limits.HasColimit (D.comp T.forget)] : CategoryTheory.Limits.HasColimit D
• CategoryTheory.Monad.ForgetCreatesLimits.newCone 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) : CategoryTheory.Limits.Cone (D.comp T.forget)
• CategoryTheory.Monad.ForgetCreatesLimits.conePoint 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : T.Algebra
• CategoryTheory.Monad.ForgetCreatesColimits.newCocone 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) : CategoryTheory.Limits.Cocone ((D.comp T.forget).comp T.toFunctor)
• CategoryTheory.Monad.ForgetCreatesLimits.liftedCone 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.Cone D
• CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t)
• CategoryTheory.Monad.ForgetCreatesColimits.γ 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} : (D.comp T.forget).comp T.toFunctor ⟶ D.comp T.forget
• CategoryTheory.Monad.ForgetCreatesLimits.γ 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) : D.comp (T.forget.comp T.toFunctor) ⟶ D.comp T.forget
• CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_pt 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).pt = CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t
• CategoryTheory.Monad.ForgetCreatesLimits.conePoint_A 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).A = c.pt
• CategoryTheory.Monad.forgetCreatesColimit 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : CategoryTheory.CreatesColimit D T.forget
• CategoryTheory.Monad.ForgetCreatesColimits.newCocone_pt 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) : (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).pt = c.pt
• CategoryTheory.Monad.ForgetCreatesColimits.coconePoint 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : T.Algebra
• CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : CategoryTheory.Limits.Cocone D
• CategoryTheory.Monad.ForgetCreatesColimits.γ_app 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (j : J) : CategoryTheory.Monad.ForgetCreatesColimits.γ.app j = (D.obj j).a
• CategoryTheory.Monad.ForgetCreatesLimits.γ_app 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (j : J) : (CategoryTheory.Monad.ForgetCreatesLimits.γ D).app j = (D.obj j).a
• CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t)
• CategoryTheory.comp_comparison_hasLimit 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D) (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] [CategoryTheory.Limits.HasLimit (F.comp R)] : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R)))
• CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_pt 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).pt = CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t
• CategoryTheory.Monad.ForgetCreatesLimits.conePoint_a 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).a = t.lift (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c)
• CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_A 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).A = c.pt
• CategoryTheory.comp_comparison_forget_hasLimit 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D) (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] [CategoryTheory.Limits.HasLimit (F.comp R)] : CategoryTheory.Limits.HasLimit ((F.comp (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R))).comp (CategoryTheory.monadicAdjunction R).toMonad.forget)
• CategoryTheory.Monad.ForgetCreatesColimits.lambda 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] : (T.mapCocone c).pt ⟶ c.pt
• CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_a 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).a = CategoryTheory.Monad.ForgetCreatesColimits.lambda c t
• CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone D) : ((CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit D c t).lift s).f = t.lift (T.forget.mapCone s)
• CategoryTheory.Monad.ForgetCreatesColimits.newCocone_ι 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) : (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).ι = CategoryTheory.CategoryStruct.comp CategoryTheory.Monad.ForgetCreatesColimits.γ c.ι
• CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (s : CategoryTheory.Limits.Cocone D) : ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit c t).desc s).f = t.desc (T.forget.mapCocone s)
• CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_π_app_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) (j : J) : ((CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).π.app j).f = c.π.app j
• CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (X : J) : (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c).π.app X = CategoryTheory.CategoryStruct.comp (T.map (c.π.app X)) (D.obj X).a
• CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_ι_app_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (j : J) : ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).ι.app j).f = c.ι.app j
• CategoryTheory.Monad.ForgetCreatesColimits.commuting 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] (j : J) : CategoryTheory.CategoryStruct.comp (T.map (c.ι.app j)) (CategoryTheory.Monad.ForgetCreatesColimits.lambda c t) = CategoryTheory.CategoryStruct.comp (D.obj j).a (c.ι.app j)
• CategoryTheory.Monad.FreeCoequalizer.π 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : T.free.obj X.A ⟶ X
• CategoryTheory.Monad.FreeCoequalizer.π_f 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : (CategoryTheory.Monad.FreeCoequalizer.π X).f = X.a
• CategoryTheory.Monad.FreeCoequalizer.bottomMap 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : T.free.obj (T.obj X.A) ⟶ T.free.obj X.A
• CategoryTheory.Monad.FreeCoequalizer.topMap 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : T.free.obj (T.obj X.A) ⟶ T.free.obj X.A
• CategoryTheory.Monad.beckAlgebraCofork 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : CategoryTheory.Limits.Cofork (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.bottomMap X)
• CategoryTheory.Monad.instIsReflexivePairAlgebraTopMapBottomMap 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : CategoryTheory.IsReflexivePair (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.bottomMap X)
• CategoryTheory.Monad.beckAlgebraCoequalizer 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.beckAlgebraCofork X)
• CategoryTheory.Monad.beckAlgebraCofork_pt 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : (CategoryTheory.Monad.beckAlgebraCofork X).pt = X
• CategoryTheory.Monad.beckCofork 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : CategoryTheory.Limits.Cofork (T.map X.a) (T.μ.app X.A)
• CategoryTheory.Monad.beckCoequalizer 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.beckCofork X)
• CategoryTheory.Monad.beckSplitCoequalizer 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : CategoryTheory.IsSplitCoequalizer (T.map X.a) (T.μ.app X.A) X.a
• CategoryTheory.Monad.beckCofork_pt 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : (CategoryTheory.Monad.beckCofork X).pt = X.A
• CategoryTheory.Monad.FreeCoequalizer.topMap_f 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : (CategoryTheory.Monad.FreeCoequalizer.topMap X).f = T.map X.a
• CategoryTheory.Monad.FreeCoequalizer.bottomMap_f 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : (CategoryTheory.Monad.FreeCoequalizer.bottomMap X).f = T.μ.app X.A
• CategoryTheory.Monad.FreeCoequalizer.condition 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.π X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.bottomMap X) (CategoryTheory.Monad.FreeCoequalizer.π X)
• CategoryTheory.Monad.beckCofork_π 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) : (CategoryTheory.Monad.beckCofork X).π = X.a
• CategoryTheory.Monad.beckAlgebraCofork_ι_app 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) (X✝ : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Monad.beckAlgebraCofork X).ι.app X✝ = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.π X)) (CategoryTheory.Monad.FreeCoequalizer.π X) X✝
• CategoryTheory.Monad.beckCoequalizer_desc 📋 Mathlib.CategoryTheory.Monad.Coequalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) (s : CategoryTheory.Limits.Cofork (T.map X.a) (T.μ.app X.A)) : (CategoryTheory.Monad.beckCoequalizer X).desc s = CategoryTheory.CategoryStruct.comp (T.η.app X.A) s.π
• CategoryTheory.Monad.MonadicityInternal.main_pair_reflexive 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) : CategoryTheory.IsReflexivePair (F.map A.a) (adj.counit.app (F.obj A.A))
• CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : D
• CategoryTheory.Monad.MonadicityInternal.main_pair_G_split 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) : G.IsSplitPair (F.map A.a) (adj.counit.app (F.obj A.A))
• CategoryTheory.Monad.instHasCoequalizerMapAAppCounitObjAOfHasCoequalizerOfIsSplitPair 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] (A : adj.toMonad.Algebra) : CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
• CategoryTheory.Monad.instCreatesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfCreatesColimitOfIsSplitPair 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.CreatesColimitOfIsSplitPair G] (A : adj.toMonad.Algebra) : CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
• CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsReflexivePair 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G] (X : adj.toMonad.Algebra) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (F.map X.a) (adj.counit.app (F.obj X.A))) G
• CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] (A : adj.toMonad.Algebra) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
• CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfReflectsColimitOfIsSplitPair 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] (A : adj.toMonad.Algebra) : CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
• CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : CategoryTheory.Functor adj.toMonad.Algebra D
• CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison adj ⊣ CategoryTheory.Monad.comparison adj
• CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A ⟶ B) ≃ (A ⟶ (CategoryTheory.Monad.comparison adj).obj B)
• CategoryTheory.Monad.MonadicityInternal.instHasColimitWalkingParallelPairParallelPairMapAppCounitObjOfHasCoequalizerAA 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B))))
• CategoryTheory.Monad.MonadicityInternal.unitCofork 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : CategoryTheory.Limits.Cofork (G.map (F.map A.a)) (G.map (adj.counit.app (F.obj A.A)))
• CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit_app 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) : (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit.app B = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))) (CategoryTheory.Monad.MonadicityInternal.counitCofork adj B)
• CategoryTheory.Monad.MonadicityInternal.unitCofork_pt 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.unitCofork A).pt = G.obj (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))
• CategoryTheory.Monad.MonadicityInternal.unitColimitOfPreservesCoequalizer 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G] : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.MonadicityInternal.unitCofork A)
• CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (A : adj.toMonad.Algebra) : ((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.app A).f = (CategoryTheory.Monad.beckCoequalizer A).desc (CategoryTheory.Monad.MonadicityInternal.unitCofork A)
• CategoryTheory.Monad.MonadicityInternal.unitCofork_π 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} (A : adj.toMonad.Algebra) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.unitCofork A).π = G.map (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
• CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f_aux 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G} [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (A : adj.toMonad.Algebra) : ((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.app A).f = (adj.homEquiv A.A (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))) (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
• CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_apply_f 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (a✝ : CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A ⟶ B) : ((CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B) a✝).f = ↑(((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B).trans ((adj.homEquiv A.A B).subtypeEquiv ⋯)) a✝)
• CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv_symm_apply 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) (B : D) [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (a✝ : A ⟶ (CategoryTheory.Monad.comparison adj).obj B) : (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B).symm a✝ = (((adj.homEquiv A.A B).symm.subtypeEquiv ⋯).trans (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B).symm) ({ toFun := fun f => ⟨f.f, ⋯⟩, invFun := fun g => { f := ↑g, h := ⋯ }, left_inv := ⋯, right_inv := ⋯ } a✝)
• CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_counit 📋 Mathlib.CategoryTheory.Monad.Monadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) [∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] : (CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit = { app := fun Y => (((adj.homEquiv (G.obj Y) Y).symm.subtypeEquiv ⋯).trans (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))) Y).symm) ({ toFun := fun f => ⟨f.f, ⋯⟩, invFun := fun g => { f := ↑g, h := ⋯ }, left_inv := ⋯, right_inv := ⋯ } (CategoryTheory.CategoryStruct.id ((CategoryTheory.Monad.comparison adj).obj Y))), naturality := ⋯ }
• CategoryTheory.Monad.algebraPreadditive 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [T.Additive] : CategoryTheory.Preadditive T.Algebra
• CategoryTheory.Monad.forget_additive 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [T.Additive] : T.forget.Additive
• CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [T.Additive] (F G : T.Algebra) : CategoryTheory.Monad.Algebra.Hom.f 0 = 0
• CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [T.Additive] (F G : T.Algebra) (α : F ⟶ G) : (-α).f = -α.f
• CategoryTheory.Monad.algebraPreadditive_homGroup_zsmul_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [T.Additive] (F G : T.Algebra) (r : ℤ) (α : F ⟶ G) : (r • α).f = r • α.f
• CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [T.Additive] (F G : T.Algebra) (α β : F ⟶ G) : (α - β).f = α.f - β.f
• CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [T.Additive] (F G : T.Algebra) (n : ℕ) (α : F ⟶ G) : (n • α).f = n • α.f
• CategoryTheory.Monad.algebraPreadditive_homGroup_add_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (T : CategoryTheory.Monad C) [T.Additive] (F G : T.Algebra) (α β : F ⟶ G) : (α + β).f = α.f + β.f
• MeasCat.Integral 📋 Mathlib.MeasureTheory.Category.MeasCat
  : MeasCat.Giry.Algebra

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c