Loogle!

Result

Found 97 declarations mentioning CategoryTheory.Comonad.Coalgebra.A.

• CategoryTheory.Comonad.Coalgebra.A 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) : C
• CategoryTheory.Comonad.forget_obj 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (A : G.Coalgebra) : G.forget.obj A = A.A
• CategoryTheory.Comonad.Coalgebra.a 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) : self.A ⟶ G.obj self.A
• CategoryTheory.Comonad.Coalgebra.Hom.f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (self : A.Hom B) : A.A ⟶ B.A
• CategoryTheory.Comonad.cofree_obj_A 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) : (G.cofree.obj X).A = G.obj X
• CategoryTheory.Comonad.Coalgebra.id_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : G.Coalgebra) : (CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.A
• CategoryTheory.Comonad.algebra_epi_of_epi 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X Y : G.Coalgebra} (f : X ⟶ Y) [h : CategoryTheory.Epi f.f] : CategoryTheory.Epi f
• CategoryTheory.Comonad.algebra_mono_of_mono 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X Y : G.Coalgebra} (f : X ⟶ Y) [h : CategoryTheory.Mono f.f] : CategoryTheory.Mono f
• CategoryTheory.Comonad.coalgebra_iso_of_iso 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {A B : G.Coalgebra} (f : A ⟶ B) [CategoryTheory.IsIso f.f] : CategoryTheory.IsIso f
• CategoryTheory.Comonad.Coalgebra.Hom.ext 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} {x y : A.Hom B} (f : x.f = y.f) : x = y
• CategoryTheory.Comonad.Coalgebra.Hom.ext_iff 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} {x y : A.Hom B} : x = y ↔ x.f = y.f
• CategoryTheory.Comonad.forget_map 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X✝ Y✝ : G.Coalgebra} (f : X✝ ⟶ Y✝) : G.forget.map f = f.f
• CategoryTheory.Comonad.Coalgebra.Hom.ext' 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (X Y : G.Coalgebra) (f g : X ⟶ Y) (h : f.f = g.f) : f = g
• CategoryTheory.Comonad.Coalgebra.Hom.ext'_iff 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {X Y : G.Coalgebra} {f g : X ⟶ Y} : f = g ↔ f.f = g.f
• CategoryTheory.Comonad.Coalgebra.counit 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) : CategoryTheory.CategoryStruct.comp self.a (G.ε.app self.A) = CategoryTheory.CategoryStruct.id self.A
• CategoryTheory.Comonad.Coalgebra.counit_assoc 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) {Z : C} (h : self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (G.ε.app self.A) h) = h
• CategoryTheory.Comonad.Coalgebra.comp_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A A' A'' : G.Coalgebra} (f : A ⟶ A') (g : A' ⟶ A'') : (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
• CategoryTheory.Comonad.Coalgebra.Hom.h 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (self : A.Hom B) : CategoryTheory.CategoryStruct.comp A.a (G.map self.f) = CategoryTheory.CategoryStruct.comp self.f B.a
• CategoryTheory.Comonad.Coalgebra.Hom.mk 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (f : A.A ⟶ B.A) (h : CategoryTheory.CategoryStruct.comp A.a (G.map f) = CategoryTheory.CategoryStruct.comp f B.a := by cat_disch) : A.Hom B
• CategoryTheory.Comonad.Coalgebra.isoMk 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (h : A.A ≅ B.A) (w : CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a := by cat_disch) : A ≅ B
• CategoryTheory.Comonad.Coalgebra.Hom.h_assoc 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (self : A.Hom B) {Z : C} (h : G.obj B.A ⟶ Z) : CategoryTheory.CategoryStruct.comp A.a (CategoryTheory.CategoryStruct.comp (G.map self.f) h) = CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp B.a h)
• CategoryTheory.Comonad.Coalgebra.coassoc 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) : CategoryTheory.CategoryStruct.comp self.a (G.δ.app self.A) = CategoryTheory.CategoryStruct.comp self.a (G.map self.a)
• CategoryTheory.Comonad.Coalgebra.isoMk_hom_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (h : A.A ≅ B.A) (w : CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a := by cat_disch) : (CategoryTheory.Comonad.Coalgebra.isoMk h w).hom.f = h.hom
• CategoryTheory.Comonad.Coalgebra.isoMk_inv_f 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra} (h : A.A ≅ B.A) (w : CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a := by cat_disch) : (CategoryTheory.Comonad.Coalgebra.isoMk h w).inv.f = h.inv
• CategoryTheory.Comonad.Coalgebra.coassoc_assoc 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) {Z : C} (h : G.obj (G.obj self.A) ⟶ Z) : CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (G.δ.app self.A) h) = CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (G.map self.a) h)
• CategoryTheory.Comonad.adj_counit 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.adj.counit = { app := fun Y => G.ε.app Y, naturality := ⋯ }
• CategoryTheory.Comonad.adj_unit 📋 Mathlib.CategoryTheory.Monad.Algebra
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.adj.unit = { app := fun X => { f := X.a, h := ⋯ }, naturality := ⋯ }
• CategoryTheory.overToCoalgebra_obj_A 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (f : CategoryTheory.Over X) : ((CategoryTheory.overToCoalgebra X).obj f).A = f.left
• CategoryTheory.coalgebraToOver_obj 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (A : (CategoryTheory.prodComonad X).Coalgebra) : (CategoryTheory.coalgebraToOver X).obj A = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)
• CategoryTheory.coalgebraToOver_map 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : (CategoryTheory.prodComonad X).Coalgebra} (f : X✝ ⟶ Y✝) : (CategoryTheory.coalgebraToOver X).map f = CategoryTheory.Over.homMk f.f ⋯
• CategoryTheory.coalgebraEquivOver_unitIso 📋 Mathlib.CategoryTheory.Monad.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] : (CategoryTheory.coalgebraEquivOver X).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Comonad.Coalgebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.prodComonad X).Coalgebra).obj A).A) ⋯) ⋯
• CategoryTheory.Over.star_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X✝ : C) : ((CategoryTheory.Over.star X).obj X✝).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ X✝))) CategoryTheory.Limits.prod.fst
• CategoryTheory.Over.star_map_left 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Over.star X).map f).left = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f
• CategoryTheory.Comonad.CofreeEqualizer.ι 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : X ⟶ T.cofree.obj X.A
• CategoryTheory.Comonad.CofreeEqualizer.ι_f 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : (CategoryTheory.Comonad.CofreeEqualizer.ι X).f = X.a
• CategoryTheory.Comonad.CofreeEqualizer.bottomMap 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : T.cofree.obj X.A ⟶ T.cofree.obj (T.obj X.A)
• CategoryTheory.Comonad.CofreeEqualizer.topMap 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : T.cofree.obj X.A ⟶ T.cofree.obj (T.obj X.A)
• CategoryTheory.Comonad.beckCoalgebraFork 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.Limits.Fork (CategoryTheory.Comonad.CofreeEqualizer.topMap X) (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)
• CategoryTheory.Comonad.instIsCoreflexivePairCoalgebraTopMapBottomMap 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.IsCoreflexivePair (CategoryTheory.Comonad.CofreeEqualizer.topMap X) (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)
• CategoryTheory.Comonad.beckCoalgebraEqualizer 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.beckCoalgebraFork X)
• CategoryTheory.Comonad.beckCoalgebraFork_pt 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : (CategoryTheory.Comonad.beckCoalgebraFork X).pt = X
• CategoryTheory.Comonad.beckFork 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.Limits.Fork (T.map X.a) (T.δ.app X.A)
• CategoryTheory.Comonad.beckEqualizer 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.beckFork X)
• CategoryTheory.Comonad.beckSplitEqualizer 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.IsSplitEqualizer (T.map X.a) (T.δ.app X.A) X.a
• CategoryTheory.Comonad.beckFork_pt 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : (CategoryTheory.Comonad.beckFork X).pt = X.A
• CategoryTheory.Comonad.CofreeEqualizer.topMap_f 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : (CategoryTheory.Comonad.CofreeEqualizer.topMap X).f = T.map X.a
• CategoryTheory.Comonad.CofreeEqualizer.bottomMap_f 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X).f = T.δ.app X.A
• CategoryTheory.Comonad.CofreeEqualizer.condition 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X) (CategoryTheory.Comonad.CofreeEqualizer.topMap X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X) (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)
• CategoryTheory.Comonad.beckFork_ι 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) : (CategoryTheory.Comonad.beckFork X).ι = X.a
• CategoryTheory.Comonad.beckEqualizer_lift 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) (s : CategoryTheory.Limits.Fork (T.map X.a) (T.δ.app X.A)) : (CategoryTheory.Comonad.beckEqualizer X).lift s = CategoryTheory.CategoryStruct.comp s.ι (T.ε.app X.A)
• CategoryTheory.Comonad.beckCoalgebraFork_π_app 📋 Mathlib.CategoryTheory.Monad.Equalizer
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra) (X✝ : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Comonad.beckCoalgebraFork X).π.app X✝ = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X✝ = t → (X ⟶ (CategoryTheory.Limits.parallelPair (CategoryTheory.Comonad.CofreeEqualizer.topMap X) (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)).obj X✝)) (fun h => ⋯ ▸ CategoryTheory.Comonad.CofreeEqualizer.ι X) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X) (CategoryTheory.Comonad.CofreeEqualizer.topMap X)) X✝ ⋯
• CategoryTheory.Comonad.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 : C) : ((CategoryTheory.Comonad.comparison h).obj X).A = L.obj X
• CategoryTheory.Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA 📋 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.Coreflective R] (X : (CategoryTheory.coreflectorAdjunction R).toComonad.Coalgebra) : CategoryTheory.IsIso ((CategoryTheory.coreflectorAdjunction R).counit.app X.A)
• CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_A 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) : (CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t).A = c.pt
• CategoryTheory.Comonad.ForgetCreatesLimits'.γ_app 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} (j : J) : CategoryTheory.Comonad.ForgetCreatesLimits'.γ.app j = (D.obj j).a
• CategoryTheory.Comonad.ForgetCreatesColimits'.γ_app 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) (j : J) : (CategoryTheory.Comonad.ForgetCreatesColimits'.γ D).app j = (D.obj j).a
• CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint_A 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) [CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint c t).A = c.pt
• CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (X : J) : (CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone D c).ι.app X = CategoryTheory.CategoryStruct.comp (D.obj X).a (T.map (c.ι.app X))
• CategoryTheory.Comonad.ForgetCreatesLimits'.commuting 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) [CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t) (T.map (c.π.app j)) = CategoryTheory.CategoryStruct.comp (c.π.app j) (D.obj j).a
• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.1 A.A))] : C
• CategoryTheory.Comonad.ComonadicityInternal.main_pair_coreflexive 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) : CategoryTheory.IsCoreflexivePair (G.map A.a) (adj.unit.app (G.obj A.A))
• CategoryTheory.Comonad.ComonadicityInternal.main_pair_F_cosplit 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) : F.IsCosplitPair (G.map A.a) (adj.unit.app (G.obj A.A))
• CategoryTheory.Comonad.instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
• CategoryTheory.Comonad.instCreatesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfCreatesLimitOfIsCosplitPair 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : CategoryTheory.CreatesLimit (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F
• CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair F] (X : adj.toComonad.Coalgebra) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (G.map X.a) (adj.unit.app (G.obj X.A))) F
• CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCosplitPair 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F
• CategoryTheory.Comonad.instReflectsLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfReflectsLimitOfIsCosplitPair 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair F] (A : adj.toComonad.Coalgebra) : CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F
• CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparison 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : CategoryTheory.Functor adj.toComonad.Coalgebra C
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : CategoryTheory.Comonad.comparison adj ⊣ CategoryTheory.Comonad.ComonadicityInternal.rightAdjointComparison adj
• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : ((CategoryTheory.Comonad.comparison adj).obj B ⟶ A) ≃ (B ⟶ CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj A)
• CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))
• CategoryTheory.Comonad.ComonadicityInternal.counitFork 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : CategoryTheory.Limits.Fork (F.map (G.map A.a)) (F.map (adj.unit.app (G.obj A.A)))
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_unit_app 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) : (CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).unit.app B = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) (CategoryTheory.Comonad.ComonadicityInternal.unitFork adj B)
• CategoryTheory.Comonad.ComonadicityInternal.counitFork_pt 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (CategoryTheory.Comonad.ComonadicityInternal.counitFork A).pt = F.obj (CategoryTheory.Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A)))
• CategoryTheory.Comonad.ComonadicityInternal.counitLimitOfPreservesEqualizer 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (G.map A.a) (adj.unit.app (G.obj A.A))) F] : CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.ComonadicityInternal.counitFork A)
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f = (CategoryTheory.Comonad.beckEqualizer A).lift (CategoryTheory.Comonad.ComonadicityInternal.counitFork A)
• CategoryTheory.Comonad.ComonadicityInternal.unitFork_ι 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} (A : adj.toComonad.Coalgebra) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (CategoryTheory.Comonad.ComonadicityInternal.counitFork A).ι = F.map (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))
• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (f : B ⟶ CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj A) : ((CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj A B).symm f).f = (adj.homEquiv B A.A).symm (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))))
• CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C) [CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (f : (CategoryTheory.Comonad.comparison adj).obj B ⟶ A) : (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj A B) f = CategoryTheory.Limits.equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] : (CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit = { app := fun Y => (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj Y (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj Y)).symm (CategoryTheory.CategoryStruct.id (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj Y)), naturality := ⋯ }
• CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux 📋 Mathlib.CategoryTheory.Monad.Comonadicity
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (A : adj.toComonad.Coalgebra) : ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f = (adj.homEquiv (CategoryTheory.Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) A.A).symm (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))
• CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (U : CategoryTheory.Comonad C) [U.Additive] (F G : U.Coalgebra) : CategoryTheory.Comonad.Coalgebra.Hom.f 0 = 0
• CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (U : CategoryTheory.Comonad C) [U.Additive] (F G : U.Coalgebra) (α : F ⟶ G) : (-α).f = -α.f
• CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (U : CategoryTheory.Comonad C) [U.Additive] (F G : U.Coalgebra) (r : ℤ) (α : F ⟶ G) : (r • α).f = r • α.f
• CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (U : CategoryTheory.Comonad C) [U.Additive] (F G : U.Coalgebra) (α β : F ⟶ G) : (α - β).f = α.f - β.f
• CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (U : CategoryTheory.Comonad C) [U.Additive] (F G : U.Coalgebra) (n : ℕ) (α : F ⟶ G) : (n • α).f = n • α.f
• CategoryTheory.Comonad.coalgebraPreadditive_homGroup_add_f 📋 Mathlib.CategoryTheory.Preadditive.EilenbergMoore
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (U : CategoryTheory.Comonad C) [U.Additive] (F G : U.Coalgebra) (α β : F ⟶ G) : (α + β).f = α.f + β.f
• CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_functor_obj_A 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (D : F.DescentDataAsCoalgebra fun x => f) : ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor.obj D).A = D.obj default
• CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_obj 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (A : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) (x✝ : ι) : ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).inverse.obj A).obj x✝ = A.A
• CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_hom 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (A : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) (x✝ x✝¹ : ι) : ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).inverse.obj A).hom x✝ x✝¹ = A.a
• CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_map_hom 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) {X✝ Y✝ : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra} (φ : X✝ ⟶ Y✝) (i : ι) : ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).inverse.map φ).hom i = φ.f
• CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} (ι : Type u_2) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : ↑(F.obj { as := Opposite.op S }).obj) : ((CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f).hom.app X✝).f = CategoryTheory.CategoryStruct.id ((F.map f.op.toLoc).l.toFunctor.obj X✝)
• CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_inv_app_f 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} (ι : Type u_2) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : ↑(F.obj { as := Opposite.op S }).obj) : ((CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f).inv.app X✝).f = CategoryTheory.CategoryStruct.id ((F.map f.op.toLoc).l.toFunctor.obj X✝)
• CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : F.DescentDataAsCoalgebra fun x => f) (i : ι) : ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).unitIso.hom.app X✝).hom i = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_unitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : F.DescentDataAsCoalgebra fun x => f) (i : ι) : ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).unitIso.inv.app X✝).hom i = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) : ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).counitIso.hom.app X✝).f = CategoryTheory.CategoryStruct.id X✝.A
• CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_inv_app_f 📋 Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) (ι : Type u_1) [Unique ι] {X S : C} (f : X ⟶ S) (X✝ : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) : ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).counitIso.inv.app X✝).f = CategoryTheory.CategoryStruct.id X✝.A

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