doc-next-gen

Mathlib.CategoryTheory.Grothendieck

Module docstring

{"# The Grothendieck construction

Given a functor F : C ⥤ Cat, the objects of Grothendieck F consist of dependent pairs (b, f), where b : C and f : F.obj c, and a morphism (b, f) ⟶ (b', f') is a pair β : b ⟶ b' in C, and φ : (F.map β).obj f ⟶ f'

Grothendieck.functor makes the Grothendieck construction into a functor from the functor category C ⥤ Cat to the over category Over C in the category of categories.

Categories such as PresheafedSpace are in fact examples of this construction, and it may be interesting to try to generalize some of the development there.

Implementation notes

Really we should treat Cat as a 2-category, and allow F to be a 2-functor.

There is also a closely related construction starting with G : Cᵒᵖ ⥤ Cat, where morphisms consists again of β : b ⟶ b' and φ : f ⟶ (F.map (op β)).obj f'.

Notable constructions

  • Grothendieck F is the Grothendieck construction.
  • Elements of Grothendieck F whose base is c : C can be transported along f : c ⟶ d using transport.
  • A natural transformation α : F ⟶ G induces map α : Grothendieck F ⥤ Grothendieck G.
  • The Grothendieck construction and map together form a functor (functor) from the functor category E ⥤ Cat to the over category Over E.
  • A functor G : D ⥤ C induces pre F G : Grothendieck (G ⋙ F) ⥤ Grothendieck F.

References

See also CategoryTheory.Functor.Elements for the category of elements of functor F : C ⥤ Type.

  • https://stacks.math.columbia.edu/tag/02XV
  • https://ncatlab.org/nlab/show/Grothendieck+construction

"}

CategoryTheory.Grothendieck structure
Full source 
/--
The Grothendieck construction (often written as `∫ F` in mathematics) for a functor `F : C ⥤ Cat`
gives a category whose
* objects `X` consist of `X.base : C` and `X.fiber : F.obj base`
* morphisms `f : X ⟶ Y` consist of
  `base : X.base ⟶ Y.base` and
  `f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber`
-/
structure Grothendieck where
  /-- The underlying object in `C` -/
  base : C
  /-- The object in the fiber of the base object. -/
  fiber : F.obj base
Grothendieck Construction
Informal description
The Grothendieck construction (often denoted $\int F$ in mathematics) for a functor $F \colon C \to \mathrm{Cat}$ yields a category where: - An object $X$ consists of a pair $(X_{\mathrm{base}}, X_{\mathrm{fiber}})$, where $X_{\mathrm{base}}$ is an object in $C$ and $X_{\mathrm{fiber}}$ is an object in $F(X_{\mathrm{base}})$. - A morphism $f \colon X \to Y$ consists of a pair $(f_{\mathrm{base}}, f_{\mathrm{fiber}})$, where $f_{\mathrm{base}} \colon X_{\mathrm{base}} \to Y_{\mathrm{base}}$ is a morphism in $C$ and $f_{\mathrm{fiber}} \colon (F(f_{\mathrm{base}}))(X_{\mathrm{fiber}}) \to Y_{\mathrm{fiber}}$ is a morphism in $F(Y_{\mathrm{base}})$.
CategoryTheory.Grothendieck.Hom structure
(X Y : Grothendieck F)
Full source 
/-- A morphism in the Grothendieck category `F : C ⥤ Cat` consists of
`base : X.base ⟶ Y.base` and `f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber`.
-/
structure Hom (X Y : Grothendieck F) where
  /-- The morphism between base objects. -/
  base : X.base ⟶ Y.base
  /-- The morphism from the pushforward to the source fiber object to the target fiber object. -/
  fiber : (F.map base).obj X.fiber ⟶ Y.fiber
Morphism in the Grothendieck construction
Informal description
A morphism in the Grothendieck category construction for a functor $F \colon C \to \mathrm{Cat}$ consists of two components: 1. A base morphism $\beta \colon X_{\mathrm{base}} \to Y_{\mathrm{base}}$ in the category $C$ 2. A fiber morphism $\varphi \colon (F(\beta))(X_{\mathrm{fiber}}) \to Y_{\mathrm{fiber}}$ in the category $F(Y_{\mathrm{base}})$ where $X = (X_{\mathrm{base}}, X_{\mathrm{fiber}})$ and $Y = (Y_{\mathrm{base}}, Y_{\mathrm{fiber}})$ are objects in the Grothendieck construction.
CategoryTheory.Grothendieck.ext theorem
{X Y : Grothendieck F} (f g : Hom X Y) (w_base : f.base = g.base) (w_fiber : eqToHom (by rw [w_base]) ≫ f.fiber = g.fiber) : f = g
Full source 
@[ext (iff := false)]
theorem ext {X Y : Grothendieck F} (f g : Hom X Y) (w_base : f.base = g.base)
    (w_fiber : eqToHomeqToHom (by rw [w_base]) ≫ f.fiber = g.fiber) : f = g := by
  cases f; cases g
  congr
  dsimp at w_base
  aesop_cat
Extensionality of Morphisms in the Grothendieck Construction
Informal description
Let $F \colon C \to \mathrm{Cat}$ be a functor, and let $X, Y$ be objects in the Grothendieck construction $\int F$. For any two morphisms $f, g \colon X \to Y$ in $\int F$, if: 1. The base morphisms are equal: $f_{\mathrm{base}} = g_{\mathrm{base}}$, and 2. The fiber morphisms satisfy $(\mathrm{eqToHom}\ p) \circ f_{\mathrm{fiber}} = g_{\mathrm{fiber}}$, where $p$ is the equality obtained from $f_{\mathrm{base}} = g_{\mathrm{base}}$, then $f = g$.
CategoryTheory.Grothendieck.id definition
(X : Grothendieck F) : Hom X X
Full source 
/-- The identity morphism in the Grothendieck category.
-/
def id (X : Grothendieck F) : Hom X X where
  base := 𝟙 X.base
  fiber := eqToHom (by simp)
Identity morphism in the Grothendieck construction
Informal description
For any object \(X = (X_{\text{base}}, X_{\text{fiber}})\) in the Grothendieck construction \(\int F\) of a functor \(F \colon C \to \mathrm{Cat}\), the identity morphism \(\mathrm{id}_X \colon X \to X\) consists of: 1. The identity morphism \(\mathrm{id}_{X_{\text{base}}}\) on the base object \(X_{\text{base}}\) in \(C\) 2. The identity morphism \(\mathrm{id}_{X_{\text{fiber}}}\) on the fiber object \(X_{\text{fiber}}\) in \(F(X_{\text{base}})\), transported along the equality induced by the functoriality of \(F\) applied to the identity morphism.
CategoryTheory.Grothendieck.instInhabitedHom instance
(X : Grothendieck F) : Inhabited (Hom X X)
Full source 
instance (X : Grothendieck F) : Inhabited (Hom X X) :=
  ⟨id X⟩
Existence of Identity Morphisms in the Grothendieck Construction
Informal description
For any object $X$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, the hom-set $\mathrm{Hom}(X, X)$ is nonempty, containing at least the identity morphism.
CategoryTheory.Grothendieck.comp definition
{X Y Z : Grothendieck F} (f : Hom X Y) (g : Hom Y Z) : Hom X Z
Full source 
/-- Composition of morphisms in the Grothendieck category.
-/
def comp {X Y Z : Grothendieck F} (f : Hom X Y) (g : Hom Y Z) : Hom X Z where
  base := f.base ≫ g.base
  fiber :=
    eqToHomeqToHom (by simp) ≫ (F.map g.base).map f.fiber ≫ g.fiber
Composition in the Grothendieck construction
Informal description
Given objects \(X, Y, Z\) in the Grothendieck construction \(\int F\) for a functor \(F \colon C \to \mathrm{Cat}\), and morphisms \(f \colon X \to Y\) and \(g \colon Y \to Z\), the composition \(g \circ f \colon X \to Z\) is defined as follows: 1. The base component is the composition \(f_{\mathrm{base}} \circ g_{\mathrm{base}}\) in \(C\) 2. The fiber component is constructed by: - First applying the functor \(F(g_{\mathrm{base}})\) to \(f_{\mathrm{fiber}}\) - Then composing with \(g_{\mathrm{fiber}}\) - Finally precomposing with an isomorphism that adjusts for the functoriality of \(F\)
CategoryTheory.Grothendieck.instCategory instance
: Category (Grothendieck F)
Full source 
instance : Category (Grothendieck F) where
  Hom X Y := Grothendieck.Hom X Y
  id X := Grothendieck.id X
  comp f g := Grothendieck.comp f g
  comp_id {X Y} f := by
    ext
    · simp [comp, id]
    · dsimp [comp, id]
      rw [← NatIso.naturality_2 (eqToIso (F.map_id Y.base)) f.fiber]
      simp
  id_comp f := by ext <;> simp [comp, id]
  assoc f g h := by
    ext
    · simp [comp, id]
    · dsimp [comp, id]
      rw [← NatIso.naturality_2 (eqToIso (F.map_comp _ _)) f.fiber]
      simp
The Category Structure on the Grothendieck Construction
Informal description
The Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$ forms a category where: - Objects are pairs $(c, x)$ with $c \in C$ and $x \in F(c)$. - A morphism $(c, x) \to (c', x')$ consists of a morphism $f \colon c \to c'$ in $C$ and a morphism $\varphi \colon F(f)(x) \to x'$ in $F(c')$. - Composition and identity morphisms are defined componentwise, respecting the functoriality of $F$.
CategoryTheory.Grothendieck.id_base theorem
(X : Grothendieck F) : Hom.base (𝟙 X) = 𝟙 X.base
Full source 
@[simp]
theorem id_base (X : Grothendieck F) :
    Hom.base (𝟙 X) = 𝟙 X.base := by
  rfl
Base Component of Identity in Grothendieck Construction
Informal description
For any object $X$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, the base component of the identity morphism $\mathrm{id}_X$ is equal to the identity morphism $\mathrm{id}_{X_{\mathrm{base}}}$ in the base category $C$.
CategoryTheory.Grothendieck.id_fiber theorem
(X : Grothendieck F) : Hom.fiber (𝟙 X) = eqToHom (by simp)
Full source 
@[simp]
theorem id_fiber (X : Grothendieck F) :
    Hom.fiber (𝟙 X) = eqToHom (by simp) :=
  rfl
Identity Morphism Fiber Component in Grothendieck Construction
Informal description
For any object $X = (c, x)$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, the fiber component of the identity morphism $\mathrm{id}_X$ is equal to the identity morphism $\mathrm{id}_x$ in the fiber category $F(c)$, up to transport along the equality induced by functoriality of $F$.
CategoryTheory.Grothendieck.comp_base theorem
{X Y Z : Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).base = f.base ≫ g.base
Full source 
@[simp]
theorem comp_base {X Y Z : Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).base = f.base ≫ g.base :=
  rfl
Composition of Base Components in the Grothendieck Construction
Informal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, the base component of the composition $f \circ g$ is equal to the composition of the base components of $f$ and $g$ in the category $C$, i.e., $(f \circ g)_{\mathrm{base}} = f_{\mathrm{base}} \circ g_{\mathrm{base}}$.
CategoryTheory.Grothendieck.comp_fiber theorem
{X Y Z : Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.fiber (f ≫ g) = eqToHom (by simp) ≫ (F.map g.base).map f.fiber ≫ g.fiber
Full source 
@[simp]
theorem comp_fiber {X Y Z : Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) :
    Hom.fiber (f ≫ g) =
      eqToHomeqToHom (by simp) ≫ (F.map g.base).map f.fiber ≫ g.fiber :=
  rfl
Fiber Component of Composition in Grothendieck Construction
Informal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, the fiber component of the composite morphism $f \circ g$ is given by: \[ (f \circ g)_{\mathrm{fiber}} = \mathrm{eqToHom}(\text{by simp}) \circ F(g_{\mathrm{base}})(f_{\mathrm{fiber}}) \circ g_{\mathrm{fiber}} \] where: - $f_{\mathrm{fiber}}$ and $g_{\mathrm{fiber}}$ are the fiber components of $f$ and $g$ respectively, - $g_{\mathrm{base}}$ is the base component of $g$, - $\mathrm{eqToHom}(\text{by simp})$ is the identity morphism obtained by simplifying the equality proof.
CategoryTheory.Grothendieck.congr theorem
{X Y : Grothendieck F} {f g : X ⟶ Y} (h : f = g) : f.fiber = eqToHom (by subst h; rfl) ≫ g.fiber
Full source 
theorem congr {X Y : Grothendieck F} {f g : X ⟶ Y} (h : f = g) :
    f.fiber = eqToHomeqToHom (by subst h; rfl) ≫ g.fiber := by
  subst h
  dsimp
  simp
Equality of Morphisms Implies Equality of Fiber Components in Grothendieck Construction
Informal description
For any two morphisms $f, g \colon X \to Y$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, if $f = g$, then the fiber component of $f$ is equal to the composition of the identity morphism (constructed via `eqToHom` from the equality $f = g$) with the fiber component of $g$.
CategoryTheory.Grothendieck.base_eqToHom theorem
{X Y : Grothendieck F} (h : X = Y) : (eqToHom h).base = eqToHom (congrArg Grothendieck.base h)
Full source 
@[simp]
theorem base_eqToHom {X Y : Grothendieck F} (h : X = Y) :
    (eqToHom h).base = eqToHom (congrArg Grothendieck.base h) := by subst h; rfl
Base Component of Equality Morphism in Grothendieck Construction
Informal description
For any objects $X$ and $Y$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, and any equality $h : X = Y$, the base component of the morphism $\mathrm{eqToHom}\, h$ is equal to $\mathrm{eqToHom}$ applied to the equality of base objects obtained by applying the base projection to $h$. That is: $$(\mathrm{eqToHom}\, h)_{\mathrm{base}} = \mathrm{eqToHom}\, (\mathrm{congrArg}\, \mathrm{base}\, h)$$
CategoryTheory.Grothendieck.fiber_eqToHom theorem
{X Y : Grothendieck F} (h : X = Y) : (eqToHom h).fiber = eqToHom (by subst h; simp)
Full source 
@[simp]
theorem fiber_eqToHom {X Y : Grothendieck F} (h : X = Y) :
    (eqToHom h).fiber = eqToHom (by subst h; simp) := by subst h; rfl
Fiber Component of Equality Morphism in Grothendieck Construction
Informal description
For any objects $X$ and $Y$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, and an equality $h : X = Y$, the fiber component of the equality morphism $\mathrm{eqToHom}\, h$ is equal to $\mathrm{eqToHom}$ applied to the trivial equality obtained by substituting $h$ and simplifying. In other words, if $X = Y$ in $\int F$, then the fiber part of the canonical isomorphism between them is the canonical isomorphism between their fibers (which are equal after substitution).
CategoryTheory.Grothendieck.eqToHom_eq theorem
{X Y : Grothendieck F} (hF : X = Y) : eqToHom hF = { base := eqToHom (by subst hF; rfl), fiber := eqToHom (by subst hF; simp) }
Full source 
lemma eqToHom_eq {X Y : Grothendieck F} (hF : X = Y) :
    eqToHom hF = { base := eqToHom (by subst hF; rfl), fiber := eqToHom (by subst hF; simp) } := by
  subst hF
  rfl
Decomposition of Equality-Induced Morphism in Grothendieck Construction
Informal description
For any objects $X$ and $Y$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, and for any equality $hF : X = Y$, the equality-induced morphism $\mathrm{eqToHom}\, hF$ is equal to the morphism whose base component is $\mathrm{eqToHom}\, (\mathrm{congrArg}\, \mathrm{base}\, hF)$ and whose fiber component is $\mathrm{eqToHom}\, (\text{by subst } hF; \text{simp})$.
CategoryTheory.Grothendieck.transport definition
(x : Grothendieck F) {c : C} (t : x.base ⟶ c) : Grothendieck F
Full source 
/--
If `F : C ⥤ Cat` is a functor and `t : c ⟶ d` is a morphism in `C`, then `transport` maps each
`c`-based element of `Grothendieck F` to a `d`-based element.
-/
@[simps]
def transport (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : Grothendieck F :=
  ⟨c, (F.map t).obj x.fiber⟩
Transport in the Grothendieck construction
Informal description
Given an object $x$ in the Grothendieck construction $\int F$ (where $x$ is a pair $(x_{\text{base}}, x_{\text{fiber}})$ with $x_{\text{base}} \in C$ and $x_{\text{fiber}} \in F(x_{\text{base}})$) and a morphism $t \colon x_{\text{base}} \to c$ in $C$, the function `transport` maps $x$ to a new object in $\int F$ with base $c$ and fiber $(F(t))(x_{\text{fiber}})$.
CategoryTheory.Grothendieck.toTransport definition
(x : Grothendieck F) {c : C} (t : x.base ⟶ c) : x ⟶ x.transport t
Full source 
/--
If `F : C ⥤ Cat` is a functor and `t : c ⟶ d` is a morphism in `C`, then `transport` maps each
`c`-based element `x` of `Grothendieck F` to a `d`-based element `x.transport t`.

`toTransport` is the morphism `x ⟶ x.transport t` induced by `t` and the identity on fibers.
-/
@[simps]
def toTransport (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : x ⟶ x.transport t :=
  ⟨t, 𝟙 _⟩
Morphism induced by transport in the Grothendieck construction
Informal description
Given an object \( x \) in the Grothendieck construction \( \int F \) (where \( x \) is a pair \((x_{\text{base}}, x_{\text{fiber}})\) with \( x_{\text{base}} \in C \) and \( x_{\text{fiber}} \in F(x_{\text{base}}) \)) and a morphism \( t \colon x_{\text{base}} \to c \) in \( C \), the morphism `toTransport` from \( x \) to \( x.\text{transport } t \) is defined as the pair \((t, \text{id}_{(F(t))(x_{\text{fiber}})})\).
CategoryTheory.Grothendieck.isoMk definition
{X Y : Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).obj X.fiber ≅ Y.fiber) : X ≅ Y
Full source 
/--
Construct an isomorphism in a Grothendieck construction from isomorphisms in its base and fiber.
-/
@[simps]
def isoMk {X Y : Grothendieck F} (e₁ : X.base ≅ Y.base)
    (e₂ : (F.map e₁.hom).obj X.fiber ≅ Y.fiber) :
    X ≅ Y where
  hom := ⟨e₁.hom, e₂.hom⟩
  inv := ⟨e₁.inv, (F.map e₁.inv).map e₂.inv ≫
    eqToHom (Functor.congr_obj (F.mapIso e₁).hom_inv_id X.fiber)⟩
  hom_inv_id := Grothendieck.ext _ _ (by simp) (by simp)
  inv_hom_id := Grothendieck.ext _ _ (by simp) (by
    have := Functor.congr_hom (F.mapIso e₁).inv_hom_id e₂.inv
    dsimp at this
    simp [this])
Isomorphism construction in the Grothendieck construction
Informal description
Given objects $X$ and $Y$ in the Grothendieck construction $\int F$ of a functor $F \colon C \to \mathrm{Cat}$, and given: - An isomorphism $e_1 \colon X_{\mathrm{base}} \to Y_{\mathrm{base}}$ in the base category $C$, - An isomorphism $e_2 \colon (F(e_1))(X_{\mathrm{fiber}}) \to Y_{\mathrm{fiber}}$ in the fiber category $F(Y_{\mathrm{base}})$, the function `isoMk` constructs an isomorphism $X \to Y$ in $\int F$ whose components are $e_1$ and $e_2$.
CategoryTheory.Grothendieck.transportIso definition
(x : Grothendieck F) {c : C} (α : x.base ≅ c) : x.transport α.hom ≅ x
Full source 
/--
If `F : C ⥤ Cat` and `x : Grothendieck F`, then every `C`-isomorphism `α : x.base ≅ c` induces
an isomorphism between `x` and its transport along `α`
-/
@[simps!]
def transportIso (x : Grothendieck F) {c : C} (α : x.base ≅ c) :
    x.transport α.hom ≅ x := (isoMk α (Iso.refl _)).symm
Isomorphism between an object and its transport along an isomorphism in the Grothendieck construction
Informal description
Given an object \( x \) in the Grothendieck construction \( \int F \) (where \( x = (x_{\text{base}}, x_{\text{fiber}}) \) with \( x_{\text{base}} \in C \) and \( x_{\text{fiber}} \in F(x_{\text{base}}) \)) and an isomorphism \( \alpha : x_{\text{base}} \cong c \) in the base category \( C \), the isomorphism `transportIso` constructs an isomorphism between the transported object \( x.\text{transport } \alpha.hom \) and \( x \) itself. More precisely, the isomorphism is given by the inverse of the isomorphism constructed from \( \alpha \) and the identity isomorphism on the fiber component.
CategoryTheory.Grothendieck.forget definition
: Grothendieck F ⥤ C
Full source 
/-- The forgetful functor from `Grothendieck F` to the source category. -/
@[simps!]
def forget : GrothendieckGrothendieck F ⥤ C where
  obj X := X.1
  map f := f.1
Forgetful functor from the Grothendieck construction
Informal description
The forgetful functor from the Grothendieck construction $\int F$ to the base category $C$, which maps an object $(c, x)$ to $c$ and a morphism $(f, \varphi)$ to $f$.
CategoryTheory.Grothendieck.map definition
(α : F ⟶ G) : Grothendieck F ⥤ Grothendieck G
Full source 
/-- The Grothendieck construction is functorial: a natural transformation `α : F ⟶ G` induces
a functor `Grothendieck.map : Grothendieck F ⥤ Grothendieck G`.
-/
@[simps!]
def map (α : F ⟶ G) : GrothendieckGrothendieck F ⥤ Grothendieck G where
  obj X :=
  { base := X.base
    fiber := (α.app X.base).obj X.fiber }
  map {X Y} f :=
  { base := f.base
    fiber := (eqToHom (α.naturality f.base).symm).app X.fiber ≫ (α.app Y.base).map f.fiber }
  map_id X := by simp only [Cat.eqToHom_app, id_fiber, eqToHom_map, eqToHom_trans]; rfl
  map_comp {X Y Z} f g := by
    dsimp
    congr 1
    simp only [comp_fiber f g, ← Category.assoc, Functor.map_comp, eqToHom_map]
    congr 1
    simp only [Cat.eqToHom_app, Cat.comp_obj, eqToHom_trans, eqToHom_map, Category.assoc,
      ← Cat.comp_map]
    rw [Functor.congr_hom (α.naturality g.base).symm f.fiber]
    simp
Functor induced by a natural transformation on Grothendieck constructions
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to \mathrm{Cat}$, the functor $\mathrm{Grothendieck.map} \alpha \colon \int F \to \int G$ maps: - An object $(c, x)$ in $\int F$ to $(c, \alpha_c(x))$ in $\int G$. - A morphism $(f_{\mathrm{base}}, f_{\mathrm{fiber}}) \colon (c, x) \to (c', x')$ in $\int F$ to $(f_{\mathrm{base}}, \alpha_{c'}(f_{\mathrm{fiber}}) \circ \mathrm{eqToHom}(\alpha_{\mathrm{naturality}}(f_{\mathrm{base}})^{-1})) \colon (c, \alpha_c(x)) \to (c', \alpha_{c'}(x'))$ in $\int G$. This functor respects composition and identities, making the Grothendieck construction functorial in $F$.
CategoryTheory.Grothendieck.map_obj theorem
{α : F ⟶ G} (X : Grothendieck F) : (Grothendieck.map α).obj X = ⟨X.base, (α.app X.base).obj X.fiber⟩
Full source 
theorem map_obj {α : F ⟶ G} (X : Grothendieck F) :
    (Grothendieck.map α).obj X = ⟨X.base, (α.app X.base).obj X.fiber⟩ := rfl
Object Mapping in Grothendieck Construction under Natural Transformation
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to \mathrm{Cat}$ and an object $X = (c, x)$ in the Grothendieck construction $\int F$, the image of $X$ under the functor $\mathrm{Grothendieck.map} \alpha$ is the pair $(c, \alpha_c(x))$ in $\int G$.
CategoryTheory.Grothendieck.map_map theorem
{α : F ⟶ G} {X Y : Grothendieck F} {f : X ⟶ Y} : (Grothendieck.map α).map f = ⟨f.base, (eqToHom (α.naturality f.base).symm).app X.fiber ≫ (α.app Y.base).map f.fiber⟩
Full source 
theorem map_map {α : F ⟶ G} {X Y : Grothendieck F} {f : X ⟶ Y} :
    (Grothendieck.map α).map f =
    ⟨f.base, (eqToHom (α.naturality f.base).symm).app X.fiber ≫ (α.app Y.base).map f.fiber⟩ := rfl
Image of a Morphism under the Grothendieck Construction Functor
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to \mathrm{Cat}$, and a morphism $f \colon (X_{\mathrm{base}}, X_{\mathrm{fiber}}) \to (Y_{\mathrm{base}}, Y_{\mathrm{fiber}})$ in the Grothendieck construction $\int F$, the image of $f$ under the induced functor $\mathrm{Grothendieck.map} \alpha$ is given by the pair $(f_{\mathrm{base}}, \varphi)$, where $\varphi$ is the composition of the morphism induced by the naturality of $\alpha$ at $f_{\mathrm{base}}$ (in reverse) with the image of $f_{\mathrm{fiber}}$ under $\alpha_{Y_{\mathrm{base}}}$. More precisely, $\varphi = (\mathrm{eqToHom}(\alpha_{\mathrm{naturality}}(f_{\mathrm{base}})^{-1}))_{X_{\mathrm{fiber}}} \circ \alpha_{Y_{\mathrm{base}}}(f_{\mathrm{fiber}})$.
CategoryTheory.Grothendieck.functor_comp_forget theorem
{α : F ⟶ G} : Grothendieck.map α ⋙ Grothendieck.forget G = Grothendieck.forget F
Full source 
/-- The functor `Grothendieck.map α : Grothendieck F ⥤ Grothendieck G` lies over `C`. -/
theorem functor_comp_forget {α : F ⟶ G} :
    Grothendieck.mapGrothendieck.map α ⋙ Grothendieck.forget G = Grothendieck.forget F := rfl
Commutativity of Grothendieck Construction with Forgetful Functor under Natural Transformation
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to \mathrm{Cat}$, the composition of the induced functor $\mathrm{Grothendieck.map} \alpha \colon \int F \to \int G$ with the forgetful functor $\mathrm{Grothendieck.forget} G \colon \int G \to C$ equals the forgetful functor $\mathrm{Grothendieck.forget} F \colon \int F \to C$. In other words, the following diagram commutes: \[ \begin{CD} \int F @>{\mathrm{Grothendieck.map} \alpha}>> \int G \\ @V{\mathrm{Grothendieck.forget} F}VV @VV{\mathrm{Grothendieck.forget} G}V \\ C @= C \end{CD} \]
CategoryTheory.Grothendieck.map_id_eq theorem
: map (𝟙 F) = 𝟙 (Cat.of <| Grothendieck <| F)
Full source 
theorem map_id_eq : map (𝟙 F) = 𝟙 (Cat.of <| Grothendieck <| F) := by
  fapply Functor.ext
  · intro X
    rfl
  · intro X Y f
    simp [map_map]
    rfl
Identity Natural Transformation Yields Identity Functor on Grothendieck Construction
Informal description
For any functor $F \colon C \to \mathrm{Cat}$, the functor $\mathrm{Grothendieck.map}$ applied to the identity natural transformation $\mathrm{id}_F$ is equal to the identity functor on the Grothendieck construction $\int F$.
CategoryTheory.Grothendieck.mapIdIso definition
: map (𝟙 F) ≅ 𝟙 (Cat.of <| Grothendieck <| F)
Full source 
/-- Making the equality of functors into an isomorphism. Note: we should avoid equality of functors
if possible, and we should prefer `mapIdIso` to `map_id_eq` whenever we can. -/
def mapIdIso : mapmap (𝟙 F) ≅ 𝟙 (Cat.of <| Grothendieck <| F) := eqToIso map_id_eq
Isomorphism between identity functor and Grothendieck construction of identity natural transformation
Informal description
The isomorphism between the functor obtained by applying the Grothendieck construction to the identity natural transformation $\mathrm{id}_F$ and the identity functor on the Grothendieck construction $\int F$ of $F$.
CategoryTheory.Grothendieck.map_comp_eq theorem
(α : F ⟶ G) (β : G ⟶ H) : map (α ≫ β) = map α ⋙ map β
Full source 
theorem map_comp_eq (α : F ⟶ G) (β : G ⟶ H) :
    map (α ≫ β) = mapmap α ⋙ map β := by
  fapply Functor.ext
  · intro X
    rfl
  · intro X Y f
    simp only [map_map, map_obj_base, NatTrans.comp_app, Cat.comp_obj, Cat.comp_map,
      eqToHom_refl, Functor.comp_map, Functor.map_comp, Category.comp_id, Category.id_comp]
    fapply Grothendieck.ext
    · rfl
    · simp
Functoriality of Grothendieck Construction under Natural Transformation Composition
Informal description
Given natural transformations $\alpha \colon F \to G$ and $\beta \colon G \to H$ between functors $F, G, H \colon C \to \mathrm{Cat}$, the functor obtained by applying the Grothendieck construction to the composition $\alpha \comp \beta$ is equal to the composition of the functors obtained by applying the Grothendieck construction to $\alpha$ and $\beta$ separately. That is, $\mathrm{map}(\alpha \comp \beta) = \mathrm{map}(\alpha) \comp \mathrm{map}(\beta)$.
CategoryTheory.Grothendieck.mapCompIso definition
(α : F ⟶ G) (β : G ⟶ H) : map (α ≫ β) ≅ map α ⋙ map β
Full source 
/-- Making the equality of functors into an isomorphism. Note: we should avoid equality of functors
if possible, and we should prefer `map_comp_iso` to `map_comp_eq` whenever we can. -/
def mapCompIso (α : F ⟶ G) (β : G ⟶ H) : mapmap (α ≫ β) ≅ map α ⋙ map β := eqToIso (map_comp_eq α β)
Isomorphism between composed Grothendieck constructions
Informal description
Given natural transformations $\alpha \colon F \to G$ and $\beta \colon G \to H$ between functors $F, G, H \colon C \to \mathrm{Cat}$, the isomorphism `mapCompIso α β` witnesses that the functor obtained by applying the Grothendieck construction to the composition $\alpha \comp \beta$ is isomorphic to the composition of the functors obtained by applying the Grothendieck construction to $\alpha$ and $\beta$ separately. That is, $\mathrm{map}(\alpha \comp \beta) \cong \mathrm{map}(\alpha) \comp \mathrm{map}(\beta)$.
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse definition
: Grothendieck F ⥤ Grothendieck (F ⋙ Cat.asSmallFunctor.{w})
Full source 
/-- The inverse functor to build the equivalence `compAsSmallFunctorEquivalence`. -/
@[simps]
def compAsSmallFunctorEquivalenceInverse :
    GrothendieckGrothendieck F ⥤ Grothendieck (F ⋙ Cat.asSmallFunctor.{w}) where
  obj X := ⟨X.base, AsSmall.up.obj X.fiber⟩
  map f := ⟨f.base, AsSmall.up.map f.fiber⟩
Inverse functor for Grothendieck construction equivalence with small categories
Informal description
The functor that is the inverse part of the equivalence between the Grothendieck construction of $F$ and the Grothendieck construction of $F$ composed with the small functor embedding. Specifically: - On objects, it maps $(c, x)$ to $(c, \text{AsSmall.up}(x))$, where $\text{AsSmall.up}$ is the embedding of $x$ into the small category. - On morphisms, it maps $(f, \varphi)$ to $(f, \text{AsSmall.up}(\varphi))$.
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor definition
: Grothendieck (F ⋙ Cat.asSmallFunctor.{w}) ⥤ Grothendieck F
Full source 
/-- The functor to build the equivalence `compAsSmallFunctorEquivalence`. -/
@[simps]
def compAsSmallFunctorEquivalenceFunctor :
    GrothendieckGrothendieck (F ⋙ Cat.asSmallFunctor.{w}) ⥤ Grothendieck F where
  obj X := ⟨X.base, AsSmall.down.obj X.fiber⟩
  map f := ⟨f.base, AsSmall.down.map f.fiber⟩
  map_id _ := by apply Grothendieck.ext <;> simp
  map_comp _ _ := by apply Grothendieck.ext <;> simp [down_comp]
Functor for the equivalence of Grothendieck constructions with small functor embedding
Informal description
The functor that builds the equivalence between the Grothendieck construction of the composition of a functor $F \colon C \to \mathrm{Cat}$ with the small functor embedding $\mathrm{Cat.asSmallFunctor}$ and the Grothendieck construction of $F$ itself. Specifically: - On objects: It maps an object $(c, x)$ in $\int (F \circ \mathrm{asSmallFunctor})$ to $(c, \mathrm{AsSmall.down}(x))$ in $\int F$. - On morphisms: It maps a morphism $(f, \varphi)$ in $\int (F \circ \mathrm{asSmallFunctor})$ to $(f, \mathrm{AsSmall.down}(\varphi))$ in $\int F$. This functor is part of an equivalence of categories, where the inverse functor is given by `compAsSmallFunctorEquivalenceInverse`.
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence definition
: Grothendieck (F ⋙ Cat.asSmallFunctor.{w}) ≌ Grothendieck F
Full source 
/-- Taking the Grothendieck construction on `F ⋙ asSmallFunctor`, where
`asSmallFunctor : Cat ⥤ Cat` is the functor which turns each category into a small category of a
(potentiall) larger universe, is equivalent to the Grothendieck construction on `F` itself. -/
@[simps]
def compAsSmallFunctorEquivalence :
    GrothendieckGrothendieck (F ⋙ Cat.asSmallFunctor.{w}) ≌ Grothendieck F where
  functor := compAsSmallFunctorEquivalenceFunctor F
  inverse := compAsSmallFunctorEquivalenceInverse F
  counitIso := Iso.refl _
  unitIso := Iso.refl _
Equivalence of Grothendieck constructions with small functor embedding
Informal description
The Grothendieck construction applied to the composition of a functor $F \colon C \to \mathrm{Cat}$ with the small functor embedding $\mathrm{Cat.asSmallFunctor}$ is equivalent to the Grothendieck construction of $F$ itself. This equivalence is given by: - A functor that maps objects $(c, x)$ to $(c, \mathrm{AsSmall.down}(x))$ and morphisms $(f, \varphi)$ to $(f, \mathrm{AsSmall.down}(\varphi))$. - An inverse functor that maps objects $(c, x)$ to $(c, \mathrm{AsSmall.up}(x))$ and morphisms $(f, \varphi)$ to $(f, \mathrm{AsSmall.up}(\varphi))$. - The unit and counit of the equivalence are both identity isomorphisms.
CategoryTheory.Grothendieck.mapWhiskerRightAsSmallFunctor definition
(α : F ⟶ G) : map (whiskerRight α Cat.asSmallFunctor.{w}) ≅ (compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse
Full source 
/-- Mapping a Grothendieck construction along the whiskering of any natural transformation
`α : F ⟶ G` with the functor `asSmallFunctor : Cat ⥤ Cat` is naturally isomorphic to conjugating
`map α` with the equivalence between `Grothendieck (F ⋙ asSmallFunctor)` and `Grothendieck F`. -/
def mapWhiskerRightAsSmallFunctor (α : F ⟶ G) :
    mapmap (whiskerRight α Cat.asSmallFunctor.{w}) ≅
    (compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙
      (compAsSmallFunctorEquivalence G).inverse :=
  NatIso.ofComponents
    (fun X => Iso.refl _)
    (fun f => by
      fapply Grothendieck.ext
      · simp [compAsSmallFunctorEquivalenceInverse]
      · simp only [compAsSmallFunctorEquivalence_functor, compAsSmallFunctorEquivalence_inverse,
          Functor.comp_obj, compAsSmallFunctorEquivalenceInverse_obj_base, map_obj_base,
          compAsSmallFunctorEquivalenceFunctor_obj_base, Cat.asSmallFunctor_obj, Cat.of_α,
          Iso.refl_hom, Functor.comp_map, comp_base, id_base,
          compAsSmallFunctorEquivalenceInverse_map_base, map_map_base,
          compAsSmallFunctorEquivalenceFunctor_map_base, Cat.asSmallFunctor_map, map_obj_fiber,
          whiskerRight_app, AsSmall.down_obj, AsSmall.up_obj_down,
          compAsSmallFunctorEquivalenceInverse_obj_fiber,
          compAsSmallFunctorEquivalenceFunctor_obj_fiber, comp_fiber, map_map_fiber,
          AsSmall.down_map, down_comp, eqToHom_down, AsSmall.up_map_down, Functor.map_comp,
          eqToHom_map, id_fiber, Category.assoc, eqToHom_trans_assoc,
          compAsSmallFunctorEquivalenceInverse_map_fiber,
          compAsSmallFunctorEquivalenceFunctor_map_fiber, eqToHom_comp_iff, comp_eqToHom_iff]
        simp only [eqToHom_trans_assoc, Category.assoc, conj_eqToHom_iff_heq']
        rw [G.map_id]
        simp )
Natural isomorphism for whiskering with small functor embedding in Grothendieck construction
Informal description
Given a natural transformation $\alpha \colon F \to G$ between functors $F, G \colon C \to \mathrm{Cat}$, the functor obtained by first whiskering $\alpha$ with the small functor embedding $\mathrm{Cat.asSmallFunctor}$ and then applying the Grothendieck construction is naturally isomorphic to the composition of: 1. The equivalence functor from $\mathrm{Grothendieck}(F \circ \mathrm{asSmallFunctor})$ to $\mathrm{Grothendieck}(F)$, 2. The functor $\mathrm{Grothendieck.map} \alpha$ induced by $\alpha$, 3. The inverse equivalence functor from $\mathrm{Grothendieck}(G)$ to $\mathrm{Grothendieck}(G \circ \mathrm{asSmallFunctor})$. This isomorphism is given componentwise by identity isomorphisms at each object, and the naturality condition follows from the functoriality of $G$.
CategoryTheory.Grothendieck.functor definition
{E : Cat.{v, u}} : (E ⥤ Cat.{v, u}) ⥤ Over (T := Cat.{v, u}) E
Full source 
/-- The Grothendieck construction as a functor from the functor category `E ⥤ Cat` to the
over category `Over E`. -/
def functor {E : CatCat.{v, u}} : (E ⥤ Cat.{v,u}) ⥤ Over (T := Cat.{v,u}) E where
  obj F := Over.mk (X := E) (Y := Cat.of (Grothendieck F)) (Grothendieck.forget F)
  map {_ _} α := Over.homMk (X:= E) (Grothendieck.map α) Grothendieck.functor_comp_forget
  map_id F := by
    ext
    exact Grothendieck.map_id_eq (F := F)
  map_comp α β := by
    simp [Grothendieck.map_comp_eq α β]
    rfl
Grothendieck construction functor
Informal description
The Grothendieck construction as a functor from the functor category $E \to \mathrm{Cat}$ to the over category $\mathrm{Over}(E)$. Specifically: - For a functor $F \colon E \to \mathrm{Cat}$, the functor maps $F$ to the forgetful functor $\mathrm{Grothendieck.forget} \colon \mathrm{Grothendieck}(F) \to E$. - For a natural transformation $\alpha \colon F \to G$, the functor maps $\alpha$ to the induced functor $\mathrm{Grothendieck.map} \alpha \colon \mathrm{Grothendieck}(F) \to \mathrm{Grothendieck}(G)$. This construction respects identities and composition of natural transformations, making it a well-defined functor.
CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor definition
: Grothendieck (G ⋙ typeToCat) ⥤ G.Elements
Full source 
/-- Auxiliary definition for `grothendieckTypeToCat`, to speed up elaboration. -/
@[simps!]
def grothendieckTypeToCatFunctor : GrothendieckGrothendieck (G ⋙ typeToCat) ⥤ G.Elements where
  obj X := ⟨X.1, X.2.as⟩
  map f := ⟨f.1, f.2.1.1⟩
Functor from Grothendieck construction to category of elements
Informal description
The functor from the Grothendieck construction of the composition of $G$ with the type-to-category functor to the category of elements of $G$. Specifically: - On objects: maps $(X, Y)$ to $(X, Y.\text{as})$, where $Y.\text{as}$ is the underlying type of $Y$. - On morphisms: maps $(f, \varphi)$ to $(f, \varphi.1.1)$, where $\varphi.1.1$ is the underlying function component of the natural transformation.
CategoryTheory.Grothendieck.grothendieckTypeToCatInverse definition
: G.Elements ⥤ Grothendieck (G ⋙ typeToCat)
Full source 
/-- Auxiliary definition for `grothendieckTypeToCat`, to speed up elaboration. -/
@[simps!]
def grothendieckTypeToCatInverse : G.Elements ⥤ Grothendieck (G ⋙ typeToCat) where
  obj X := ⟨X.1, ⟨X.2⟩⟩
  map f := ⟨f.1, ⟨⟨f.2⟩⟩⟩
Inverse functor from category of elements to Grothendieck construction
Informal description
The functor maps an object $(X, x)$ in the category of elements of $G$ to the object $(X, x)$ in the Grothendieck construction of the composition $G \circ \mathrm{typeToCat}$, and a morphism $(f, \varphi)$ to $(f, \varphi)$.
CategoryTheory.Grothendieck.grothendieckTypeToCat definition
: Grothendieck (G ⋙ typeToCat) ≌ G.Elements
Full source 
/-- The Grothendieck construction applied to a functor to `Type`
(thought of as a functor to `Cat` by realising a type as a discrete category)
is the same as the 'category of elements' construction.
-/
@[simps!]
def grothendieckTypeToCat : GrothendieckGrothendieck (G ⋙ typeToCat) ≌ G.Elements where
  functor := grothendieckTypeToCatFunctor G
  inverse := grothendieckTypeToCatInverse G
  unitIso :=
    NatIso.ofComponents
      (fun X => by
        rcases X with ⟨_, ⟨⟩⟩
        exact Iso.refl _)
      (by
        rintro ⟨_, ⟨⟩⟩ ⟨_, ⟨⟩⟩ ⟨base, ⟨⟨f⟩⟩⟩
        dsimp at *
        simp
        rfl)
  counitIso :=
    NatIso.ofComponents
      (fun X => by
        cases X
        exact Iso.refl _)
      (by
        rintro ⟨⟩ ⟨⟩ ⟨f, e⟩
        dsimp at *
        simp
        rfl)
  functor_unitIso_comp := by
    rintro ⟨_, ⟨⟩⟩
    dsimp
    simp
    rfl
Equivalence between Grothendieck construction and category of elements for type-valued functors
Informal description
The Grothendieck construction applied to the composition of a functor $G \colon C \to \mathrm{Type}$ with the type-to-category functor is equivalent to the category of elements of $G$. More precisely, there is an equivalence of categories between: 1. The Grothendieck construction $\int (G \circ \mathrm{typeToCat})$, whose objects are pairs $(X, Y)$ where $X$ is an object in $C$ and $Y$ is an object in the discrete category corresponding to $G(X)$. 2. The category of elements $G.\mathrm{Elements}$, whose objects are pairs $(X, x)$ where $X$ is an object in $C$ and $x \in G(X)$. This equivalence is given by: - A functor mapping $(X, Y)$ to $(X, Y.\text{as})$ (where $Y.\text{as}$ is the underlying type) - An inverse functor mapping $(X, x)$ to $(X, x)$ - Natural isomorphisms witnessing the equivalence
CategoryTheory.Grothendieck.pre definition
(G : D ⥤ C) : Grothendieck (G ⋙ F) ⥤ Grothendieck F
Full source 
/-- Applying a functor `G : D ⥤ C` to the base of the Grothendieck construction induces a functor
`Grothendieck (G ⋙ F) ⥤ Grothendieck F`. -/
@[simps]
def pre (G : D ⥤ C) : GrothendieckGrothendieck (G ⋙ F) ⥤ Grothendieck F where
  obj X := ⟨G.obj X.base, X.fiber⟩
  map f := ⟨G.map f.base, f.fiber⟩
  map_id X := Grothendieck.ext _ _ (G.map_id _) (by simp)
  map_comp f g := Grothendieck.ext _ _ (G.map_comp _ _) (by simp)
Base Change Functor for Grothendieck Construction
Informal description
Given a functor $G \colon D \to C$, the functor $\text{pre} F G$ from the Grothendieck construction of the composition $G \circ F$ to the Grothendieck construction of $F$ is defined as follows: - On objects: It maps an object $(d, x)$ to $(G(d), x)$. - On morphisms: It maps a morphism $(f, \varphi)$ to $(G(f), \varphi)$.
CategoryTheory.Grothendieck.pre_id theorem
: pre F (𝟭 C) = 𝟭 _
Full source 
@[simp]
theorem pre_id : pre F (𝟭 C) = 𝟭 _ := rfl
Base Change Functor for Identity Functor is Identity in Grothendieck Construction
Informal description
For any functor $F \colon C \to \mathrm{Cat}$, the base change functor $\mathrm{pre} F (\mathrm{id}_C)$ associated with the identity functor $\mathrm{id}_C \colon C \to C$ is equal to the identity functor on the Grothendieck construction $\int F$.
CategoryTheory.Grothendieck.preNatIso definition
{G H : D ⥤ C} (α : G ≅ H) : pre F G ≅ map (whiskerRight α.hom F) ⋙ (pre F H)
Full source 
/--
An natural isomorphism between functors `G ≅ H` induces a natural isomorphism between the canonical
morphism `pre F G` and `pre F H`, up to composition with
`Grothendieck (G ⋙ F) ⥤ Grothendieck (H ⋙ F)`.
-/
def preNatIso {G H : D ⥤ C} (α : G ≅ H) :
    prepre F G ≅ map (whiskerRight α.hom F) ⋙ (pre F H) :=
  NatIso.ofComponents
    (fun X => (transportIso ⟨G.obj X.base, X.fiber⟩ (α.app X.base)).symm)
    (fun f => by fapply Grothendieck.ext <;> simp)
Natural isomorphism between base change functors induced by an isomorphism of functors
Informal description
Given an isomorphism $\alpha \colon G \cong H$ between functors $G, H \colon D \to C$, the natural isomorphism $\mathrm{preNatIso} \alpha$ relates the base change functors $\mathrm{pre} F G$ and $\mathrm{pre} F H$ via the composition with $\mathrm{map} (\alpha \circ F)$. Specifically, for each object $X$ in $\int (G \circ F)$, the component of the natural isomorphism at $X$ is given by the inverse of the transport isomorphism along $\alpha_{X_{\mathrm{base}}}$.
CategoryTheory.Grothendieck.preInv definition
(G : D ≌ C) : Grothendieck F ⥤ Grothendieck (G.functor ⋙ F)
Full source 
/--
Given an equivalence of categories `G`, `preInv _ G` is the (weak) inverse of the `pre _ G.functor`.
-/
def preInv (G : D ≌ C) : GrothendieckGrothendieck F ⥤ Grothendieck (G.functor ⋙ F) :=
  mapmap (whiskerRight G.counitInv F) ⋙ Grothendieck.pre (G.functor ⋙ F) G.inverse
Inverse Base Change Functor for Grothendieck Construction
Informal description
Given an equivalence of categories $G \colon D \simeq C$, the functor $\text{preInv} F G$ is the (weak) inverse of the functor $\text{pre} F G.\text{functor}$. Specifically, it maps objects and morphisms from the Grothendieck construction of $F$ to the Grothendieck construction of the composition $G.\text{functor} \circ F$, using the inverse counit natural transformation of $G$.
CategoryTheory.Grothendieck.pre_comp_map theorem
(G : D ⥤ C) {H : C ⥤ Cat} (α : F ⟶ H) : pre F G ⋙ map α = map (whiskerLeft G α) ⋙ pre H G
Full source 
lemma pre_comp_map (G: D ⥤ C) {H : C ⥤ Cat} (α : F ⟶ H) :
    prepre F G ⋙ map α = mapmap (whiskerLeft G α) ⋙ pre H G := rfl
Naturality of Base Change with Respect to Natural Transformations in the Grothendieck Construction
Informal description
Given functors $G \colon D \to C$ and $H \colon C \to \mathrm{Cat}$, and a natural transformation $\alpha \colon F \to H$, the following diagram of functors between Grothendieck constructions commutes: \[ \begin{CD} \int (G \circ F) @>\mathrm{pre}\, F\, G>> \int F \\ @V\mathrm{map}\, (\mathrm{whiskerLeft}\, G\, \alpha) VV @VV\mathrm{map}\, \alpha V \\ \int (G \circ H) @>\mathrm{pre}\, H\, G>> \int H \end{CD} \] Here, $\mathrm{whiskerLeft}\, G\, \alpha$ denotes the left whiskering of $\alpha$ by $G$.
CategoryTheory.Grothendieck.pre_comp_map_assoc theorem
(G : D ⥤ C) {H : C ⥤ Cat} (α : F ⟶ H) {E : Type*} [Category E] (K : Grothendieck H ⥤ E) : pre F G ⋙ map α ⋙ K = map (whiskerLeft G α) ⋙ pre H G ⋙ K
Full source 
lemma pre_comp_map_assoc (G: D ⥤ C) {H : C ⥤ Cat} (α : F ⟶ H) {E : Type*} [Category E]
    (K : GrothendieckGrothendieck H ⥤ E) : prepre F G ⋙ map α ⋙ K= mapmap (whiskerLeft G α) ⋙ pre H G ⋙ K := rfl
Naturality of Grothendieck Construction with Respect to Precomposition and Mapping
Informal description
Given functors $G \colon D \to C$ and $H \colon C \to \mathrm{Cat}$, a natural transformation $\alpha \colon F \to H$, and a category $E$ with a functor $K \colon \int H \to E$, the following diagram commutes: \[ \begin{CD} \int (G \circ F) @>\mathrm{pre}\,F\,G>> \int F @>\mathrm{map}\,\alpha>> \int H @>K>> E \\ @. @| @AA\mathrm{map}\,(G \circ \alpha)A @| \\ @. \int F @<<\mathrm{pre}\,H\,G< \int (G \circ H) @. E \end{CD} \] More precisely, the composition $\mathrm{pre}\,F\,G \circ \mathrm{map}\,\alpha \circ K$ is equal to $\mathrm{map}\,(G \circ \alpha) \circ \mathrm{pre}\,H\,G \circ K$.
CategoryTheory.Grothendieck.pre_comp theorem
(G : D ⥤ C) (H : E ⥤ D) : pre F (H ⋙ G) = pre (G ⋙ F) H ⋙ pre F G
Full source 
@[simp]
lemma pre_comp (G : D ⥤ C) (H : E ⥤ D) : pre F (H ⋙ G) = prepre (G ⋙ F) H ⋙ pre F G := rfl
Composition Law for Base Change Functors in Grothendieck Construction
Informal description
Given functors $G \colon D \to C$ and $H \colon E \to D$, the functor $\text{pre} F (H \circ G)$ from the Grothendieck construction of $(H \circ G) \circ F$ to the Grothendieck construction of $F$ is equal to the composition of the functors $\text{pre} (G \circ F) H$ and $\text{pre} F G$. In other words, the following diagram commutes: \[ \int (H \circ G \circ F) \xrightarrow{\text{pre} F (H \circ G)} \int F \] is equal to: \[ \int (H \circ G \circ F) \xrightarrow{\text{pre} (G \circ F) H} \int (G \circ F) \xrightarrow{\text{pre} F G} \int F \]
CategoryTheory.Grothendieck.preUnitIso definition
(G : D ≌ C) : map (whiskerRight G.unitInv _) ≅ pre (G.functor ⋙ F) (G.functor ⋙ G.inverse)
Full source 
/--
Let `G` be an equivalence of categories. The functor induced via `pre` by `G.functor ⋙ G.inverse`
is naturally isomorphic to the functor induced via `map` by a whiskered version of `G`'s inverse
unit.
-/
protected def preUnitIso (G : D ≌ C) :
    mapmap (whiskerRight G.unitInv _) ≅ pre (G.functor ⋙ F) (G.functor ⋙ G.inverse) :=
  preNatIso _ G.unitIso.symm |>.symm
Natural isomorphism between whiskered inverse unit and base change functor in Grothendieck construction
Informal description
Given an equivalence of categories $G \colon D \simeq C$, the natural isomorphism $\mathrm{preUnitIso}$ relates the functor $\mathrm{map} (G.\mathrm{unitInv} \circ F)$ to the base change functor $\mathrm{pre} (G.\mathrm{functor} \circ F) (G.\mathrm{functor} \circ G.\mathrm{inverse})$. Specifically, it provides an isomorphism between these two functors from the Grothendieck construction of $(G.\mathrm{functor} \circ G.\mathrm{inverse} \circ G.\mathrm{functor} \circ F)$ to the Grothendieck construction of $F$.
CategoryTheory.Grothendieck.preEquivalence definition
(G : D ≌ C) : Grothendieck (G.functor ⋙ F) ≌ Grothendieck F
Full source 
/--
Given a functor `F : C ⥤ Cat` and an equivalence of categories `G : D ≌ C`, the functor
`pre F G.functor` is an equivalence between `Grothendieck (G.functor ⋙ F)` and `Grothendieck F`.
-/
def preEquivalence (G : D ≌ C) : GrothendieckGrothendieck (G.functor ⋙ F) ≌ Grothendieck F where
  functor := pre F G.functor
  inverse := preInv F G
  unitIso := by
    refine (eqToIso ?_)
      ≪≫ (Grothendieck.preUnitIso F G |> isoWhiskerLeft (map _))
      ≪≫ (pre_comp_map_assoc G.functor _ _ |> Eq.symm |> eqToIso)
    calc
      _ = map (𝟙 _) := map_id_eq.symm
      _ = map _ := ?_
      _ = mapmap _ ⋙ map _ := map_comp_eq _ _
    congr; ext X
    simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, Functor.id_obj,
      Functor.map_id, NatTrans.comp_app, NatTrans.id_app, whiskerLeft_app, whiskerRight_app,
      Equivalence.counitInv_functor_comp]
  counitIso := preNatIso F G.counitIso.symm |>.symm
  functor_unitIso_comp := by
    intro X
    simp only [preInv, Grothendieck.preUnitIso, eq_mpr_eq_cast, cast_eq, pre_id, id_eq,
      Iso.trans_hom, eqToIso.hom, eqToHom_app, eqToHom_refl, isoWhiskerLeft_hom, NatTrans.comp_app]
    fapply Grothendieck.ext <;> simp [preNatIso, transportIso]
Equivalence of Grothendieck constructions under base change by an equivalence
Informal description
Given an equivalence of categories $G \colon D \simeq C$ and a functor $F \colon C \to \mathrm{Cat}$, the Grothendieck constructions $\int (G \circ F)$ and $\int F$ are equivalent categories. Specifically: - The forward functor maps an object $(d, x)$ in $\int (G \circ F)$ to $(G(d), x)$ in $\int F$. - The inverse functor maps an object $(c, y)$ in $\int F$ to $(G^{-1}(c), \text{transport along } \epsilon_c^{-1} \ y)$ in $\int (G \circ F)$, where $\epsilon$ is the counit of the equivalence $G$. - The unit and counit isomorphisms are constructed using the natural isomorphisms arising from the equivalence $G$.
CategoryTheory.Grothendieck.mapWhiskerLeftIsoConjPreMap definition
{F' : C ⥤ Cat} (G : D ≌ C) (α : F ⟶ F') : map (whiskerLeft G.functor α) ≅ (preEquivalence F G).functor ⋙ map α ⋙ (preEquivalence F' G).inverse
Full source 
/--
Let `F, F' : C ⥤ Cat` be functor, `G : D ≌ C` an equivalence and `α : F ⟶ F'` a natural
transformation.

Left-whiskering `α` by `G` and then taking the Grothendieck construction is, up to isomorphism,
the same as taking the Grothendieck construction of `α` and using the equivalences `pre F G`
and `pre F' G` to match the expected type:

```
Grothendieck (G.functor ⋙ F) ≌ Grothendieck F ⥤ Grothendieck F' ≌ Grothendieck (G.functor ⋙ F')
```
-/
def mapWhiskerLeftIsoConjPreMap {F' : C ⥤ Cat} (G : D ≌ C) (α : F ⟶ F') :
    mapmap (whiskerLeft G.functor α) ≅
      (preEquivalence F G).functor ⋙ map α ⋙ (preEquivalence F' G).inverse :=
  (Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft _ (preEquivalence F' G).unitIso
Natural isomorphism between whiskered Grothendieck construction and composed equivalence functors
Informal description
Given an equivalence of categories $G \colon D \simeq C$ and a natural transformation $\alpha \colon F \to F'$ between functors $F, F' \colon C \to \mathrm{Cat}$, there is a natural isomorphism between: 1. The functor obtained by first left-whiskering $\alpha$ with $G$ and then applying the Grothendieck construction, and 2. The composition of the equivalence functor $\mathrm{preEquivalence}\, F\, G$, the Grothendieck construction of $\alpha$, and the inverse of the equivalence functor $\mathrm{preEquivalence}\, F'\, G$. This isomorphism expresses the compatibility between whiskering natural transformations and the Grothendieck construction under base change by an equivalence.
CategoryTheory.Grothendieck.ι definition
(c : C) : F.obj c ⥤ Grothendieck F
Full source 
/-- The inclusion of a fiber `F.obj c` of a functor `F : C ⥤ Cat` into its Grothendieck
construction. -/
@[simps obj map]
def ι (c : C) : F.obj c ⥤ Grothendieck F where
  obj d := ⟨c, d⟩
  map f := ⟨𝟙 _, eqToHom (by simp) ≫ f⟩
  map_id d := by
    dsimp
    congr
    simp only [Category.comp_id]
  map_comp f g := by
    apply Grothendieck.ext _ _ (by simp)
    simp only [comp_base, ← Category.assoc, eqToHom_trans, comp_fiber, Functor.map_comp,
      eqToHom_map]
    congr 1
    simp only [eqToHom_comp_iff, Category.assoc, eqToHom_trans_assoc]
    apply Functor.congr_hom (F.map_id _).symm
Inclusion functor of a fiber into the Grothendieck construction
Informal description
For a functor \( F \colon C \to \mathrm{Cat} \) and an object \( c \in C \), the inclusion functor \( \iota_F(c) \colon F(c) \to \int F \) maps: - An object \( d \in F(c) \) to the pair \( (c, d) \) in the Grothendieck construction \( \int F \). - A morphism \( f \colon d \to d' \) in \( F(c) \) to the morphism \( (1_c, \mathrm{eqToHom}(\text{by simp}) \circ f) \) in \( \int F \), where \( 1_c \) is the identity morphism on \( c \) and \( \mathrm{eqToHom} \) constructs a morphism from an equality proof.
CategoryTheory.Grothendieck.faithful_ι instance
(c : C) : (ι F c).Faithful
Full source 
instance faithful_ι (c : C) : (ι F c).Faithful where
  map_injective f := by
    injection f with _ f
    rwa [cancel_epi] at f
Faithfulness of Fiber Inclusion in the Grothendieck Construction
Informal description
For any object $c$ in the base category $C$, the inclusion functor $\iota_F(c) : F(c) \to \int F$ from the fiber category $F(c)$ to the Grothendieck construction $\int F$ is faithful. That is, for any two morphisms $f, g$ in $F(c)$, if $\iota_F(c)(f) = \iota_F(c)(g)$, then $f = g$.
CategoryTheory.Grothendieck.ιNatTrans definition
{X Y : C} (f : X ⟶ Y) : ι F X ⟶ F.map f ⋙ ι F Y
Full source 
/-- Every morphism `f : X ⟶ Y` in the base category induces a natural transformation from the fiber
inclusion `ι F X` to the composition `F.map f ⋙ ι F Y`. -/
@[simps]
def ιNatTrans {X Y : C} (f : X ⟶ Y) : ιι F X ⟶ F.map f ⋙ ι F Y where
  app d := ⟨f, 𝟙 _⟩
  naturality _ _ _ := by
    simp only [ι, Functor.comp_obj, Functor.comp_map]
    exact Grothendieck.ext _ _ (by simp) (by simp [eqToHom_map])
Natural transformation induced by a base morphism in the Grothendieck construction
Informal description
For any morphism $f \colon X \to Y$ in the base category $C$, there is an induced natural transformation from the fiber inclusion functor $\iota_F X \colon F(X) \to \int F$ to the composition $F(f) \circ \iota_F Y \colon F(X) \to \int F$. Explicitly, the natural transformation maps an object $d \in F(X)$ to the morphism $(f, \mathrm{id}_{F(f)(d)})$ in the Grothendieck construction $\int F$.
CategoryTheory.Grothendieck.functorFrom definition
: Grothendieck F ⥤ E
Full source 
/-- Construct a functor from `Grothendieck F` to another category `E` by providing a family of
functors on the fibers of `Grothendieck F`, a family of natural transformations on morphisms in the
base of `Grothendieck F` and coherence data for this family of natural transformations. -/
@[simps]
def functorFrom : GrothendieckGrothendieck F ⥤ E where
  obj X := (fib X.base).obj X.fiber
  map {X Y} f := (hom f.base).app X.fiber ≫ (fib Y.base).map f.fiber
  map_id X := by simp [hom_id]
  map_comp f g := by simp [hom_comp]
Functor from the Grothendieck construction to a target category
Informal description
Given a functor $F \colon C \to \mathrm{Cat}$ and a category $E$, the construction `functorFrom` builds a functor from the Grothendieck construction $\int F$ to $E$ by: - Mapping an object $(c, x)$ in $\int F$ (where $c \in C$ and $x \in F(c)$) to the object $(fib\, c)\, x$ in $E$, where $fib$ is a family of functors on the fibers of $\int F$. - Mapping a morphism $(f, \varphi) \colon (c, x) \to (c', x')$ in $\int F$ (where $f \colon c \to c'$ in $C$ and $\varphi \colon F(f)(x) \to x'$ in $F(c')$) to the composition $(hom\, f)\, x \circ (fib\, c')\, \varphi$ in $E$, where $hom$ is a family of natural transformations on morphisms in the base category $C$. The construction ensures functoriality by respecting identity morphisms (`hom_id`) and composition (`hom_comp`).
CategoryTheory.Grothendieck.ιCompFunctorFrom definition
(c : C) : ι F c ⋙ (functorFrom fib hom hom_id hom_comp) ≅ fib c
Full source 
/-- `Grothendieck.ι F c` composed with `Grothendieck.functorFrom` is isomorphic a functor on a fiber
on `F` supplied as the first argument to `Grothendieck.functorFrom`. -/
def ιCompFunctorFrom (c : C) : ιι F c ⋙ (functorFrom fib hom hom_id hom_comp)ι F c ⋙ (functorFrom fib hom hom_id hom_comp) ≅ fib c :=
  NatIso.ofComponents (fun _ => Iso.refl _) (fun f => by simp [hom_id])
Natural isomorphism between inclusion-functor composition and fiber functor
Informal description
For a functor \( F \colon C \to \mathrm{Cat} \) and an object \( c \in C \), the composition of the inclusion functor \( \iota_F(c) \colon F(c) \to \int F \) with the functor \( \text{functorFrom} \colon \int F \to E \) is naturally isomorphic to the fiber functor \( \text{fib}_c \colon F(c) \to E \). More precisely, there is a natural isomorphism \( \iota_F(c) \circ \text{functorFrom} \cong \text{fib}_c \) whose components are identity isomorphisms, and this isomorphism respects morphisms in \( F(c) \).
CategoryTheory.Grothendieck.ιCompMap definition
{F' : C ⥤ Cat} (α : F ⟶ F') (c : C) : ι F c ⋙ map α ≅ α.app c ⋙ ι F' c
Full source 
/-- The fiber inclusion `ι F c` composed with `map α` is isomorphic to `α.app c ⋙ ι F' c`. -/
@[simps!]
def ιCompMap {F' : C ⥤ Cat} (α : F ⟶ F') (c : C) : ιι F c ⋙ map αι F c ⋙ map α ≅ α.app c ⋙ ι F' c :=
  NatIso.ofComponents (fun X => Iso.refl _) (fun f => by simp [map])
Natural isomorphism between fiber inclusion and Grothendieck construction functors
Informal description
For a natural transformation $\alpha \colon F \to F'$ between functors $F, F' \colon C \to \mathrm{Cat}$ and an object $c \in C$, the composition of the fiber inclusion functor $\iota_F(c) \colon F(c) \to \int F$ with the induced functor $\mathrm{map}\, \alpha \colon \int F \to \int F'$ is naturally isomorphic to the composition of $\alpha_c \colon F(c) \to F'(c)$ with the fiber inclusion functor $\iota_{F'}(c) \colon F'(c) \to \int F'$. In other words, the following diagram commutes up to natural isomorphism: \[ \begin{CD} F(c) @>{\iota_F(c)}>> \int F \\ @V{\alpha_c}VV @VV{\mathrm{map}\, \alpha}V \\ F'(c) @>>{\iota_{F'}(c)}> \int F' \end{CD} \]