Loogle!
Result
Found 425 declarations mentioning CategoryTheory.LocallyDiscrete. Of these, only the first 200 are shown.
- CategoryTheory.LocallyDiscrete 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
(C : Type u) : Type u - CategoryTheory.LocallyDiscrete.as 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} (self : CategoryTheory.LocallyDiscrete C) : C - CategoryTheory.LocallyDiscrete.mk 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} (as : C) : CategoryTheory.LocallyDiscrete C - CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} : CategoryTheory.LocallyDiscrete C ≃ C - CategoryTheory.locallyDiscreteBicategory 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
(C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Bicategory (CategoryTheory.LocallyDiscrete C) - CategoryTheory.LocallyDiscrete.categoryStruct 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] : CategoryTheory.CategoryStruct.{v, u} (CategoryTheory.LocallyDiscrete C) - CategoryTheory.LocallyDiscrete.instDecidableEq 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [DecidableEq C] : DecidableEq (CategoryTheory.LocallyDiscrete C) - CategoryTheory.LocallyDiscrete.instInhabited 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [Inhabited C] : Inhabited (CategoryTheory.LocallyDiscrete C) - CategoryTheory.Bicategory.instIsLocallyDiscreteLocallyDiscrete 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] : CategoryTheory.Bicategory.IsLocallyDiscrete (CategoryTheory.LocallyDiscrete C) - CategoryTheory.locallyDiscreteBicategory.strict 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
(C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Bicategory.Strict (CategoryTheory.LocallyDiscrete C) - CategoryTheory.LocallyDiscrete.mk_as 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} (a : CategoryTheory.LocallyDiscrete C) : { as := a.as } = a - CategoryTheory.LocallyDiscrete.ext 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} {x y : CategoryTheory.LocallyDiscrete C} (as : x.as = y.as) : x = y - CategoryTheory.LocallyDiscrete.ext_iff 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} {x y : CategoryTheory.LocallyDiscrete C} : x = y ↔ x.as = y.as - CategoryTheory.LocallyDiscrete.homSmallCategory 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (a b : CategoryTheory.LocallyDiscrete C) : CategoryTheory.SmallCategory (a ⟶ b) - Quiver.Hom.toLoc 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a b : C} (f : a ⟶ b) : { as := a } ⟶ { as := b } - CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_apply 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} (self : CategoryTheory.LocallyDiscrete C) : CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv self = self.as - CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_symm_apply_as 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} (as : C) : (CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv.symm as).as = as - Quiver.Hom.id_toLoc 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (a : C) : (CategoryTheory.CategoryStruct.id a).toLoc = CategoryTheory.CategoryStruct.id { as := a } - CategoryTheory.LocallyDiscrete.id_as 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (a : CategoryTheory.LocallyDiscrete C) : (CategoryTheory.CategoryStruct.id a).as = CategoryTheory.CategoryStruct.id a.as - CategoryTheory.LocallyDiscrete.eqToHom_toLoc 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.Category.{v, u} C] {a b : C} (h : a = b) : (CategoryTheory.eqToHom h).toLoc = CategoryTheory.eqToHom ⋯ - CategoryTheory.LocallyDiscrete.subsingleton2Hom 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a b : CategoryTheory.LocallyDiscrete C} (f g : a ⟶ b) : Subsingleton (f ⟶ g) - Quiver.Hom.comp_toLoc 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a b c : C} (f : a ⟶ b) (g : b ⟶ c) : (CategoryTheory.CategoryStruct.comp f g).toLoc = CategoryTheory.CategoryStruct.comp f.toLoc g.toLoc - CategoryTheory.LocallyDiscrete.eq_of_hom 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X Y : CategoryTheory.LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : f = g - CategoryTheory.LocallyDiscrete.comp_as 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a b c : CategoryTheory.LocallyDiscrete C} (f : a ⟶ b) (g : b ⟶ c) : (CategoryTheory.CategoryStruct.comp f g).as = CategoryTheory.CategoryStruct.comp f.as g.as - CategoryTheory.CommSq.toLoc 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (h : CategoryTheory.CommSq t l r b) : CategoryTheory.CommSq t.toLoc l.toLoc r.toLoc b.toLoc - CategoryTheory.Functor.toOplaxFunctor 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete C) (CategoryTheory.LocallyDiscrete D) - CategoryTheory.Functor.toPseudofunctor 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete C) (CategoryTheory.LocallyDiscrete D) - CategoryTheory.Functor.toOplaxFunctor' 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete I) B - CategoryTheory.Functor.toPseudofunctor' 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete I) B - CategoryTheory.Functor.toPseudofunctor'_obj 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) : F.toPseudofunctor'.obj x✝ = F.obj x✝.as - CategoryTheory.Functor.toPseudofunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (x✝ : CategoryTheory.LocallyDiscrete C) : F.toPseudofunctor.obj x✝ = { as := F.obj x✝.as } - CategoryTheory.Functor.toOplaxFunctor'_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {X✝ Y✝ : CategoryTheory.LocallyDiscrete I} (x✝ : X✝ ⟶ Y✝) : F.toOplaxFunctor'.map x✝ = match x✝ with | { as := f } => F.map f - CategoryTheory.Functor.toPseudofunctor'_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {X✝ Y✝ : CategoryTheory.LocallyDiscrete I} (x✝ : X✝ ⟶ Y✝) : F.toPseudofunctor'.map x✝ = match x✝ with | { as := f } => F.map f - CategoryTheory.Functor.toOplaxFunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.LocallyDiscrete C} (x✝ : X✝ ⟶ Y✝) : F.toOplaxFunctor.map x✝ = match x✝ with | { as := f } => (F.map f).toLoc - CategoryTheory.Functor.toPseudofunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.LocallyDiscrete C} (x✝ : X✝ ⟶ Y✝) : F.toPseudofunctor.map x✝ = match x✝ with | { as := f } => (F.map f).toLoc - CategoryTheory.Functor.toPseudofunctor'_mapId 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) : F.toPseudofunctor'.mapId x✝ = CategoryTheory.eqToIso ⋯ - CategoryTheory.Functor.toPseudofunctor_mapId 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (x✝ : CategoryTheory.LocallyDiscrete C) : F.toPseudofunctor.mapId x✝ = CategoryTheory.eqToIso ⋯ - CategoryTheory.Functor.toPseudofunctor'_mapComp 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete I} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toPseudofunctor'.mapComp f g = CategoryTheory.eqToIso ⋯ - CategoryTheory.Functor.toPseudofunctor_mapComp 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete C} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : F.toPseudofunctor.mapComp x✝ x✝¹ = match x✝ with | { as := f } => match x✝¹ with | { as := g } => CategoryTheory.eqToIso ⋯ - CategoryTheory.LocallyDiscrete.mkPseudofunctor 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete B₀) C - CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapId 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (x✝ : CategoryTheory.LocallyDiscrete B₀) : (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapId x✝ = mapId x✝.as - CategoryTheory.LocallyDiscrete.mkPseudofunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (b : CategoryTheory.LocallyDiscrete B₀) : (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).obj b = obj b.as - CategoryTheory.LocallyDiscrete.mkPseudofunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) {X✝ Y✝ : CategoryTheory.LocallyDiscrete B₀} (f : X✝ ⟶ Y✝) : (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).map f = map f.as - CategoryTheory.LocallyDiscrete.mkPseudofunctor_mapComp 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
{B₀ : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} B₀] [CategoryTheory.Bicategory C] (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) (mapId : (b : B₀) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b)) (mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g)) (map₂_associator : ∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv) (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_left_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f)) (CategoryTheory.Bicategory.leftUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) (map₂_right_unitor : ∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (map f)).hom) = CategoryTheory.eqToHom ⋯ := by cat_disch) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete B₀} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (CategoryTheory.LocallyDiscrete.mkPseudofunctor obj map mapId mapComp map₂_associator map₂_left_unitor map₂_right_unitor).mapComp x✝ x✝¹ = mapComp x✝.as x✝¹.as - CommRingCat.moduleCatExtendScalarsPseudofunctor 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
: CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete CommRingCat) CategoryTheory.Cat - CommRingCat.moduleCatRestrictScalarsPseudofunctor 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
: CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ) CategoryTheory.Cat - RingCat.moduleCatRestrictScalarsPseudofunctor 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
: CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete RingCatᵒᵖ) CategoryTheory.Cat - CommRingCat.moduleCatExtendScalarsPseudofunctor_obj 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
(b : CategoryTheory.LocallyDiscrete CommRingCat) : CommRingCat.moduleCatExtendScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑b.as) - RingCat.moduleCatRestrictScalarsPseudofunctor_obj 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
(b : CategoryTheory.LocallyDiscrete RingCatᵒᵖ) : RingCat.moduleCatRestrictScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑(Opposite.unop b.as)) - CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
(b : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑(Opposite.unop b.as)) - CommRingCat.moduleCatExtendScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
{X✝ Y✝ : CategoryTheory.LocallyDiscrete CommRingCat} (f : X✝ ⟶ Y✝) : CommRingCat.moduleCatExtendScalarsPseudofunctor.map f = (ModuleCat.extendScalars (CommRingCat.Hom.hom f.as)).toCatHom - RingCat.moduleCatRestrictScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
{X✝ Y✝ : CategoryTheory.LocallyDiscrete RingCatᵒᵖ} (f : X✝ ⟶ Y✝) : RingCat.moduleCatRestrictScalarsPseudofunctor.map f = (ModuleCat.restrictScalars (RingCat.Hom.hom f.as.unop)).toCatHom - CommRingCat.moduleCatRestrictScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
{X✝ Y✝ : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.map f = (ModuleCat.restrictScalars (CommRingCat.Hom.hom f.as.unop)).toCatHom - CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
(x✝ : CategoryTheory.LocallyDiscrete CommRingCat) : CommRingCat.moduleCatExtendScalarsPseudofunctor.mapId x✝ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.extendScalarsId ↑x✝.as) - RingCat.moduleCatRestrictScalarsPseudofunctor_mapId 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
(x✝ : CategoryTheory.LocallyDiscrete RingCatᵒᵖ) : RingCat.moduleCatRestrictScalarsPseudofunctor.mapId x✝ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsId ↑(Opposite.unop x✝.as)) - CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
(x✝ : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.mapId x✝ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsId ↑(Opposite.unop x✝.as)) - CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
{a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete CommRingCat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CommRingCat.moduleCatExtendScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom x✝.as) (CommRingCat.Hom.hom x✝¹.as)) - RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
{a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete RingCatᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : RingCat.moduleCatRestrictScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsComp (RingCat.Hom.hom x✝¹.as.unop) (RingCat.Hom.hom x✝.as.unop)) - CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
{a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom x✝¹.as.unop) (CommRingCat.Hom.hom x✝.as.unop)) - AlgebraicGeometry.Scheme.Modules.pseudofunctor 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
: CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) (CategoryTheory.Bicategory.Adj CategoryTheory.Cat) - AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
(b : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.obj b).obj = CategoryTheory.Cat.of (Opposite.unop b.as).Modules - AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).l = (AlgebraicGeometry.Scheme.Modules.pullback f.as.unop).toCatHom - AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).r = (AlgebraicGeometry.Scheme.Modules.pushforward f.as.unop).toCatHom - AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).adj = (AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f.as.unop).toCat - AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
(x✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x✝).hom.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackId (Opposite.unop x✝.as)).hom - AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
(x✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x✝).inv.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackId (Opposite.unop x✝.as)).inv - AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
(x✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x✝).hom.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardId (Opposite.unop x✝.as)).inv - AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
(x✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x✝).inv.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardId (Opposite.unop x✝.as)).hom - AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).hom.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackComp x✝¹.as.unop x✝.as.unop).inv - AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).inv.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackComp x✝¹.as.unop x✝.as.unop).hom - AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).hom.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardComp x✝¹.as.unop x✝.as.unop).hom - AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).inv.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardComp x✝¹.as.unop x✝.as.unop).inv - CategoryTheory.FreeBicategory.inclusion 📋 Mathlib.CategoryTheory.Bicategory.Coherence
(B : Type u) [Quiver B] : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Paths B)) (CategoryTheory.FreeBicategory B) - CategoryTheory.FreeBicategory.normalize 📋 Mathlib.CategoryTheory.Bicategory.Coherence
(B : Type u) [Quiver B] : CategoryTheory.Pseudofunctor (CategoryTheory.FreeBicategory B) (CategoryTheory.LocallyDiscrete (CategoryTheory.Paths B)) - CategoryTheory.FreeBicategory.preinclusion 📋 Mathlib.CategoryTheory.Bicategory.Coherence
(B : Type u) [Quiver B] : CategoryTheory.PrelaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Paths B)) (CategoryTheory.FreeBicategory B) - CategoryTheory.FreeBicategory.preinclusion_obj 📋 Mathlib.CategoryTheory.Bicategory.Coherence
{B : Type u} [Quiver B] (a : B) : (CategoryTheory.FreeBicategory.preinclusion B).obj { as := a } = a - CategoryTheory.FreeBicategory.normalizeUnitIso 📋 Mathlib.CategoryTheory.Bicategory.Coherence
{B : Type u} [Quiver B] (a b : CategoryTheory.FreeBicategory B) : CategoryTheory.Functor.id (a ⟶ b) ≅ ((CategoryTheory.FreeBicategory.normalize B).mapFunctor a b).comp (CategoryTheory.FreeBicategory.inclusionPath a b) - CategoryTheory.FreeBicategory.normalizeIso 📋 Mathlib.CategoryTheory.Bicategory.Coherence
{B : Type u} [Quiver B] {a b c : B} (p : Quiver.Path a b) (f : CategoryTheory.FreeBicategory.Hom b c) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) f ≅ (CategoryTheory.FreeBicategory.preinclusion B).map { as := CategoryTheory.FreeBicategory.normalizeAux p f } - CategoryTheory.FreeBicategory.normalizeIso_id 📋 Mathlib.CategoryTheory.Bicategory.Coherence
{B : Type u} [Quiver B] {a : B} {b : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b) : CategoryTheory.FreeBicategory.normalizeIso p (CategoryTheory.CategoryStruct.id b) = CategoryTheory.Bicategory.rightUnitor ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) - CategoryTheory.FreeBicategory.inclusionMapCompAux 📋 Mathlib.CategoryTheory.Bicategory.Coherence
{B : Type u} [Quiver B] {a b c : B} (f : Quiver.Path a b) (g : Quiver.Path b c) : (CategoryTheory.FreeBicategory.preinclusion B).map (CategoryTheory.CategoryStruct.comp { as := f } { as := g }) ≅ CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := f }) ((CategoryTheory.FreeBicategory.preinclusion B).map { as := g }) - CategoryTheory.FreeBicategory.preinclusion_map₂ 📋 Mathlib.CategoryTheory.Bicategory.Coherence
{B : Type u} [Quiver B] {a b : B} (f g : CategoryTheory.Discrete (Quiver.Path a b)) (η : f ⟶ g) : (CategoryTheory.FreeBicategory.preinclusion B).map₂ η = CategoryTheory.eqToHom ⋯ - CategoryTheory.FreeBicategory.normalize_naturality 📋 Mathlib.CategoryTheory.Bicategory.Coherence
{B : Type u} [Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : CategoryTheory.FreeBicategory.Hom b c} (η : f ⟶ g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) η) (CategoryTheory.FreeBicategory.normalizeIso p g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.normalizeIso p f).hom ((CategoryTheory.FreeBicategory.preinclusion B).map₂ (CategoryTheory.eqToHom ⋯)) - CategoryTheory.FreeBicategory.normalizeIso_comp 📋 Mathlib.CategoryTheory.Bicategory.Coherence
{B : Type u} [Quiver B] {a : B} {b c d : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b) (f : b ⟶ c) (g : c ⟶ d) : CategoryTheory.FreeBicategory.normalizeIso p (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.Bicategory.associator ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) f g).symm ≪≫ CategoryTheory.Bicategory.whiskerRightIso (CategoryTheory.FreeBicategory.normalizeIso p f) g ≪≫ CategoryTheory.FreeBicategory.normalizeIso (CategoryTheory.FreeBicategory.normalizeAux p f) g - CategoryTheory.Pseudofunctor.Grothendieck 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) : Type (max u₁ u₂) - CategoryTheory.Pseudofunctor.CoGrothendieck 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) : Type (max u₁ u₂) - CategoryTheory.Pseudofunctor.Grothendieck.base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (self : F.Grothendieck) : 𝒮 - CategoryTheory.Pseudofunctor.Grothendieck.category 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} : CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} F.Grothendieck - CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} : CategoryTheory.CategoryStruct.{max v₂ v₁, max u₂ u₁} F.Grothendieck - CategoryTheory.Pseudofunctor.CoGrothendieck.base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (self : F.CoGrothendieck) : 𝒮 - CategoryTheory.Pseudofunctor.CoGrothendieck.category 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} : CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} F.CoGrothendieck - CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} : CategoryTheory.CategoryStruct.{max v₂ v₁, max u₂ u₁} F.CoGrothendieck - CategoryTheory.Pseudofunctor.Grothendieck.Hom 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (X Y : F.Grothendieck) : Type (max v₁ v₂) - CategoryTheory.Pseudofunctor.Grothendieck.forget 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) : CategoryTheory.Functor F.Grothendieck 𝒮 - CategoryTheory.Pseudofunctor.Grothendieck.instInhabitedHom 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (X : F.Grothendieck) : Inhabited (X.Hom X) - CategoryTheory.Pseudofunctor.CoGrothendieck.Hom 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X Y : F.CoGrothendieck) : Type (max v₁ v₂) - CategoryTheory.Pseudofunctor.CoGrothendieck.forget 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) : CategoryTheory.Functor F.CoGrothendieck 𝒮 - CategoryTheory.Pseudofunctor.CoGrothendieck.instInhabitedHom 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.CoGrothendieck) : Inhabited (X.Hom X) - CategoryTheory.Pseudofunctor.Grothendieck.forget_obj 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) (X : F.Grothendieck) : (CategoryTheory.Pseudofunctor.Grothendieck.forget F).obj X = X.base - CategoryTheory.Pseudofunctor.CoGrothendieck.forget_obj 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (X : F.CoGrothendieck) : (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).obj X = X.base - CategoryTheory.Pseudofunctor.Grothendieck.Hom.base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X Y : F.Grothendieck} (self : X.Hom Y) : X.base ⟶ Y.base - CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {X Y : F.CoGrothendieck} (self : X.Hom Y) : X.base ⟶ Y.base - CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (X : F.Grothendieck) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base - CategoryTheory.Pseudofunctor.Grothendieck.map_id_eq 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) : CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.id F) = CategoryTheory.Functor.id F.Grothendieck - CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.CoGrothendieck) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base - CategoryTheory.Pseudofunctor.Grothendieck.map 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) : CategoryTheory.Functor F.Grothendieck G.Grothendieck - CategoryTheory.Pseudofunctor.CoGrothendieck.map_id_eq 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) : CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.id F) = CategoryTheory.Functor.id F.CoGrothendieck - CategoryTheory.Pseudofunctor.Grothendieck.mapIdIso 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) : CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.id F) ≅ CategoryTheory.Functor.id F.Grothendieck - CategoryTheory.Pseudofunctor.Grothendieck.forget_map 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) {X✝ Y✝ : F.Grothendieck} (f : X✝ ⟶ Y✝) : (CategoryTheory.Pseudofunctor.Grothendieck.forget F).map f = f.base - CategoryTheory.Pseudofunctor.CoGrothendieck.map 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G) : CategoryTheory.Functor F.CoGrothendieck G.CoGrothendieck - CategoryTheory.Pseudofunctor.Grothendieck.map_obj_base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) (a : F.Grothendieck) : ((CategoryTheory.Pseudofunctor.Grothendieck.map α).obj a).base = a.base - CategoryTheory.Pseudofunctor.CoGrothendieck.forget_map 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) {X✝ Y✝ : F.CoGrothendieck} (f : X✝ ⟶ Y✝) : (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).map f = f.base - CategoryTheory.Pseudofunctor.CoGrothendieck.mapIdIso 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) : CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.id F) ≅ CategoryTheory.Functor.id F.CoGrothendieck - CategoryTheory.Pseudofunctor.Grothendieck.map_comp_forget 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) : (CategoryTheory.Pseudofunctor.Grothendieck.map α).comp (CategoryTheory.Pseudofunctor.Grothendieck.forget G) = CategoryTheory.Pseudofunctor.Grothendieck.forget F - CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G) (a : F.CoGrothendieck) : ((CategoryTheory.Pseudofunctor.CoGrothendieck.map α).obj a).base = a.base - CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X x✝ x✝¹ : F.Grothendieck} (f : X.Hom x✝) (g : x✝.Hom x✝¹) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base - CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x✝ x✝¹ Z : F.CoGrothendieck} (f : x✝.Hom x✝¹) (g : x✝¹.Hom Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base - CategoryTheory.Pseudofunctor.CoGrothendieck.map_comp_forget 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G) : (CategoryTheory.Pseudofunctor.CoGrothendieck.map α).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.forget G) = CategoryTheory.Pseudofunctor.CoGrothendieck.forget F - CategoryTheory.Pseudofunctor.Grothendieck.mk 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (base : 𝒮) (fiber : ↑(F.obj { as := base })) : F.Grothendieck - CategoryTheory.Pseudofunctor.Grothendieck.fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (self : F.Grothendieck) : ↑(F.obj { as := self.base }) - CategoryTheory.Pseudofunctor.Grothendieck.map_comp_eq 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.Pseudofunctor.Grothendieck.map α).comp (CategoryTheory.Pseudofunctor.Grothendieck.map β) - CategoryTheory.Pseudofunctor.Grothendieck.map_id_map 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {x y : F.Grothendieck} (f : x ⟶ y) : (CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.id F)).map f = f - CategoryTheory.Pseudofunctor.Grothendieck.mapCompIso 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) ≅ (CategoryTheory.Pseudofunctor.Grothendieck.map α).comp (CategoryTheory.Pseudofunctor.Grothendieck.map β) - CategoryTheory.Pseudofunctor.CoGrothendieck.mk 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (base : 𝒮) (fiber : ↑(F.obj { as := Opposite.op base })) : F.CoGrothendieck - CategoryTheory.Pseudofunctor.CoGrothendieck.fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (self : F.CoGrothendieck) : ↑(F.obj { as := Opposite.op self.base }) - CategoryTheory.Pseudofunctor.CoGrothendieck.map_comp_eq 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.Pseudofunctor.CoGrothendieck.map α).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.map β) - CategoryTheory.Pseudofunctor.CoGrothendieck.map_id_map 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x y : F.CoGrothendieck} (f : x ⟶ y) : (CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.id F)).map f = f - CategoryTheory.Pseudofunctor.CoGrothendieck.mapCompIso 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.comp α β) ≅ (CategoryTheory.Pseudofunctor.CoGrothendieck.map α).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.map β) - CategoryTheory.Pseudofunctor.Grothendieck.ext 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} 𝒮} {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {x y : F.Grothendieck} (base : x.base = y.base) (fiber : x.fiber ≍ y.fiber) : x = y - CategoryTheory.Pseudofunctor.Grothendieck.ext_iff 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} 𝒮} {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {x y : F.Grothendieck} : x = y ↔ x.base = y.base ∧ x.fiber ≍ y.fiber - CategoryTheory.Pseudofunctor.CoGrothendieck.ext 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} 𝒮} {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x y : F.CoGrothendieck} (base : x.base = y.base) (fiber : x.fiber ≍ y.fiber) : x = y - CategoryTheory.Pseudofunctor.CoGrothendieck.ext_iff 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} 𝒮} {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x y : F.CoGrothendieck} : x = y ↔ x.base = y.base ∧ x.fiber ≍ y.fiber - CategoryTheory.Pseudofunctor.Grothendieck.map_obj_fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) (a : F.Grothendieck) : ((CategoryTheory.Pseudofunctor.Grothendieck.map α).obj a).fiber = (α.app { as := a.base }).toFunctor.obj a.fiber - CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G) (a : F.CoGrothendieck) : ((CategoryTheory.Pseudofunctor.CoGrothendieck.map α).obj a).fiber = (α.app { as := Opposite.op a.base }).toFunctor.obj a.fiber - CategoryTheory.Pseudofunctor.Grothendieck.Hom.fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X Y : F.Grothendieck} (self : X.Hom Y) : (F.map self.base.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber - CategoryTheory.Pseudofunctor.Grothendieck.Hom.mk 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X Y : F.Grothendieck} (base : X.base ⟶ Y.base) (fiber : (F.map base.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber) : X.Hom Y - CategoryTheory.Pseudofunctor.Grothendieck.map_map_base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) {a b : F.Grothendieck} (f : a ⟶ b) : ((CategoryTheory.Pseudofunctor.Grothendieck.map α).map f).base = f.base - CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {X Y : F.CoGrothendieck} (self : X.Hom Y) : X.fiber ⟶ (F.map self.base.op.toLoc).toFunctor.obj Y.fiber - CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.mk 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {X Y : F.CoGrothendieck} (base : X.base ⟶ Y.base) (fiber : X.fiber ⟶ (F.map base.op.toLoc).toFunctor.obj Y.fiber) : X.Hom Y - CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G) {a b : F.CoGrothendieck} (f : a ⟶ b) : ((CategoryTheory.Pseudofunctor.CoGrothendieck.map α).map f).base = f.base - CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (X : F.Grothendieck) : (CategoryTheory.CategoryStruct.id X).fiber = (F.mapId { as := X.base }).hom.toNatTrans.app X.fiber - CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.CoGrothendieck) : (CategoryTheory.CategoryStruct.id X).fiber = (F.mapId { as := Opposite.op X.base }).inv.toNatTrans.app X.fiber - CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {a b : F.Grothendieck} {f g : a ⟶ b} (h : f = g) : f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber - CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {a b : F.Grothendieck} (f g : a ⟶ b) (hfg₁ : f.base = g.base) (hfg₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber) : f = g - CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {a b : F.Grothendieck} (f g : a ⟶ b) : f = g ↔ ∃ (hfg : f.base = g.base), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber - CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a b : F.CoGrothendieck} {f g : a ⟶ b} (h : f = g) : f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯) - CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a b : F.CoGrothendieck} (f g : a ⟶ b) (hfg₁ : f.base = g.base) (hfg₂ : f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯)) : f = g - CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a b : F.CoGrothendieck} (f g : a ⟶ b) : f = g ↔ ∃ (hfg : f.base = g.base), f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯) - CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {X x✝ x✝¹ : F.Grothendieck} (f : X.Hom x✝) (g : x✝.Hom x✝¹) : (CategoryTheory.CategoryStruct.comp f g).fiber = CategoryTheory.CategoryStruct.comp ((F.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app X.fiber) (CategoryTheory.CategoryStruct.comp ((F.map g.base.toLoc).toFunctor.map f.fiber) g.fiber) - CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x✝ x✝¹ Z : F.CoGrothendieck} (f : x✝.Hom x✝¹) (g : x✝¹.Hom Z) : (CategoryTheory.CategoryStruct.comp f g).fiber = CategoryTheory.CategoryStruct.comp f.fiber (CategoryTheory.CategoryStruct.comp ((F.map f.base.op.toLoc).toFunctor.map g.fiber) ((F.mapComp g.base.op.toLoc f.base.op.toLoc).inv.toNatTrans.app Z.fiber)) - CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) {a b : F.Grothendieck} (f : a ⟶ b) : ((CategoryTheory.Pseudofunctor.Grothendieck.map α).map f).fiber = CategoryTheory.CategoryStruct.comp ((α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber) ((α.app { as := b.base }).toFunctor.map f.fiber) - CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber 📋 Mathlib.CategoryTheory.Bicategory.Grothendieck
{𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G) {a b : F.CoGrothendieck} (f : a ⟶ b) : ((CategoryTheory.Pseudofunctor.CoGrothendieck.map α).map f).fiber = CategoryTheory.CategoryStruct.comp ((α.app { as := Opposite.op a.base }).toFunctor.map f.fiber) ((α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber) - CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.toOplax 📋 Mathlib.CategoryTheory.Bicategory.Monad.Basic
{B : Type u} [CategoryTheory.Bicategory B] (m : CategoryTheory.Bicategory.OplaxTrans.ComonadBicat B) : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete PUnit.{1})) B - CategoryTheory.Bicategory.Comonad.toOplax 📋 Mathlib.CategoryTheory.Bicategory.Monad.Basic
{B : Type u} [CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [CategoryTheory.Bicategory.Comonad t] : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete Unit)) B - CategoryTheory.Bicategory.Comonad.ofOplaxFromUnit 📋 Mathlib.CategoryTheory.Bicategory.Monad.Basic
{B : Type u} [CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete Unit)) B) : CategoryTheory.Bicategory.Comonad (F.map (CategoryTheory.CategoryStruct.id { as := { as := () } })) - CategoryTheory.RetractArrow.toLoc 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : CategoryTheory.Bicategory.RetractArrow₁ f'.toLoc f.toLoc - CategoryTheory.RetractArrow.toLoc_i₁ 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : r.toLoc.i₁ = (CategoryTheory.Arrow.Hom.left r.i).toLoc - CategoryTheory.RetractArrow.toLoc_i₂ 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : r.toLoc.i₂ = (CategoryTheory.Arrow.Hom.right r.i).toLoc - CategoryTheory.RetractArrow.toLoc_r₁ 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : r.toLoc.r₁ = (CategoryTheory.Arrow.Hom.left r.r).toLoc - CategoryTheory.RetractArrow.toLoc_r₂ 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : r.toLoc.r₂ = (CategoryTheory.Arrow.Hom.right r.r).toLoc - CategoryTheory.RetractArrow.toLoc_id₁ 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : r.toLoc.id₁ = CategoryTheory.eqToIso ⋯ - CategoryTheory.RetractArrow.toLoc_id₂ 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : r.toLoc.id₂ = CategoryTheory.eqToIso ⋯ - CategoryTheory.RetractArrow.toLoc_commi 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : r.toLoc.commi = CategoryTheory.eqToIso ⋯ - CategoryTheory.RetractArrow.toLoc_commr 📋 Mathlib.CategoryTheory.Bicategory.RetractArrow
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y X' Y' : C} {f' : X' ⟶ Y'} {f : X ⟶ Y} (r : CategoryTheory.RetractArrow f' f) : r.toLoc.commr = CategoryTheory.eqToIso ⋯ - CategoryTheory.Pseudofunctor.CoGrothendieck.instHasFibersForget 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) : HasFibers (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F) - CategoryTheory.Pseudofunctor.CoGrothendieck.instIsFiberedForget 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} : (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsFibered - CategoryTheory.Pseudofunctor.CoGrothendieck.domainCartesianLift 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) : F.CoGrothendieck - CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) : CategoryTheory.Pseudofunctor.CoGrothendieck.domainCartesianLift a f ⟶ { base := S, fiber := a } - CategoryTheory.Pseudofunctor.CoGrothendieck.isHomLift_cartesianLift 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) : (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift f (CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift a f) - CategoryTheory.Pseudofunctor.CoGrothendieck.isStronglyCartesian_homCartesianLift 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) : (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsStronglyCartesian f (CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift a f) - CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮} {a : ↑(F.obj { as := Opposite.op S })} (f : R ⟶ S) {a' : F.CoGrothendieck} (g : a'.base ⟶ R) (φ' : a' ⟶ { base := S, fiber := a }) [(CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'] : a' ⟶ CategoryTheory.Pseudofunctor.CoGrothendieck.domainCartesianLift a f - CategoryTheory.Pseudofunctor.CoGrothendieck.isHomLift_homCartesianLift 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) {a' : F.CoGrothendieck} {φ' : a' ⟶ { base := S, fiber := a }} {g : a'.base ⟶ R} [(CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'] : (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift g (CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift f g φ') - CategoryTheory.Pseudofunctor.CoGrothendieck.ι 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) : CategoryTheory.Functor (↑(F.obj { as := Opposite.op S })) F.CoGrothendieck - CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_base 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) (a : ↑(F.obj { as := Opposite.op S })) : ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).obj a).base = S - CategoryTheory.Pseudofunctor.CoGrothendieck.ι_obj_fiber 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) (a : ↑(F.obj { as := Opposite.op S })) : ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).obj a).fiber = a - CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) : (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).EssSurj - CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) : (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).Faithful - CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) : (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).Full - CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) : (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).IsEquivalence - CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_base 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) {a b : ↑(F.obj { as := Opposite.op S })} (φ : a ⟶ b) : ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).map φ).base = CategoryTheory.CategoryStruct.id S - CategoryTheory.Pseudofunctor.CoGrothendieck.comp_const 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) : (CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F) = (CategoryTheory.Functor.const ↑(F.obj { as := Opposite.op S })).obj S - CategoryTheory.Pseudofunctor.CoGrothendieck.compIso 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) : (CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F) ≅ (CategoryTheory.Functor.const ↑(F.obj { as := Opposite.op S })).obj S - CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_hom_app 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) (X : ↑(F.obj { as := Opposite.op S })) : (CategoryTheory.Pseudofunctor.CoGrothendieck.compIso F S).hom.app X = CategoryTheory.CategoryStruct.id S - CategoryTheory.Pseudofunctor.CoGrothendieck.compIso_inv_app 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) (X : ↑(F.obj { as := Opposite.op S })) : (CategoryTheory.Pseudofunctor.CoGrothendieck.compIso F S).inv.app X = CategoryTheory.CategoryStruct.id S - CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber 📋 Mathlib.CategoryTheory.FiberedCategory.Grothendieck
{𝒮 : Type u_1} [CategoryTheory.Category.{v_1, u_1} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮) {a b : ↑(F.obj { as := Opposite.op S })} (φ : a ⟶ b) : ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).map φ).fiber = CategoryTheory.CategoryStruct.comp φ ((F.mapId { as := Opposite.op S }).inv.toNatTrans.app b) - CategoryTheory.Pseudofunctor.IsPrestack 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) (J : CategoryTheory.GrothendieckTopology C) : Prop - CategoryTheory.Pseudofunctor.presheafHom 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} (M N : ↑(F.obj { as := Opposite.op S })) : CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ (Type v') - CategoryTheory.Pseudofunctor.sheafHom 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) (J : CategoryTheory.GrothendieckTopology C) [F.IsPrestack J] {S : C} (M N : ↑(F.obj { as := Opposite.op S })) : CategoryTheory.Sheaf (J.over S) (Type v') - CategoryTheory.Pseudofunctor.IsPrestack.isSheaf 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} (J : CategoryTheory.GrothendieckTopology C) [self : F.IsPrestack J] {S : C} (M N : ↑(F.obj { as := Opposite.op S })) : CategoryTheory.Presheaf.IsSheaf (J.over S) (F.presheafHom M N) - CategoryTheory.Pseudofunctor.IsPrestack.mk 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {J : CategoryTheory.GrothendieckTopology C} (isSheaf : ∀ {S : C} (M N : ↑(F.obj { as := Opposite.op S })), CategoryTheory.Presheaf.IsSheaf (J.over S) (F.presheafHom M N)) : F.IsPrestack J - CategoryTheory.Pseudofunctor.sheafHom_obj 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) (J : CategoryTheory.GrothendieckTopology C) [F.IsPrestack J] {S : C} (M N : ↑(F.obj { as := Opposite.op S })) : (F.sheafHom J M N).obj = F.presheafHom M N - CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} {M N : ↑(F.obj { as := Opposite.op S })} : (M ⟶ N) ≃ (F.presheafHom M N).obj (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S))) - CategoryTheory.Pseudofunctor.overMapCompPresheafHomIso 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} (M N : ↑(F.obj { as := Opposite.op S })) {S' : C} (q : S' ⟶ S) : (CategoryTheory.Over.map q).op.comp (F.presheafHom M N) ≅ F.presheafHom ((F.map q.op.toLoc).toFunctor.obj M) ((F.map q.op.toLoc).toFunctor.obj N) - CategoryTheory.Pseudofunctor.presheafHom_obj 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} (M N : ↑(F.obj { as := Opposite.op S })) (T : (CategoryTheory.Over S)ᵒᵖ) : (F.presheafHom M N).obj T = ((F.map (Opposite.unop T).hom.op.toLoc).toFunctor.obj M ⟶ (F.map (Opposite.unop T).hom.op.toLoc).toFunctor.obj N) - CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_id 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄ ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄ (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) : CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ (CategoryTheory.CategoryStruct.id Y) f₁ f₂ ⋯ ⋯ = φ - CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄ ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄ (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) ⦃Y' : C⦄ (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁ := by cat_disch) (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂ := by cat_disch) : (F.map gf₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map gf₂.op.toLoc).toFunctor.obj M₂ - CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_pullHom 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄ ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄ (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) ⦃Y' : C⦄ (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) ⦃Y'' : C⦄ (g' : Y'' ⟶ Y') (g'f₁ : Y'' ⟶ X₁) (g'f₂ : Y'' ⟶ X₂) (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁ := by cat_disch) (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂ := by cat_disch) (hg'f₁ : CategoryTheory.CategoryStruct.comp g' gf₁ = g'f₁ := by cat_disch) (hg'f₂ : CategoryTheory.CategoryStruct.comp g' gf₂ = g'f₂ := by cat_disch) : CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ g gf₁ gf₂ hgf₁ hgf₂) g' g'f₁ g'f₂ hg'f₁ hg'f₂ = CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ (CategoryTheory.CategoryStruct.comp g' g) g'f₁ g'f₂ ⋯ ⋯ - CategoryTheory.Pseudofunctor.presheafHom_map 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} (M N : ↑(F.obj { as := Opposite.op S })) {T₁ T₂ : (CategoryTheory.Over S)ᵒᵖ} (p : T₁ ⟶ T₂) : (F.presheafHom M N).map p = TypeCat.ofHom fun f => CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom f (CategoryTheory.Over.Hom.left p.unop) (Opposite.unop T₂).hom (Opposite.unop T₂).hom ⋯ ⋯ - CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} {M N : ↑(F.obj { as := Opposite.op S })} (f : M ⟶ N) : F.presheafHomObjHomEquiv f = CategoryTheory.CategoryStruct.comp ((F.mapId { as := Opposite.op S }).hom.toNatTrans.app M) (CategoryTheory.CategoryStruct.comp f ((F.mapId { as := Opposite.op S }).inv.toNatTrans.app N)) - CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C} {M N : ↑(F.obj { as := Opposite.op S })} (f : (F.map (Opposite.unop (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S)))).hom.op.toLoc).toFunctor.obj M ⟶ (F.map (Opposite.unop (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S)))).hom.op.toLoc).toFunctor.obj N) : F.presheafHomObjHomEquiv.symm f = CategoryTheory.CategoryStruct.comp ((F.mapId { as := Opposite.op S }).inv.toNatTrans.app M) (CategoryTheory.CategoryStruct.comp f ((F.mapId { as := Opposite.op S }).hom.toNatTrans.app N)) - CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom 📋 Mathlib.CategoryTheory.Sites.Descent.IsPrestack
{C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄ ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄ (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) ⦃Y' : C⦄ (g : Y' ⟶ Y) (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁) (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂) : (F.map g.op.toLoc).toFunctor.map φ = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).inv.toNatTrans.app M₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ g gf₁ gf₂ hgf₁ hgf₂) ((F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).hom.toNatTrans.app M₂))
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:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.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