Loogle!

Result

Found 31 declarations mentioning CategoryTheory.Grothendieck.map.

• 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.CategoryStruct.id (CategoryTheory.Cat.of (CategoryTheory.Grothendieck F))
• 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) ≅ CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (CategoryTheory.Grothendieck 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.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.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.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.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.whiskerRight α.hom F)).comp (CategoryTheory.Grothendieck.pre F H)
• 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 (CategoryTheory.whiskerLeft G α)).comp (CategoryTheory.Grothendieck.pre H G)
• CategoryTheory.Grothendieck.preInv.eq_1 📋 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.preInv F G = (CategoryTheory.Grothendieck.map (CategoryTheory.whiskerRight G.counitInv F)).comp (CategoryTheory.Grothendieck.pre (G.functor.comp F) G.inverse)
• 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.{u_2, u_1} E] (K : CategoryTheory.Functor (CategoryTheory.Grothendieck H) E) : (CategoryTheory.Grothendieck.pre F G).comp ((CategoryTheory.Grothendieck.map α).comp K) = (CategoryTheory.Grothendieck.map (CategoryTheory.whiskerLeft G α)).comp ((CategoryTheory.Grothendieck.pre H G).comp K)
• 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 α) ≅ CategoryTheory.Functor.comp (α.app c) (CategoryTheory.Grothendieck.ι F' c)
• 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.whiskerRight α CategoryTheory.Cat.asSmallFunctor) ≅ (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).functor.comp ((CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence G).inverse)
• 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).obj X.fiber }
• 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.whiskerRight G.unitInv (G.functor.comp F)) ≅ CategoryTheory.Grothendieck.pre (G.functor.comp F) (G.functor.comp G.inverse)
• 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).obj X.fiber
• 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 (CategoryTheory.whiskerLeft G.functor α) ≅ (CategoryTheory.Grothendieck.preEquivalence F G).functor.comp ((CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.preEquivalence F' G).inverse)
• CategoryTheory.Grothendieck.preNatIso.eq_1 📋 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.preNatIso F α = CategoryTheory.NatIso.ofComponents (fun X => ({ base := G.obj X.base, fiber := X.fiber }.transportIso (α.app X.base)).symm) ⋯
• 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.preUnitIso.eq_1 📋 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.preUnitIso F G = (CategoryTheory.Grothendieck.preNatIso (G.functor.comp F) G.unitIso.symm).symm
• 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.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 ⋯).app X.fiber) ((α.app 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.map.eq_1 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) : CategoryTheory.Grothendieck.map α = { obj := fun X => { base := X.base, fiber := (α.app X.base).obj X.fiber }, map := fun {X Y} f => { base := f.base, fiber := CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).app X.fiber) ((α.app Y.base).map f.fiber) }, map_id := ⋯, map_comp := ⋯ }
• 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).map f.fiber)
• 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), CategoryTheory.Functor.Final (α.app X)] : (CategoryTheory.Grothendieck.map α).Final
• 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), CategoryTheory.Functor.Final (α.app X)] (H : CategoryTheory.Functor (CategoryTheory.Grothendieck G) (Type u₂)) : CategoryTheory.Limits.fiberwiseColimit ((CategoryTheory.Grothendieck.map α).comp H) ≅ CategoryTheory.Limits.fiberwiseColimit H
• CategoryTheory.Grothendieck.ιCompMap.eq_1 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) : CategoryTheory.Grothendieck.ιCompMap α c = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl (((CategoryTheory.Grothendieck.ι F c).comp (CategoryTheory.Grothendieck.map α)).obj X)) ⋯
• CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence.eq_1 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) [∀ (X : C), CategoryTheory.Functor.Final (α.app X)] (H : CategoryTheory.Functor (CategoryTheory.Grothendieck G) (Type u₂)) : CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence α H = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Limits.HasColimit.isoOfNatIso (((CategoryTheory.Grothendieck.ι F X).associator (CategoryTheory.Grothendieck.map α) H).symm ≪≫ CategoryTheory.isoWhiskerRight (CategoryTheory.Grothendieck.ιCompMap α X) H ≪≫ CategoryTheory.Functor.associator (α.app X) (CategoryTheory.Grothendieck.ι G X) H) ≪≫ CategoryTheory.Functor.Final.colimitIso (α.app X) ((CategoryTheory.Grothendieck.ι G X).comp H)) ⋯

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 19971e9 serving mathlib revision 40fea08