Loogle!

Result

Found 76 declarations mentioning CategoryTheory.Comma.snd.

• CategoryTheory.Comma.snd 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : CategoryTheory.Functor (CategoryTheory.Comma L R) B
• CategoryTheory.Comma.snd_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.snd L R).obj X = X.right
• CategoryTheory.Comma.toIdPUnitEquiv_functor_iso 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})} {R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})} : (CategoryTheory.Comma.toIdPUnitEquiv L R).functor = CategoryTheory.Comma.snd L R
• CategoryTheory.Comma.snd_map 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {Y✝ X✝ : CategoryTheory.Comma L R} (f : Y✝ ⟶ X✝) : (CategoryTheory.Comma.snd L R).map f = f.right
• CategoryTheory.Comma.natTrans 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.fst L R).comp L ⟶ (CategoryTheory.Comma.snd L R).comp R
• CategoryTheory.Comma.natTrans_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.natTrans L R).app X = X.hom
• CategoryTheory.Comma.rightIso_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {R₁ : CategoryTheory.Functor B T} {L₁ : CategoryTheory.Functor A T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y) : (CategoryTheory.Comma.rightIso α).hom = α.hom.right
• CategoryTheory.Comma.rightIso_inv 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {R₁ : CategoryTheory.Functor B T} {L₁ : CategoryTheory.Functor A T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y) : (CategoryTheory.Comma.rightIso α).inv = α.inv.right
• CategoryTheory.Comma.map_snd 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {B' : Type u₄} [CategoryTheory.Category.{v₄, u₄} B'] {A' : Type u₅} [CategoryTheory.Category.{v₅, u₅} A'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {R : CategoryTheory.Functor B T} {L : CategoryTheory.Functor A T} {R' : CategoryTheory.Functor B' T'} {L' : CategoryTheory.Functor A' T'} {F₂ : CategoryTheory.Functor B B'} {F₁ : CategoryTheory.Functor A A'} {F : CategoryTheory.Functor T T'} (β : F₁.comp L' ⟶ L.comp F) (α : R.comp F ⟶ F₂.comp R') : (CategoryTheory.Comma.map β α).comp (CategoryTheory.Comma.snd L' R') = (CategoryTheory.Comma.snd L R).comp F₂
• CategoryTheory.Comma.mapSnd 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {B' : Type u₄} [CategoryTheory.Category.{v₄, u₄} B'] {A' : Type u₅} [CategoryTheory.Category.{v₅, u₅} A'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {R : CategoryTheory.Functor B T} {L : CategoryTheory.Functor A T} {R' : CategoryTheory.Functor B' T'} {L' : CategoryTheory.Functor A' T'} {F₂ : CategoryTheory.Functor B B'} {F₁ : CategoryTheory.Functor A A'} {F : CategoryTheory.Functor T T'} (β : F₁.comp L' ⟶ L.comp F) (α : R.comp F ⟶ F₂.comp R') : (CategoryTheory.Comma.map β α).comp (CategoryTheory.Comma.snd L' R') ≅ (CategoryTheory.Comma.snd L R).comp F₂
• CategoryTheory.Comma.unopFunctorCompFst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.unopFunctor L R).comp (CategoryTheory.Comma.fst R L).op ≅ CategoryTheory.Comma.snd L.op R.op
• CategoryTheory.Comma.unopFunctorCompSnd 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.unopFunctor L R).comp (CategoryTheory.Comma.snd R L).op ≅ CategoryTheory.Comma.fst L.op R.op
• CategoryTheory.Comma.opFunctorCompFst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.opFunctor L R).leftOp.comp (CategoryTheory.Comma.fst R.op L.op) ≅ (CategoryTheory.Comma.snd L R).op
• CategoryTheory.Comma.opFunctorCompSnd 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : (CategoryTheory.Comma.opFunctor L R).leftOp.comp (CategoryTheory.Comma.snd R.op L.op) ≅ (CategoryTheory.Comma.fst L R).op
• CategoryTheory.Comma.equivProd_functor_map 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.equivProd L R).functor.map f = CategoryTheory.Prod.mkHom f.left f.right
• CategoryTheory.Comma.mapSnd_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {B' : Type u₄} [CategoryTheory.Category.{v₄, u₄} B'] {A' : Type u₅} [CategoryTheory.Category.{v₅, u₅} A'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {R : CategoryTheory.Functor B T} {L : CategoryTheory.Functor A T} {R' : CategoryTheory.Functor B' T'} {L' : CategoryTheory.Functor A' T'} {F₂ : CategoryTheory.Functor B B'} {F₁ : CategoryTheory.Functor A A'} {F : CategoryTheory.Functor T T'} (β : F₁.comp L' ⟶ L.comp F) (α : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.mapSnd β α).hom.app X = CategoryTheory.CategoryStruct.id (F₂.obj X.right)
• CategoryTheory.Comma.mapSnd_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {B' : Type u₄} [CategoryTheory.Category.{v₄, u₄} B'] {A' : Type u₅} [CategoryTheory.Category.{v₅, u₅} A'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {R : CategoryTheory.Functor B T} {L : CategoryTheory.Functor A T} {R' : CategoryTheory.Functor B' T'} {L' : CategoryTheory.Functor A' T'} {F₂ : CategoryTheory.Functor B B'} {F₁ : CategoryTheory.Functor A A'} {F : CategoryTheory.Functor T T'} (β : F₁.comp L' ⟶ L.comp F) (α : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.mapSnd β α).inv.app X = CategoryTheory.CategoryStruct.id (F₂.obj X.right)
• CategoryTheory.Comma.equivProd_counitIso_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : (CategoryTheory.Comma.equivProd L R).counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Comma.equivProd_counitIso_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : (CategoryTheory.Comma.equivProd L R).counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Comma.unopFunctorCompFst_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctorCompFst L R).hom.app X = CategoryTheory.CategoryStruct.id X.right
• CategoryTheory.Comma.unopFunctorCompFst_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctorCompFst L R).inv.app X = CategoryTheory.CategoryStruct.id X.right
• CategoryTheory.Comma.unopFunctorCompSnd_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctorCompSnd L R).hom.app X = CategoryTheory.CategoryStruct.id X.left
• CategoryTheory.Comma.unopFunctorCompSnd_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op) : (CategoryTheory.Comma.unopFunctorCompSnd L R).inv.app X = CategoryTheory.CategoryStruct.id X.left
• CategoryTheory.Comma.opFunctorCompFst_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ) : (CategoryTheory.Comma.opFunctorCompFst L R).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).right)
• CategoryTheory.Comma.opFunctorCompFst_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ) : (CategoryTheory.Comma.opFunctorCompFst L R).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).right)
• CategoryTheory.Comma.opFunctorCompSnd_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ) : (CategoryTheory.Comma.opFunctorCompSnd L R).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).left)
• CategoryTheory.Comma.opFunctorCompSnd_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ) : (CategoryTheory.Comma.opFunctorCompSnd L R).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).left)
• CategoryTheory.Comma.costructuredArrowSndInclusion 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow L (R.obj b)) (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b)
• CategoryTheory.Comma.costructuredArrowSndProj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) : CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b) (CategoryTheory.CostructuredArrow L (R.obj b))
• CategoryTheory.Comma.costructuredArrowSndAdjunction 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) : CategoryTheory.Comma.costructuredArrowSndProj L R b ⊣ CategoryTheory.Comma.costructuredArrowSndInclusion L R b
• CategoryTheory.Comma.costructuredArrowSndInclusion_obj_right_as 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)) : ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).right.as = PUnit.unit
• CategoryTheory.Comma.costructuredArrowSndInclusion_obj_left_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)) : ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).left.right = b
• CategoryTheory.Comma.costructuredArrowSndInclusion_obj_hom 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)) : ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).hom = CategoryTheory.CategoryStruct.id b
• CategoryTheory.Comma.costructuredArrowSndInclusion_obj_left_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)) : ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).left.left = X.left
• CategoryTheory.Comma.costructuredArrowSndInclusion_obj_left_hom 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)) : ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).left.hom = X.hom
• CategoryTheory.Comma.costructuredArrowSndProj_obj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b) : (CategoryTheory.Comma.costructuredArrowSndProj L R b).obj X = CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp X.left.hom (R.map X.hom))
• CategoryTheory.Comma.costructuredArrowSndInclusion_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) {X✝ Y✝ : CategoryTheory.CostructuredArrow L (R.obj b)} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.costructuredArrowSndInclusion L R b).map f = CategoryTheory.CostructuredArrow.homMk { left := f.left, right := CategoryTheory.CategoryStruct.id b, w := ⋯ } ⋯
• CategoryTheory.Comma.costructuredArrowSndAdjunction_counit_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)) : (CategoryTheory.Comma.costructuredArrowSndAdjunction L R b).counit.app X = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.CategoryStruct.id X.left) ⋯
• CategoryTheory.Comma.costructuredArrowSndProj_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) {X✝ Y✝ : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.costructuredArrowSndProj L R b).map f = CategoryTheory.CostructuredArrow.homMk f.left.left ⋯
• CategoryTheory.Comma.costructuredArrowSndAdjunction_unit_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.snd L R) b) : (CategoryTheory.Comma.costructuredArrowSndAdjunction L R b).unit.app X = CategoryTheory.CostructuredArrow.homMk { left := CategoryTheory.CategoryStruct.id X.left.left, right := X.hom, w := ⋯ } ⋯
• CategoryTheory.Comma.preservesColimitsOfShape_snd 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.Limits.HasColimitsOfShape J B] [CategoryTheory.Limits.PreservesColimitsOfShape J L] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Comma.snd L R)
• CategoryTheory.Comma.colimitAuxiliaryCocone 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : CategoryTheory.Limits.Cocone ((F.comp (CategoryTheory.Comma.fst L R)).comp L)
• CategoryTheory.Comma.limitAuxiliaryCone 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) : CategoryTheory.Limits.Cone ((F.comp (CategoryTheory.Comma.snd L R)).comp R)
• CategoryTheory.Comma.hasColimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Comma.fst L R))] [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Comma.snd L R))] [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] : CategoryTheory.Limits.HasColimit F
• CategoryTheory.Comma.hasLimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Comma.fst L R))] [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Comma.snd L R))] [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] : CategoryTheory.Limits.HasLimit F
• CategoryTheory.Comma.colimitAuxiliaryCocone_pt 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).pt = R.obj c₂.pt
• CategoryTheory.Comma.limitAuxiliaryCone_pt 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) : (CategoryTheory.Comma.limitAuxiliaryCone F c₁).pt = L.obj c₁.pt
• CategoryTheory.Comma.coconeOfPreserves 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Comma.coneOfPreserves 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : CategoryTheory.Limits.Cone F
• CategoryTheory.Comma.fstSndJointlyReflectColimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {F : CategoryTheory.Functor J (CategoryTheory.Comma L R)} {c : CategoryTheory.Limits.Cocone F} [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] (h₁ : CategoryTheory.Limits.IsColimit ((CategoryTheory.Comma.fst L R).mapCocone c)) (h₂ : CategoryTheory.Limits.IsColimit ((CategoryTheory.Comma.snd L R).mapCocone c)) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Comma.fstSndJointlyReflectLimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {F : CategoryTheory.Functor J (CategoryTheory.Comma L R)} {c : CategoryTheory.Limits.Cone F} [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (h₁ : CategoryTheory.Limits.IsLimit ((CategoryTheory.Comma.fst L R).mapCone c)) (h₂ : CategoryTheory.Limits.IsLimit ((CategoryTheory.Comma.snd L R).mapCone c)) : CategoryTheory.Limits.IsLimit c
• CategoryTheory.Comma.coconeOfPreservesIsColimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂)
• CategoryTheory.Comma.coneOfPreservesIsLimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] {c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsLimit c₁) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : CategoryTheory.Limits.IsLimit (CategoryTheory.Comma.coneOfPreserves F c₁ t₂)
• CategoryTheory.Comma.coconeOfPreserves_pt_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.left = c₁.pt
• CategoryTheory.Comma.coconeOfPreserves_pt_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.right = c₂.pt
• CategoryTheory.Comma.coneOfPreserves_pt_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.left = c₁.pt
• CategoryTheory.Comma.coneOfPreserves_pt_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.right = c₂.pt
• CategoryTheory.Comma.coconeOfPreserves_pt_hom 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.hom = (CategoryTheory.Limits.isColimitOfPreserves L t₁).desc (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂)
• CategoryTheory.Comma.coneOfPreserves_pt_hom 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) : (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.hom = (CategoryTheory.Limits.isLimitOfPreserves R t₂).lift (CategoryTheory.Comma.limitAuxiliaryCone F c₁)
• CategoryTheory.Comma.colimitAuxiliaryCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (X : J) : (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).ι.app X = CategoryTheory.CategoryStruct.comp (F.obj X).hom (R.map (c₂.ι.app X))
• CategoryTheory.Comma.limitAuxiliaryCone_π_app 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) (X : J) : (CategoryTheory.Comma.limitAuxiliaryCone F c₁).π.app X = CategoryTheory.CategoryStruct.comp (L.map (c₁.π.app X)) (F.obj X).hom
• CategoryTheory.Comma.coconeOfPreserves_ι_app_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J) : ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).left = c₁.ι.app j
• CategoryTheory.Comma.coconeOfPreserves_ι_app_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J) : ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).right = c₂.ι.app j
• CategoryTheory.Comma.coneOfPreserves_π_app_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) (j : J) : ((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).left = c₁.π.app j
• CategoryTheory.Comma.coneOfPreserves_π_app_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))) {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂) (j : J) : ((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).right = c₂.π.app j
• CategoryTheory.Comma.initial_snd 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [L.Initial] : (CategoryTheory.Comma.snd L R).Initial
• CategoryTheory.Comma.final_snd 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.IsFiltered A] [CategoryTheory.IsFiltered B] [R.Final] : (CategoryTheory.Comma.snd L R).Final
• CategoryTheory.Comma.initial_snd_of_isConnected_costructuredArrow 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [∀ (b : B), CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow L (R.obj b))] : (CategoryTheory.Comma.snd L R).Initial
• CategoryTheory.Comma.final_snd_of_isFiltered_structuredArrow 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [CategoryTheory.IsFiltered A] [CategoryTheory.IsFiltered B] [∀ (a : A), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow (L.obj a) R)] : (CategoryTheory.Comma.snd L R).Final
• CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_hom 📋 Mathlib.CategoryTheory.Bicategory.Kan.HasKan
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h).hom = CategoryTheory.Bicategory.lanDesc ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h)
• CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_hom 📋 Mathlib.CategoryTheory.Bicategory.Kan.HasKan
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h).hom = CategoryTheory.Bicategory.lanLiftDesc ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h)
• CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_inv 📋 Mathlib.CategoryTheory.Bicategory.Kan.HasKan
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c) [CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x) [CategoryTheory.Bicategory.Lan.CommuteWith f g h] : (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h).inv = (CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h))
• CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_inv 📋 Mathlib.CategoryTheory.Bicategory.Kan.HasKan
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a) [CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c) [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] : (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h).inv = (CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g))
• CategoryTheory.instAdditiveCommaSnd 📋 Mathlib.CategoryTheory.Preadditive.Comma
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Preadditive A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Preadditive B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T) [L.Additive] (R : CategoryTheory.Functor B T) [R.Additive] : (CategoryTheory.Comma.snd L R).Additive
• CategoryTheory.Comma.instIsCardinalAccessibleSnd 📋 Mathlib.CategoryTheory.Presentable.Comma
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] (F₁ : CategoryTheory.Functor C₁ D) (F₂ : CategoryTheory.Functor C₂ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [F₁.IsCardinalAccessible κ] [CategoryTheory.HasCardinalFilteredColimits C₁ κ] [CategoryTheory.HasCardinalFilteredColimits C₂ κ] : (CategoryTheory.Comma.snd F₁ F₂).IsCardinalAccessible κ
• CategoryTheory.Comma.instPreservesCardinalPresentableSnd 📋 Mathlib.CategoryTheory.Presentable.Comma
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] (F₁ : CategoryTheory.Functor C₁ D) (F₂ : CategoryTheory.Functor C₂ D) (κ : Cardinal.{w}) [Fact κ.IsRegular] [CategoryTheory.IsCardinalAccessibleCategory C₁ κ] [CategoryTheory.IsCardinalAccessibleCategory C₂ κ] [F₁.IsCardinalAccessible κ] [F₂.IsCardinalAccessible κ] [F₁.PreservesCardinalPresentable κ] [CategoryTheory.LocallySmall.{w, v_3, u_3} D] : (CategoryTheory.Comma.snd F₁ F₂).PreservesCardinalPresentable κ

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