commaFromUnder — Mathlib

Lean4
/-- The category of functors `J ⥤ Under X` can be seen as part of a comma category,
namely the comma category constructed from the identity of the category of functors
`J ⥤ C` and the functor that maps `X : C` to the constant functor `J ⥤ C`.

Given a functor `K : J ⥤ Under X`, it is mapped to a natural transformation to the
obvious functor `J ⥤ C` from the constant functor `X`. -/
@[simps]
def commaFromUnder : (J ⥤ Under X) ⥤ Comma (Functor.const J) (𝟭 (J ⥤ C))
    where
  obj
    K :=
    { left := X
      right := K ⋙ Under.forget X
      hom.app a := (K.obj a).hom }
  map
    f :=
    { left := 𝟙 X
      right := Functor.whiskerRight f (Under.forget X) }
Похожие утверждения