Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Module docstring

{"# Structured Arrow Categories as strict functor to Cat

Forming a structured arrow category StructuredArrow d T with d : D and T : C ⥤ D is strictly functorial in S, inducing a functor Dᵒᵖ ⥤ Cat. This file constructs said functor and proves that, in the dual case, we can precompose it with another functor L : E ⥤ D to obtain a category equivalent to Comma L T. "}

CategoryTheory.StructuredArrow.functor definition

(T : C ⥤ D) : Dᵒᵖ ⥤ Cat

Full source

/-- The structured arrow category `StructuredArrow d T` depends on the chosen domain `d : D` in a
functorial way, inducing a functor `Dᵒᵖ ⥤ Cat`. -/
@[simps]
def functor (T : C ⥤ D) : DᵒᵖDᵒᵖ ⥤ Cat where
  obj d := .of <| StructuredArrow d.unop T
  map f := map f.unop
  map_id d := Functor.ext (fun ⟨_, _, _⟩ => by simp [CostructuredArrow.map, Comma.mapRight])
  map_comp f g := Functor.ext (fun _ => by simp [CostructuredArrow.map, Comma.mapRight])

Functoriality of Structured Arrow Categories

Informal description

The functor $\mathrm{StructuredArrow}(-, T) : D^{\mathrm{op}} \to \mathrm{Cat}$ assigns to each object $d \in D$ the category $\mathrm{StructuredArrow}(d, T)$ of structured arrows with domain $d$ and codomain in the image of $T : C \to D$. For a morphism $f : d \to d'$ in $D^{\mathrm{op}}$, the functor maps it to the functor $\mathrm{StructuredArrow}(f, T) : \mathrm{StructuredArrow}(d', T) \to \mathrm{StructuredArrow}(d, T)$ induced by precomposition with $f$.

CategoryTheory.CostructuredArrow.functor definition

(T : C ⥤ D) : D ⥤ Cat

Full source

/-- The costructured arrow category `CostructuredArrow T d` depends on the chosen codomain `d : D`
in a functorial way, inducing a functor `D ⥤ Cat`. -/
@[simps]
def functor (T : C ⥤ D) : D ⥤ Cat where
  obj d := .of <| CostructuredArrow T d
  map f := CostructuredArrow.map f
  map_id d := Functor.ext (fun ⟨_, _, _⟩ => by simp [CostructuredArrow.map, Comma.mapRight])
  map_comp f g := Functor.ext (fun _ => by simp [CostructuredArrow.map, Comma.mapRight])

Functoriality of Costructured Arrow Categories

Informal description

The functor `CostructuredArrow.functor T` maps each object `d` in category `D` to the category `CostructuredArrow T d`, which consists of objects of the form `(c, f)` where `c` is an object in `C` and `f : T c → d` is a morphism in `D`. For a morphism `f : d → d'` in `D`, the functor acts by post-composition with `f` on the morphisms in the costructured arrow category. This construction is strictly functorial in `T`.

CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma definition

: Grothendieck (R ⋙ functor L) ⥤ Comma L R

Full source

/-- The functor used to establish the equivalence `grothendieckPrecompFunctorEquivalence` between
the Grothendieck construction on `CostructuredArrow.functor` and the comma category. -/
@[simps]
def grothendieckPrecompFunctorToComma : GrothendieckGrothendieck (R ⋙ functor L) ⥤ Comma L R where
  obj P := ⟨P.fiber.left, P.base, P.fiber.hom⟩
  map f := ⟨f.fiber.left, f.base, by simp⟩

Functor from Grothendieck construction to comma category via precomposition

Informal description

The functor $\mathrm{grothendieckPrecompFunctorToComma}$ maps an object $(d, (c, f))$ in the Grothendieck construction of the functor $R \circ \mathrm{functor}\,L$ to the object $(c, d, f)$ in the comma category $\mathrm{Comma}\,L\,R$. On morphisms, it sends a morphism $(g, h)$ in the Grothendieck construction to the morphism $(g, h)$ in the comma category, where the components are appropriately matched.

CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst definition

 (X : E) : Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst _ _ ≅ proj L (R.obj X)

Full source

/-- Fibers of `grothendieckPrecompFunctorToComma L R`, composed with `Comma.fst L R`, are isomorphic
to the projection `proj L (R.obj X)`. -/
@[simps!]
def ιCompGrothendieckPrecompFunctorToCommaCompFst (X : E) :
    Grothendieck.ιGrothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst _ _Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst _ _ ≅
    proj L (R.obj X) :=
  NatIso.ofComponents (fun X => Iso.refl _) (fun _ => by simp)

Natural isomorphism of composed functors in Grothendieck construction and comma category

Informal description

For any object $ X $ in category $ E $, the composition of the inclusion functor $ \iota $ from the fiber at $ X $ in the Grothendieck construction of $ R \circ \mathrm{functor}\,L $, followed by the functor $ \mathrm{grothendieckPrecompFunctorToComma}\,L\,R $ and then the projection functor $ \mathrm{Comma.fst} $, is naturally isomorphic to the projection functor $ \mathrm{proj}\,L\,(R.obj\,X) $.

CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor definition

: Comma L R ⥤ Grothendieck (R ⋙ functor L)

Full source

/-- The inverse functor used to establish the equivalence `grothendieckPrecompFunctorEquivalence`
between the Grothendieck construction on `CostructuredArrow.functor` and the comma category. -/
@[simps]
def commaToGrothendieckPrecompFunctor : CommaComma L R ⥤ Grothendieck (R ⋙ functor L) where
  obj X := ⟨X.right, mk X.hom⟩
  map f := ⟨f.right, homMk f.left⟩
  map_id X := Grothendieck.ext _ _ rfl (by simp)
  map_comp f g := Grothendieck.ext _ _ rfl (by simp)

Functor from comma category to Grothendieck construction of precomposition

Informal description

The functor maps an object $X$ in the comma category $\mathrm{Comma}\, L\, R$ to an object in the Grothendieck construction of the composition $R \circ \mathrm{functor}\, L$, where: - The base object is $X_{\mathrm{right}}$ (the right component of $X$ in $\mathrm{Comma}\, L\, R$). - The fiber object is constructed from the morphism $X_{\mathrm{hom}}$ (the natural transformation component of $X$). For a morphism $f$ in $\mathrm{Comma}\, L\, R$, the functor maps it to a morphism in the Grothendieck construction, where: - The base morphism is $f_{\mathrm{right}}$ (the right component of $f$). - The fiber morphism is constructed from $f_{\mathrm{left}}$ (the left component of $f$). The functor preserves identity and composition strictly.

CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence definition

: Grothendieck (R ⋙ functor L) ≌ Comma L R

Full source

/-- For `L : C ⥤ D`, taking the Grothendieck construction of `CostructuredArrow.functor L`
precomposed with another functor `R : E ⥤ D` results in a category which is equivalent to
the comma category `Comma L R`. -/
@[simps]
def grothendieckPrecompFunctorEquivalence : GrothendieckGrothendieck (R ⋙ functor L) ≌ Comma L R where
  functor := grothendieckPrecompFunctorToComma _ _
  inverse := commaToGrothendieckPrecompFunctor _ _
  unitIso := NatIso.ofComponents (fun _ => Iso.refl _)
  counitIso := NatIso.ofComponents (fun _ => Iso.refl _)

Equivalence between Grothendieck construction and comma category via precomposition

Informal description

The Grothendieck construction of the composition $R \circ \mathrm{functor}\, L$ is equivalent to the comma category $\mathrm{Comma}\, L\, R$. Here: - $\mathrm{functor}\, L$ is the functor that maps each object $d$ in $D$ to the costructured arrow category $\mathrm{CostructuredArrow}\, L\, d$. - The equivalence is established via the functors $\mathrm{grothendieckPrecompFunctorToComma}$ and $\mathrm{commaToGrothendieckPrecompFunctor}$, with both the unit and counit natural isomorphisms being identity isomorphisms.

CategoryTheory.CostructuredArrow.grothendieckProj definition

: Grothendieck (functor L) ⥤ C

Full source

/-- The functor projecting out the domain of arrows from the Grothendieck construction on
costructured arrows. -/
@[simps!]
def grothendieckProj : GrothendieckGrothendieck (functor L) ⥤ C :=
  grothendieckPrecompFunctorToCommagrothendieckPrecompFunctorToComma L (𝟭 _) ⋙ Comma.fst _ _

Projection functor from Grothendieck construction to base category via costructured arrows

Informal description

The functor $\mathrm{grothendieckProj}\, L$ maps an object $(d, (c, f))$ in the Grothendieck construction of the functor $\mathrm{functor}\, L$ to the object $c$ in category $C$. On morphisms, it sends a morphism $(g, h)$ in the Grothendieck construction to the morphism $g$ in $C$, where $g$ is the left component of the morphism in the comma category obtained via the functor $\mathrm{grothendieckPrecompFunctorToComma}$.

CategoryTheory.CostructuredArrow.ιCompGrothendieckProj definition

(X : D) : Grothendieck.ι (functor L) X ⋙ grothendieckProj L ≅ proj L X

Full source

/-- Fibers of `grothendieckProj L` are isomorphic to the projection `proj L X`. -/
@[simps!]
def ιCompGrothendieckProj (X : D) :
    Grothendieck.ιGrothendieck.ι (functor L) X ⋙ grothendieckProj LGrothendieck.ι (functor L) X ⋙ grothendieckProj L ≅ proj L X :=
  ιCompGrothendieckPrecompFunctorToCommaCompFst L (𝟭 _) X

Natural isomorphism between composed inclusion and projection functors in Grothendieck construction

Informal description

For any object $ X $ in category $ D $, the composition of the inclusion functor $ \iota $ from the fiber at $ X $ in the Grothendieck construction of the functor $ \mathrm{functor}\,L $, followed by the projection functor $ \mathrm{grothendieckProj}\,L $, is naturally isomorphic to the projection functor $ \mathrm{proj}\,L\,X $.

CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj definition

{X Y : D} (f : X ⟶ Y) : CostructuredArrow.map f ⋙ Grothendieck.ι (functor L) Y ⋙ grothendieckProj L ≅ proj L X

Full source

/-- Functors between costructured arrow categories induced by morphisms in the base category
composed with fibers of `grothendieckProj L` are isomorphic to the projection `proj L X`. -/
@[simps!]
def mapCompιCompGrothendieckProj {X Y : D} (f : X ⟶ Y) :
    CostructuredArrow.mapCostructuredArrow.map f ⋙ Grothendieck.ι (functor L) Y ⋙ grothendieckProj LCostructuredArrow.map f ⋙ Grothendieck.ι (functor L) Y ⋙ grothendieckProj L ≅ proj L X :=
  isoWhiskerLeft (CostructuredArrow.map f) (ιCompGrothendieckPrecompFunctorToCommaCompFst L (𝟭 _) Y)

Natural isomorphism of composed functors involving costructured arrow map and Grothendieck construction

Informal description

For any morphism $ f : X \to Y $ in category $ D $, the composition of the functor `CostructuredArrow.map f` (which post-composes with $ f $ in the costructured arrow category), followed by the inclusion functor $ \iota $ into the Grothendieck construction at $ Y $, and then the projection functor `grothendieckProj L`, is naturally isomorphic to the projection functor `proj L X`.

CategoryTheory.CostructuredArrow.preFunctor definition

{D : Type u₁} [Category.{v₁} D] (S : C ⥤ D) (T : D ⥤ E) : functor (S ⋙ T) ⟶ functor T

Full source

/-- The functor `CostructuredArrow.pre` induces a natural transformation
`CostructuredArrow.functor (S ⋙ T) ⟶ CostructuredArrow.functor T` for `S : C ⥤ D` and
`T : D ⥤ E`. -/
@[simps]
def preFunctor {D : Type u₁} [Category.{v₁} D] (S : C ⥤ D) (T : D ⥤ E) :
    functorfunctor (S ⋙ T) ⟶ functor T where
  app e := pre S T e

Natural transformation induced by precomposition in costructured arrow categories

Informal description

Given functors $S \colon C \to D$ and $T \colon D \to E$, the natural transformation $\mathrm{CostructuredArrow.preFunctor}\ S\ T$ maps from the functor $\mathrm{CostructuredArrow.functor}\ (S \circ T)$ to the functor $\mathrm{CostructuredArrow.functor}\ T$. This transformation is constructed using the precomposition operation $\mathrm{CostructuredArrow.pre}$.