Loogle!

Result

Found 198 declarations mentioning CategoryTheory.Grothendieck.

• CategoryTheory.Grothendieck 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : Type (max u u₂)
• CategoryTheory.Grothendieck.base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (self : CategoryTheory.Grothendieck F) : C
• CategoryTheory.Grothendieck.instCategory 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : CategoryTheory.Category.{max v₂ v, max u₂ u} (CategoryTheory.Grothendieck F)
• CategoryTheory.Grothendieck.Hom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X Y : CategoryTheory.Grothendieck F) : Type (max v v₂)
• CategoryTheory.Grothendieck.id 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : X.Hom X
• CategoryTheory.Grothendieck.forget 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) C
• CategoryTheory.Grothendieck.instInhabitedHom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : Inhabited (X.Hom X)
• CategoryTheory.Grothendieck.mk 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (base : C) (fiber : ↑(F.obj base)) : CategoryTheory.Grothendieck F
• CategoryTheory.Grothendieck.fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (self : CategoryTheory.Grothendieck F) : ↑(F.obj self.base)
• CategoryTheory.Grothendieck.transport 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : CategoryTheory.Grothendieck F
• CategoryTheory.Grothendieck.forget_obj 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.forget F).obj X = X.base
• CategoryTheory.Grothendieck.ι 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C) : CategoryTheory.Functor (↑(F.obj c)) (CategoryTheory.Grothendieck F)
• CategoryTheory.Grothendieck.comp 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y Z : CategoryTheory.Grothendieck F} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z
• CategoryTheory.Grothendieck.Hom.base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (self : X.Hom Y) : X.base ⟶ Y.base
• CategoryTheory.Grothendieck.faithful_ι 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (c : C) : (CategoryTheory.Grothendieck.ι F c).Faithful
• CategoryTheory.Grothendieck.transport_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.transport t).base = c
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor) ≌ CategoryTheory.Grothendieck F
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)) (CategoryTheory.Grothendieck F)
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor))
• CategoryTheory.Grothendieck.grothendieckTypeToCat 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat) ≌ G.Elements
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Functor (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) G.Elements
• CategoryTheory.Grothendieck.grothendieckTypeToCatInverse 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Functor G.Elements (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat))
• CategoryTheory.Grothendieck.transportIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : x.transport α.hom ≅ x
• CategoryTheory.Grothendieck.pre 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) : CategoryTheory.Functor (CategoryTheory.Grothendieck (G.comp F)) (CategoryTheory.Grothendieck F)
• CategoryTheory.Grothendieck.toTransport 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : x ⟶ x.transport t
• CategoryTheory.Grothendieck.map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) (CategoryTheory.Grothendieck G)
• CategoryTheory.Grothendieck.map_id_eq 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.id F) = CategoryTheory.Functor.id (CategoryTheory.Grothendieck F)
• CategoryTheory.Grothendieck.preEquivalence 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : D ≌ C) : CategoryTheory.Grothendieck (G.functor.comp F) ≌ CategoryTheory.Grothendieck F
• CategoryTheory.Grothendieck.preInv 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : D ≌ C) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) (CategoryTheory.Grothendieck (G.functor.comp F))
• CategoryTheory.Grothendieck.toTransport_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.toTransport t).base = t
• CategoryTheory.Grothendieck.id_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base
• CategoryTheory.Grothendieck.ι_obj 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C) (d : ↑(F.obj c)) : (CategoryTheory.Grothendieck.ι F c).obj d = { base := c, fiber := d }
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).obj X).base = X.base
• CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).base = X.fst
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).obj X).base = X.base
• CategoryTheory.Grothendieck.map_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.map α).obj X).base = X.base
• CategoryTheory.Grothendieck.forget_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck F} (f : X✝ ⟶ Y✝) : (CategoryTheory.Grothendieck.forget F).map f = f.base
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_functor 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).functor = CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_inverse 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).inverse = CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F
• CategoryTheory.Grothendieck.functor_comp_forget 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} : (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.forget G) = CategoryTheory.Grothendieck.forget F
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_fst 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).fst = X.base
• CategoryTheory.Grothendieck.pre_id 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Grothendieck.pre F (CategoryTheory.Functor.id C) = CategoryTheory.Functor.id (CategoryTheory.Grothendieck ((CategoryTheory.Functor.id C).comp F))
• CategoryTheory.Grothendieck.base_eqToHom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (h : X = Y) : (CategoryTheory.eqToHom h).base = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.pre_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) (X : CategoryTheory.Grothendieck (G.comp F)) : ((CategoryTheory.Grothendieck.pre F G).obj X).base = G.obj X.base
• CategoryTheory.Grothendieck.mapIdIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : (CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.id F)).toCatHom ≅ CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (CategoryTheory.Grothendieck F))
• CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).base = X.fst
• CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).fiber.as = X.snd
• CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).fst = X.base
• CategoryTheory.Grothendieck.pre_obj_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) (X : CategoryTheory.Grothendieck (G.comp F)) : ((CategoryTheory.Grothendieck.pre F G).obj X).fiber = X.fiber
• CategoryTheory.Grothendieck.transportIso_hom_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).hom.base = α.inv
• CategoryTheory.Grothendieck.transportIso_inv_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).inv.base = α.hom
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as
• CategoryTheory.Grothendieck.transport_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.transport t).fiber = (F.map t).toFunctor.obj x.fiber
• CategoryTheory.Grothendieck.comp_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y Z : CategoryTheory.Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).fiber.as = X.snd
• CategoryTheory.Grothendieck.map_comp_eq 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G H : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.map β)
• CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).snd = X.fiber.as
• CategoryTheory.Grothendieck.mapCompIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G H : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) ≅ (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.map β)
• CategoryTheory.Grothendieck.map_obj 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.map α).obj X = { base := X.base, fiber := (α.app X.base).toFunctor.obj X.fiber }
• CategoryTheory.Grothendieck.map_obj_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.map α).obj X).fiber = (α.app X.base).toFunctor.obj X.fiber
• CategoryTheory.Grothendieck.isoMk 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : X ≅ Y
• CategoryTheory.Grothendieck.Hom.fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (self : X.Hom Y) : (F.map self.base).toFunctor.obj X.fiber ⟶ Y.fiber
• CategoryTheory.Grothendieck.pre_comp 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (G : CategoryTheory.Functor D C) (H : CategoryTheory.Functor E D) : CategoryTheory.Grothendieck.pre F (H.comp G) = (CategoryTheory.Grothendieck.pre (G.comp F) H).comp (CategoryTheory.Grothendieck.pre F G)
• CategoryTheory.Grothendieck.Hom.mk 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (base : X.base ⟶ Y.base) (fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber) : X.Hom Y
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).obj X).fiber = CategoryTheory.AsSmall.up.obj X.fiber
• CategoryTheory.Grothendieck.ιNatTrans 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C} (f : X ⟶ Y) : CategoryTheory.Grothendieck.ι F X ⟶ (F.map f).toFunctor.comp (CategoryTheory.Grothendieck.ι F Y)
• CategoryTheory.Grothendieck.ιCompMap 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) : (CategoryTheory.Grothendieck.ι F c).comp (CategoryTheory.Grothendieck.map α) ≅ (α.app c).toFunctor.comp (CategoryTheory.Grothendieck.ι F' c)
• CategoryTheory.Grothendieck.preNatIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) {G H : CategoryTheory.Functor D C} (α : G ≅ H) : CategoryTheory.Grothendieck.pre F G ≅ (CategoryTheory.Grothendieck.map (CategoryTheory.Functor.whiskerRight α.hom F)).comp (CategoryTheory.Grothendieck.pre F H)
• CategoryTheory.Grothendieck.isoMk_hom_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).hom.base = e₁.hom
• CategoryTheory.Grothendieck.isoMk_inv_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).inv.base = e₁.inv
• CategoryTheory.Grothendieck.pre_comp_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {F : CategoryTheory.Functor C CategoryTheory.Cat} (G : CategoryTheory.Functor D C) {H : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ H) : (CategoryTheory.Grothendieck.pre F G).comp (CategoryTheory.Grothendieck.map α) = (CategoryTheory.Grothendieck.map (G.whiskerLeft α)).comp (CategoryTheory.Grothendieck.pre H G)
• CategoryTheory.Grothendieck.eqToHom_eq 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (hF : X = Y) : CategoryTheory.eqToHom hF = { base := CategoryTheory.eqToHom ⋯, fiber := CategoryTheory.eqToHom ⋯ }
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_counitIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).comp (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F))
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).obj X).fiber = CategoryTheory.AsSmall.down.obj X.fiber
• CategoryTheory.Grothendieck.pre_comp_map_assoc 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {F : CategoryTheory.Functor C CategoryTheory.Cat} (G : CategoryTheory.Functor D C) {H : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ H) {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (K : CategoryTheory.Functor (CategoryTheory.Grothendieck H) E) : (CategoryTheory.Grothendieck.pre F G).comp ((CategoryTheory.Grothendieck.map α).comp K) = (CategoryTheory.Grothendieck.map (G.whiskerLeft α)).comp ((CategoryTheory.Grothendieck.pre H G).comp K)
• CategoryTheory.Grothendieck.ιNatTrans_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C} (f : X ⟶ Y) (d : ↑(F.obj X)) : ((CategoryTheory.Grothendieck.ιNatTrans f).app d).base = f
• CategoryTheory.Grothendieck.pre_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp F)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.pre F G).map f).base = G.map f.base
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_unitIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)))
• CategoryTheory.Grothendieck.map_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : ((CategoryTheory.Grothendieck.map α).map f).base = f.base
• CategoryTheory.Grothendieck.mapWhiskerRightAsSmallFunctor 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) : CategoryTheory.Grothendieck.map (CategoryTheory.Functor.whiskerRight α CategoryTheory.Cat.asSmallFunctor) ≅ (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).functor.comp ((CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence G).inverse)
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).map f).base = f.base
• CategoryTheory.Grothendieck.id_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.CategoryStruct.id X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.fiber_eqToHom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (h : X = Y) : (CategoryTheory.eqToHom h).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.preUnitIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : D ≌ C) : CategoryTheory.Grothendieck.map (CategoryTheory.Functor.whiskerRight G.unitInv (G.functor.comp F)) ≅ CategoryTheory.Grothendieck.pre (G.functor.comp F) (G.functor.comp G.inverse)
• CategoryTheory.Grothendieck.mapWhiskerLeftIsoConjPreMap 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (G : D ≌ C) (α : F ⟶ F') : CategoryTheory.Grothendieck.map (G.functor.whiskerLeft α) ≅ (CategoryTheory.Grothendieck.preEquivalence F G).functor.comp ((CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.preEquivalence F' G).inverse)
• CategoryTheory.Grothendieck.isoMk_hom_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).hom.fiber = e₂.hom
• CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X✝ Y✝ : G.Elements} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).map f).base = ↑f
• CategoryTheory.Grothendieck.toTransport_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.toTransport t).fiber = CategoryTheory.CategoryStruct.id ((F.map t).toFunctor.obj x.fiber)
• CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X✝ Y✝ : G.Elements} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.map f).base = ↑f
• CategoryTheory.Grothendieck.transportIso_inv_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).inv.fiber = CategoryTheory.CategoryStruct.id ((F.map α.hom).toFunctor.obj x.fiber)
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).map f).base = f.base
• CategoryTheory.Grothendieck.ι_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C) {X✝ Y✝ : ↑(F.obj c)} (f : X✝ ⟶ Y✝) : (CategoryTheory.Grothendieck.ι F c).map f = { base := CategoryTheory.CategoryStruct.id { base := c, fiber := X✝ }.base, fiber := CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f }
• CategoryTheory.Grothendieck.pre_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp F)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.pre F G).map f).fiber = f.fiber
• CategoryTheory.Grothendieck.transportIso_hom_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).hom.fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ιCompMap_hom_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).hom.app X).base = CategoryTheory.CategoryStruct.id c
• CategoryTheory.Grothendieck.ιCompMap_inv_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).inv.app X).base = CategoryTheory.CategoryStruct.id c
• CategoryTheory.Grothendieck.ext 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (f g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber) : f = g
• CategoryTheory.Grothendieck.congr 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} {f g : X ⟶ Y} (h : f = g) : f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).base = CategoryTheory.CategoryStruct.id X.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).base = CategoryTheory.CategoryStruct.id X.base
• CategoryTheory.Grothendieck.isoMk_inv_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).inv.fiber = CategoryTheory.CategoryStruct.comp ((F.map e₁.inv).toFunctor.map e₂.inv) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X✝ ⟶ Y✝) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).map f) = f.base
• CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X✝ ⟶ Y✝) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.map f) = f.base
• CategoryTheory.Grothendieck.comp_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y Z : CategoryTheory.Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map g.base).toFunctor.map f.fiber) g.fiber)
• CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.hom.app X) = CategoryTheory.CategoryStruct.id X.fst
• CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.inv.app X) = CategoryTheory.CategoryStruct.id X.fst
• CategoryTheory.Grothendieck.functorFrom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) E
• CategoryTheory.Grothendieck.functorFrom_obj 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).obj X = (fib X.base).obj X.fiber
• CategoryTheory.Grothendieck.ιCompFunctorFrom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) (c : C) : (CategoryTheory.Grothendieck.ι F c).comp (CategoryTheory.Grothendieck.functorFrom fib (fun {c c'} => hom) hom_id hom_comp) ≅ fib c
• CategoryTheory.Grothendieck.map_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} {X Y : CategoryTheory.Grothendieck F} {f : X ⟶ Y} : (CategoryTheory.Grothendieck.map α).map f = { base := f.base, fiber := CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).toNatTrans.app X.fiber) ((α.app Y.base).toFunctor.map f.fiber) }
• CategoryTheory.Grothendieck.functorFrom_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).map f = CategoryTheory.CategoryStruct.comp ((hom f.base).app X.fiber) ((fib Y.base).map f.fiber)
• CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).hom.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).inv.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ιNatTrans_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C} (f : X ⟶ Y) (d : ↑(F.obj X)) : ((CategoryTheory.Grothendieck.ιNatTrans f).app d).fiber = CategoryTheory.CategoryStruct.id ((F.map f).toFunctor.obj ((CategoryTheory.Grothendieck.ι F X).obj d).fiber)
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.map_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : ((CategoryTheory.Grothendieck.map α).map f).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((α.app Y.base).toFunctor.map f.fiber)
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).map f).fiber = CategoryTheory.AsSmall.down.map f.fiber
• CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).map f).fiber = CategoryTheory.AsSmall.up.map f.fiber
• CategoryTheory.Limits.hasColimitsOfShape_grothendieck 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj X)) H] [CategoryTheory.Limits.HasColimitsOfShape C H] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Grothendieck F) H
• CategoryTheory.Limits.fiberwiseColim 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (H : Type u₂) [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] : CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) (CategoryTheory.Functor C H)
• CategoryTheory.Limits.fiberwiseColim_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (H : Type u₂) [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : (CategoryTheory.Limits.fiberwiseColim F H).obj G = CategoryTheory.Limits.fiberwiseColimit G
• CategoryTheory.Limits.fiberwiseColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] : CategoryTheory.Functor C H
• CategoryTheory.Limits.fiberwiseColimCompColimIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasColimitsOfShape C H] : (CategoryTheory.Limits.fiberwiseColim F H).comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim
• CategoryTheory.Limits.coconeFiberwiseColimitOfCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (c : CategoryTheory.Limits.Cocone G) : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)
• CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)) : CategoryTheory.Limits.Cocone G
• CategoryTheory.Limits.hasColimit_fiberwiseColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit G] : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)
• CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] : CategoryTheory.Limits.HasColimit G
• CategoryTheory.Limits.isColimitCoconeFiberwiseColimitOfCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] {c : CategoryTheory.Limits.Cocone G} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeFiberwiseColimitOfCocone c)
• CategoryTheory.Limits.isColimitCoconeOfFiberwiseCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] {c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit c)
• CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (c : CategoryTheory.Limits.Cocone G) : (CategoryTheory.Limits.coconeFiberwiseColimitOfCocone c).pt = c.pt
• CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)) : (CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit c).pt = c.pt
• CategoryTheory.Limits.colimitFiberwiseColimitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] : CategoryTheory.Limits.colimit (CategoryTheory.Limits.fiberwiseColimit G) ≅ CategoryTheory.Limits.colimit G
• CategoryTheory.Limits.hasColimit_ι_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (X : C) : CategoryTheory.Limits.HasColimit ((CategoryTheory.Grothendieck.ι F X).comp G)
• CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] : G ⟶ (CategoryTheory.Grothendieck.forget F).comp (CategoryTheory.Limits.fiberwiseColimit G)
• CategoryTheory.Limits.fiberwiseColimit_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (X : C) : (CategoryTheory.Limits.fiberwiseColimit G).obj X = CategoryTheory.Limits.colimit ((CategoryTheory.Grothendieck.ι F X).comp G)
• CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit G).app X = CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber
• CategoryTheory.Limits.fiberwiseColimCompEvaluationIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (c : C) : (CategoryTheory.Limits.fiberwiseColim F H).comp ((CategoryTheory.evaluation C H).obj c) ≅ ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj c)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F c)).comp CategoryTheory.Limits.colim
• CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (c : CategoryTheory.Limits.Cocone G) (X : C) : (CategoryTheory.Limits.coconeFiberwiseColimitOfCocone c).ι.app X = CategoryTheory.Limits.colimit.desc ((CategoryTheory.Grothendieck.ι F X).comp G) (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.Grothendieck.ι F X) c)
• CategoryTheory.Limits.fiberwiseColimCompColimIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : CategoryTheory.Limits.fiberwiseColimCompColimIso.hom.app X = (CategoryTheory.Limits.colimitFiberwiseColimitIso X).hom
• CategoryTheory.Limits.fiberwiseColimCompColimIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : CategoryTheory.Limits.fiberwiseColimCompColimIso.inv.app X = (CategoryTheory.Limits.colimitFiberwiseColimitIso X).inv
• CategoryTheory.Limits.fiberwiseColim_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (H : Type u₂) [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} (α : X✝ ⟶ Y✝) (c : C) : ((CategoryTheory.Limits.fiberwiseColim F H).map α).app c = CategoryTheory.Limits.colim.map ((CategoryTheory.Grothendieck.ι F c).whiskerLeft α)
• CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] (X : CategoryTheory.Grothendieck F) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X) (CategoryTheory.Limits.colimitFiberwiseColimitIso G).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber) (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X.base)
• CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] (c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit c).ι.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber) (c.ι.app X.base)
• CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] (X : C) (d : ↑(F.obj X)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X).comp G) d) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X) (CategoryTheory.Limits.colimitFiberwiseColimitIso G).hom) = CategoryTheory.Limits.colimit.ι G { base := X, fiber := d }
• CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] (X : CategoryTheory.Grothendieck F) {Z : H} (h : CategoryTheory.Limits.colimit (CategoryTheory.Limits.fiberwiseColimit G) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFiberwiseColimitIso G).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X.base).comp G) X.fiber) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X.base) h)
• CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] (X : C) (d : ↑(F.obj X)) {Z : H} (h : CategoryTheory.Limits.colimit G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X).comp G) d) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFiberwiseColimitIso G).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G { base := X, fiber := d }) h
• CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (c : C) (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso c).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit ((CategoryTheory.Grothendieck.ι F c).comp X))
• CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] (c : C) (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) : (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso c).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit ((CategoryTheory.Grothendieck.ι F c).comp X))
• CategoryTheory.Limits.fiberwiseColimit_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.fiberwiseColimit G).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Grothendieck.ιNatTrans f) G) ((F.map f).toFunctor.associator (CategoryTheory.Grothendieck.ι F Y) G).hom)) (CategoryTheory.Limits.colimit.pre ((CategoryTheory.Grothendieck.ι F Y).comp G) (F.map f).toFunctor)
• CategoryTheory.Grothendieck.final_pre 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D CategoryTheory.Cat) (G : CategoryTheory.Functor C D) [hG : G.Final] : (CategoryTheory.Grothendieck.pre F G).Final
• CategoryTheory.Grothendieck.final_map 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) [hα : ∀ (X : C), (α.app X).toFunctor.Final] : (CategoryTheory.Grothendieck.map α).Final
• CategoryTheory.Grothendieck.structuredArrowToStructuredArrowPre 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D CategoryTheory.Cat) (G : CategoryTheory.Functor C D) (d : D) (f : ↑(F.obj d)) : CategoryTheory.StructuredArrow d G ⥤q CategoryTheory.StructuredArrow { base := d, fiber := f } (CategoryTheory.Grothendieck.pre F G)
• CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) [∀ (X : C), (α.app X).toFunctor.Final] (H : CategoryTheory.Functor (CategoryTheory.Grothendieck G) (Type u₂)) : CategoryTheory.Limits.fiberwiseColimit ((CategoryTheory.Grothendieck.map α).comp H) ≅ CategoryTheory.Limits.fiberwiseColimit H
• CategoryTheory.CostructuredArrow.grothendieckProj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) C
• CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) : CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)))
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)) ≌ CategoryTheory.Comma L R
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) : CategoryTheory.Functor (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) (CategoryTheory.Comma L R)
• CategoryTheory.CostructuredArrow.grothendieckProj_obj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) : (CategoryTheory.CostructuredArrow.grothendieckProj L).obj X = CategoryTheory.CostructuredArrow.left X.fiber
• CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : CategoryTheory.Comma L R) : ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).obj X).base = X.right
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).right = P.base
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) : (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).functor = CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) : (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).inverse = CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R
• CategoryTheory.CostructuredArrow.ιCompGrothendieckProj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : D) : (CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) X).comp (CategoryTheory.CostructuredArrow.grothendieckProj L) ≅ CategoryTheory.CostructuredArrow.proj L X
• CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) : (CategoryTheory.CostructuredArrow.map f).comp ((CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) Y).comp (CategoryTheory.CostructuredArrow.grothendieckProj L)) ≅ CategoryTheory.CostructuredArrow.proj L X
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).left = CategoryTheory.CostructuredArrow.left P.fiber
• CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : CategoryTheory.Comma L R) : ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).obj X).fiber = CategoryTheory.CostructuredArrow.mk X.hom
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).hom = CategoryTheory.CostructuredArrow.hom P.fiber
• CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) : (CategoryTheory.Grothendieck.ι (R.comp (CategoryTheory.CostructuredArrow.functor L)) X).comp ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).comp (CategoryTheory.Comma.fst L R)) ≅ CategoryTheory.CostructuredArrow.proj L (R.obj X)
• CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).map f).base = f.right
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).map f).right = f.base
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) : (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).comp (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R)).obj x)) ⋯
• CategoryTheory.CostructuredArrow.grothendieckProj_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.grothendieckProj L).map f = f.fiber.left
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) : (CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence L R).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)))).obj x)) ⋯
• CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : D) (X✝ : ↑(((CategoryTheory.Functor.id D).comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) : (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X).hom.app X✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X✝)
• CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) (X : D) (X✝ : ↑(((CategoryTheory.Functor.id D).comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) : (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X).inv.app X✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X✝)
• CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) (X✝ : ↑((R.comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) : (CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).hom.app X✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X✝)
• CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) (X : E) (X✝ : ↑((R.comp (CategoryTheory.CostructuredArrow.functor L)).obj X)) : (CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst L R X).inv.app X✝ = CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X✝)
• CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).map f).left = f.fiber.left
• CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CategoryTheory.CostructuredArrow L X) : (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
• CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CategoryTheory.CostructuredArrow L X) : (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
• CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D) (R : CategoryTheory.Functor E D) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor L R).map f).fiber = CategoryTheory.CostructuredArrow.homMk f.left ⋯
• CategoryTheory.Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape D H] : CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G)
• CategoryTheory.Functor.colimitIsoColimitGrothendieck 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape D H] [CategoryTheory.Limits.HasColimitsOfShape C H] : CategoryTheory.Limits.colimit G ≅ CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G)
• CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] : L.leftKanExtension F ≅ CategoryTheory.Limits.fiberwiseColimit ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp F)
• CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] {X Y : D} (f : X ⟶ Y) : CategoryTheory.Limits.HasColimit (((CategoryTheory.CostructuredArrow.functor L).map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) Y).comp ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp F)))
• CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape D H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X) (L.colimitIsoColimitGrothendieck G).hom = CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) { base := L.obj X, fiber := CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)) }
• CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape D H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) X) (L.colimitIsoColimitGrothendieck G).inv = CategoryTheory.Limits.colimit.ι G ((CategoryTheory.CostructuredArrow.proj L X.base).obj X.fiber)
• CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom_assoc 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape D H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : C) {Z : H} (h : CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G X) (CategoryTheory.CategoryStruct.comp (L.colimitIsoColimitGrothendieck G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) { base := L.obj X, fiber := CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)) }) h
• CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension G] [CategoryTheory.Limits.HasColimitsOfShape D H] [CategoryTheory.Limits.HasColimitsOfShape C H] (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)) {Z : H} (h : CategoryTheory.Limits.colimit G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) X) (CategoryTheory.CategoryStruct.comp (L.colimitIsoColimitGrothendieck G).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G ((CategoryTheory.CostructuredArrow.proj L X.base).obj X.fiber)) h
• CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] (X : D) : (L.leftKanExtensionIsoFiberwiseColimit F).hom.app X = CategoryTheory.CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F X).hom (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X) F)).inv
• CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] [L.HasLeftKanExtension F] (X : D) : (L.leftKanExtensionIsoFiberwiseColimit F).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X) F)).hom (L.leftKanExtensionObjIsoColimit F X).inv
• CategoryTheory.Limits.preservesLimitsOfShape_colim_grothendieck 📋 Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] (F : CategoryTheory.Functor C CategoryTheory.Cat) [CategoryTheory.Limits.HasColimitsOfShape C H] [CategoryTheory.Limits.HasLimitsOfShape J H] [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] : CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
• CategoryTheory.Limits.fiberwiseColimitLimitIso 📋 Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat} (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)) [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasLimitsOfShape J H] [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] : CategoryTheory.Limits.fiberwiseColimit (CategoryTheory.Limits.limit K) ≅ CategoryTheory.Limits.limit (K.comp (CategoryTheory.Limits.fiberwiseColim F H))
• CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat} (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)) [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasLimitsOfShape J H] [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (X : C) : (CategoryTheory.Limits.fiberwiseColimitLimitIso K).inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (K.comp (CategoryTheory.Limits.fiberwiseColim F H)) X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso (K.associator ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F X)) CategoryTheory.Limits.colim ≪≫ K.isoWhiskerLeft (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso X).symm ≪≫ (K.associator (CategoryTheory.Limits.fiberwiseColim F H) ((CategoryTheory.evaluation C H).obj X)).symm)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso CategoryTheory.Limits.colim (K.comp ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F X)))).inv (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit K (CategoryTheory.Grothendieck.ι F X)).symm).inv))
• CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] {J : Type u₃} [CategoryTheory.Category.{v₃, u₃} J] {F : CategoryTheory.Functor C CategoryTheory.Cat} (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)) [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] [CategoryTheory.Limits.HasLimitsOfShape J H] [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] (X : C) : (CategoryTheory.Limits.fiberwiseColimitLimitIso K).hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit K (CategoryTheory.Grothendieck.ι F X)).symm).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso CategoryTheory.Limits.colim (K.comp ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F X)))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso (K.associator ((CategoryTheory.Functor.whiskeringLeft (↑(F.obj X)) (CategoryTheory.Grothendieck F) H).obj (CategoryTheory.Grothendieck.ι F X)) CategoryTheory.Limits.colim ≪≫ K.isoWhiskerLeft (CategoryTheory.Limits.fiberwiseColimCompEvaluationIso X).symm ≪≫ (K.associator (CategoryTheory.Limits.fiberwiseColim F H) ((CategoryTheory.evaluation C H).obj X)).symm)).hom (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (K.comp (CategoryTheory.Limits.fiberwiseColim F H)) X).inv))
• CategoryTheory.instIsFilteredGrothendieckOfαCategoryObjCat 📋 Mathlib.CategoryTheory.Filtered.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) [CategoryTheory.IsFiltered C] [∀ (c : C), CategoryTheory.IsFiltered ↑(F.obj c)] : CategoryTheory.IsFiltered (CategoryTheory.Grothendieck F)
• CategoryTheory.instIsFilteredOrEmptyGrothendieckOfαCategoryObjCat 📋 Mathlib.CategoryTheory.Filtered.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) [CategoryTheory.IsFilteredOrEmpty C] [∀ (c : C), CategoryTheory.IsFilteredOrEmpty ↑(F.obj c)] : CategoryTheory.IsFilteredOrEmpty (CategoryTheory.Grothendieck F)

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