Loogle!

Result

Found 108 declarations mentioning CategoryTheory.Under.forget.

• CategoryTheory.Under.forget 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) : CategoryTheory.Functor (CategoryTheory.Under X) T
• CategoryTheory.Under.forgetCone 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) : CategoryTheory.Limits.Cone (CategoryTheory.Under.forget X)
• CategoryTheory.Under.forget_faithful 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} : (CategoryTheory.Under.forget X).Faithful
• CategoryTheory.Under.forget_reflects_iso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} : (CategoryTheory.Under.forget X).ReflectsIsomorphisms
• CategoryTheory.Under.forgetCone_pt 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) : (CategoryTheory.Under.forgetCone X).pt = X
• CategoryTheory.Under.forget_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Under X} : (CategoryTheory.Under.forget X).obj U = U.right
• CategoryTheory.Under.equivalenceOfIsInitial_functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).functor = CategoryTheory.Under.forget X
• CategoryTheory.Under.mapForget_eq 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) : (CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X) = CategoryTheory.Under.forget Y
• CategoryTheory.Under.mapForget 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y) : (CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X) ≅ CategoryTheory.Under.forget Y
• CategoryTheory.Under.post_forget_eq_forget_comp 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor T D) (X : T) : (CategoryTheory.Under.post F).comp (CategoryTheory.Under.forget (F.obj X)) = (CategoryTheory.Under.forget X).comp F
• CategoryTheory.StructuredArrow.ofDiagEquivalence 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T) ≌ CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)
• CategoryTheory.StructuredArrow.ofDiagEquivalence' 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T) ≌ CategoryTheory.StructuredArrow X.1 (CategoryTheory.Under.forget X.2)
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) : CategoryTheory.Functor (CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)) (CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1))
• CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) : CategoryTheory.Functor (CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)) (CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T))
• CategoryTheory.Under.forget_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} {f : U ⟶ V} : (CategoryTheory.Under.forget X).map f = CategoryTheory.Under.Hom.right f
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F) ≌ CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) (CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F))
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) (CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F))
• CategoryTheory.Functor.toUnder_comp_forget 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X ⟶ F.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) : (F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X) = F
• CategoryTheory.Functor.toUnderCompForget 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X ⟶ F.obj Y) (h : ∀ {Y Z : S} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) : (F.toUnder X f ⋯).comp (CategoryTheory.Under.forget X) ≅ F
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G) ≌ CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.Functor (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) (CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G)
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : CategoryTheory.Functor (CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G))
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).left.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).obj Y).left.as = PUnit.unit
• CategoryTheory.Under.forgetCone_π_app 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) (self : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (CategoryTheory.Functor.id T)) : (CategoryTheory.Under.forgetCone X).π.app self = self.hom
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).right.left.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).right.right = Y.right
• CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).obj Y).right = Y.right.right
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).left.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).left.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).right.left.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).right.left.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).left.as = PUnit.unit
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).right.right = Y✝.right.right
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).right.right = Y✝.right.right
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).right = X.right.right
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).hom = Y.hom.2
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.right = Y.right
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).hom = Y✝.right.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.left = Y.left.right
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).hom = Y✝.right.hom
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).right.hom = Y.hom.1
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence_functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).functor = CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence_inverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).inverse = CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).right.hom = Y✝.hom
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).right.hom = Y✝.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).hom = Y.left.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).left = CategoryTheory.Under.mk X.hom
• CategoryTheory.Under.equivalenceOfIsInitial_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (({ obj := fun Y => CategoryTheory.Under.mk (hX.to Y), map := fun {X_1 Y} f => CategoryTheory.Under.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.Under.forget X)).obj x)) ⋯
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).obj X).hom = X.right.hom
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_right_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).right.hom = Y.hom
• CategoryTheory.Under.equivalenceOfIsInitial_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Under X)).obj Y).right) ⋯) ⋯
• CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).obj Y).hom = (Y.right.hom, Y.hom)
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).map f).right = (CategoryTheory.StructuredArrow.Hom.right f).right
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).map g).right.right = g.right
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_right_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).map g).right.left = CategoryTheory.Under.Hom.right g.left
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G))).obj x)) ⋯
• CategoryTheory.StructuredArrow.ofCommaSndEquivalence_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) : (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).comp (CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c)).obj x)) ⋯
• CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T) (G : CategoryTheory.Functor D T) (c : C) {X✝ Y✝ : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).map f).left = CategoryTheory.Under.homMk (CategoryTheory.StructuredArrow.Hom.right f).left ⋯
• CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) {X✝ Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).map g).right.right = g.right
• CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_map_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) {X✝ Y✝ : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).map g).right = CategoryTheory.Under.Hom.right g.right
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) {X✝ Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).map g).right.right = g.right.right
• CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) {X✝ Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).map g).right.right = CategoryTheory.Under.Hom.right g.right
• CommRingCat.forget₂Adj 📋 Mathlib.Algebra.Category.Ring.Adjunctions
  {R : CommRingCat} (hR : CategoryTheory.Limits.IsInitial R) : R.monoidAlgebra.comp (CategoryTheory.Under.forget R) ⊣ CategoryTheory.forget₂ CommRingCat CommMonCat
• CommRingCat.monoidAlgebraAdj 📋 Mathlib.Algebra.Category.Ring.Adjunctions
  (R : CommRingCat) : R.monoidAlgebra ⊣ (CategoryTheory.Under.forget R).comp (CategoryTheory.forget₂ CommRingCat CommMonCat)
• CategoryTheory.Under.instIsRightAdjointForget 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : (CategoryTheory.Under.forget X).IsRightAdjoint
• CategoryTheory.Under.costarAdjForget 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryCoproducts C] : CategoryTheory.Under.costar X ⊣ CategoryTheory.Under.forget X
• CategoryTheory.Under.forgetMapInitial 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.Under.forget X ≅ (CategoryTheory.Under.map (hI.to X)).comp (CategoryTheory.Under.equivalenceOfIsInitial hI).functor
• CategoryTheory.Under.forgetMapInitial_hom_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) (X✝ : CategoryTheory.Under X) : (CategoryTheory.Under.forgetMapInitial X hI).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.right
• CategoryTheory.Under.forgetMapInitial_inv_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) (X✝ : CategoryTheory.Under X) : (CategoryTheory.Under.forgetMapInitial X hI).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.right
• CategoryTheory.Limits.Cone.toStructuredArrow_comp_toUnder_comp_forget 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.toStructuredArrow.comp ((CategoryTheory.StructuredArrow.toUnder c.pt F).comp (CategoryTheory.Under.forget c.pt)) = F
• CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.toStructuredArrow.comp ((CategoryTheory.StructuredArrow.toUnder c.pt F).comp (CategoryTheory.Under.forget c.pt)) ≅ F
• CategoryTheory.Limits.Cone.mapConeToUnder 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Under.forget c.pt).mapCone c.toUnder ≅ c
• CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget_hom_app 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J) : c.toStructuredArrowCompToUnderCompForget.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget_inv_app 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J) : c.toStructuredArrowCompToUnderCompForget.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Limits.Cone.mapConeToUnder_hom_hom 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.mapConeToUnder.hom.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.Cone.mapConeToUnder_inv_hom 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.mapConeToUnder.inv.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Under.createsLimitsOfSize 📋 Mathlib.CategoryTheory.Limits.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : CategoryTheory.CreatesLimitsOfSize.{w, w', v, v, max u v, u} (CategoryTheory.Under.forget X)
• CategoryTheory.Under.hasLimit_of_hasLimit_comp_forget 📋 Mathlib.CategoryTheory.Limits.Over
  {J : Type w} [CategoryTheory.Category.{w', w} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (F : CategoryTheory.Functor J (CategoryTheory.Under X)) [i : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Under.forget X))] : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Under.createLimitsOfSizeMapCompForget 📋 Mathlib.CategoryTheory.Limits.Over
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CreatesLimitsOfSize.{w, w', v, v, max u v, u} ((CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X))
• CategoryTheory.WithInitial.commaFromUnder_obj_right 📋 Mathlib.CategoryTheory.WithTerminal.Cone
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} (K : CategoryTheory.Functor J (CategoryTheory.Under X)) : (CategoryTheory.WithInitial.commaFromUnder.obj K).right = K.comp (CategoryTheory.Under.forget X)
• CategoryTheory.WithInitial.commaFromUnder_obj_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Cone
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} (K : CategoryTheory.Functor J (CategoryTheory.Under X)) (a : J) : (CategoryTheory.WithInitial.commaFromUnder.obj K).hom.app a = (K.obj a).hom
• CategoryTheory.WithInitial.commaFromUnder_map_left 📋 Mathlib.CategoryTheory.WithTerminal.Cone
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} {X✝ Y✝ : CategoryTheory.Functor J (CategoryTheory.Under X)} (f : X✝ ⟶ Y✝) : (CategoryTheory.WithInitial.commaFromUnder.map f).left = CategoryTheory.CategoryStruct.id X
• CategoryTheory.WithInitial.commaFromUnder_map_right 📋 Mathlib.CategoryTheory.WithTerminal.Cone
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [CategoryTheory.Category.{w', w} J] {X : C} {X✝ Y✝ : CategoryTheory.Functor J (CategoryTheory.Under X)} (f : X✝ ⟶ Y✝) : (CategoryTheory.WithInitial.commaFromUnder.map f).right = CategoryTheory.Functor.whiskerRight f (CategoryTheory.Under.forget X)
• CategoryTheory.MorphismProperty.under_eq_inverseImage 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
  {T : Type u_3} [CategoryTheory.Category.{v_3, u_3} T] (W : CategoryTheory.MorphismProperty T) (X : T) : W.under = W.inverseImage (CategoryTheory.Under.forget X)
• CategoryTheory.MorphismProperty.Under.forget_comp_forget_map 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
  {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T) [Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B) : ((CategoryTheory.MorphismProperty.Under.forget P Q X).comp (CategoryTheory.Under.forget X)).map f = f.right
• CategoryTheory.Limits.IsColimit.underPost 📋 Mathlib.CategoryTheory.Limits.Final
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D} (hc : CategoryTheory.Limits.IsColimit c) (j : J) [(CategoryTheory.Under.forget j).Final] : CategoryTheory.Limits.IsColimit (c.underPost j)
• CategoryTheory.Under.final_forget 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (c : C) : (CategoryTheory.Under.forget c).Final
• CategoryTheory.Under.createsColimitsOfShapeForgetOfIsConnected 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
  {J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsConnected J] {B : C} : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.Under.forget B)
• CategoryTheory.Under.preservesColimitsOfShape_forget_of_isConnected 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
  {J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsConnected J] {B : C} : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Under.forget B)
• CategoryTheory.Limits.instPreservesFilteredColimitsOfSizeUnderForget 📋 Mathlib.CategoryTheory.Limits.Preserves.Over
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X : C} : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1} (CategoryTheory.Under.forget X)
• CommRingCat.preservesColimit_coyoneda_of_finitePresentation 📋 Mathlib.Algebra.Category.Ring.FinitePresentation
  {J : Type uJ} [CategoryTheory.Category.{vJ, uJ} J] [CategoryTheory.IsFiltered J] (R : CommRingCat) (S : CategoryTheory.Under R) (hS : (CommRingCat.Hom.hom S.hom).FinitePresentation) (F : CategoryTheory.Functor J (CategoryTheory.Under R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Under.forget R)) (CategoryTheory.forget CommRingCat)] : CategoryTheory.Limits.PreservesColimit F (CategoryTheory.coyoneda.obj (Opposite.op S))
• CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀) : (CategoryTheory.Functor.const (CategoryTheory.Under j₀)).obj X ⟶ (CategoryTheory.Under.forget j₀).comp Y
• CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g_app 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀) (t : CategoryTheory.Under j₀) : (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y).app t = CategoryTheory.CategoryStruct.comp y (Y.map t.hom)
• CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀) (j : CategoryTheory.Under j₀) : (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F y).obj j = CategoryTheory.MonoOver.mk ((CategoryTheory.Limits.kernel.ι (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).app j)
• CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀) {j j' : CategoryTheory.Under j₀} (f : j ⟶ j') : (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F y).map f = CategoryTheory.MonoOver.homMk ((CategoryTheory.Limits.kernel (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).map f) ⋯
• CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀) : CategoryTheory.Limits.colimit (CategoryTheory.Limits.kernel (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)) ⟶ X
• CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y} (hc : CategoryTheory.Limits.IsColimit c) {j₀ : J} {y : X ⟶ Y.obj j₀} (hy : CategoryTheory.CategoryStruct.comp y (c.ι.app j₀) = 0) [CategoryTheory.IsFiltered J] : CategoryTheory.Epi (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f y)
• CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀) (j : CategoryTheory.Under j₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.kernel (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)) j) (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f y) = (CategoryTheory.Limits.kernel.ι (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).app j
• CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_obj 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] (j : J) : (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂).obj j = CategoryTheory.Enriched.FunctorCategory.enrichedHom V ((CategoryTheory.Under.forget j).comp F₁) ((CategoryTheory.Under.forget j).comp F₂)
• CategoryTheory.Enriched.FunctorCategory.instHasEnrichedHomUnderCompMapForget 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] {j j' : J} (f : j ⟶ j') : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V ((CategoryTheory.Under.map f).comp ((CategoryTheory.Under.forget j).comp F₁)) ((CategoryTheory.Under.map f).comp ((CategoryTheory.Under.forget j).comp F₂))
• CategoryTheory.Enriched.FunctorCategory.functorEnrichedId_app 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₁] (j : J) : (CategoryTheory.Enriched.FunctorCategory.functorEnrichedId V F₁).app j = CategoryTheory.Enriched.FunctorCategory.enrichedId V ((CategoryTheory.Under.forget j).comp F₁)
• CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom_π_app 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] (j : J) : (CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom V F₁ F₂).π.app j = CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom V F₁ F₂ (CategoryTheory.Under.forget j)
• CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp_app 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₃] [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₃] (j : J) : (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₃).app j = CategoryTheory.Enriched.FunctorCategory.enrichedComp V ((CategoryTheory.Under.forget j).comp F₁) ((CategoryTheory.Under.forget j).comp F₂) ((CategoryTheory.Under.forget j).comp F₃)
• CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_map 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C) [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂).map f = CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom' V (CategoryTheory.Under.map f) (CategoryTheory.Iso.refl ((CategoryTheory.Under.map f).comp ((CategoryTheory.Under.forget X✝).comp F₁))) (CategoryTheory.Iso.refl ((CategoryTheory.Under.map f).comp ((CategoryTheory.Under.forget X✝).comp F₂)))
• CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_apply_app 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] {F₁ F₂ : CategoryTheory.Functor J C} [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] (a✝ : F₁ ⟶ F₂) (X : J) : ((CategoryTheory.Enriched.FunctorCategory.functorHomEquiv V) a✝).app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Enriched.FunctorCategory.homEquiv V) a✝) (CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom V F₁ F₂ (CategoryTheory.Under.forget X))
• CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality 📋 Mathlib.CategoryTheory.Sites.Monoidal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalClosed A] {M : A} {F G : CategoryTheory.Functor Cᵒᵖ A} {X Y : C} (f : X ⟶ Y) [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F G] (y : ((CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom A F G).comp (CategoryTheory.coyoneda.obj (Opposite.op M))).obj (Opposite.op Y)) : (CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv M F G X) (CategoryTheory.CategoryStruct.comp y (CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom' A (CategoryTheory.Under.map f.op) (CategoryTheory.Iso.refl ((CategoryTheory.Under.map f.op).comp ((CategoryTheory.Under.forget (Opposite.op Y)).comp F))) (CategoryTheory.Iso.refl ((CategoryTheory.Under.map f.op).comp ((CategoryTheory.Under.forget (Opposite.op Y)).comp G))))) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.presheafHom (CategoryTheory.MonoidalCategoryStruct.tensorObj F ((CategoryTheory.Functor.const Cᵒᵖ).obj M)) G).map f.op)) ((CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv M F G Y) y)

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