commaFromOver — Mathlib

Lean4
/-- The category of functors `J ⥤ Over 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 ⥤ Over X`, it is mapped to a natural transformation from the
obvious functor `J ⥤ C` to the constant functor `X`. -/
@[simps]
def commaFromOver : (J ⥤ Over X) ⥤ Comma (𝟭 (J ⥤ C)) (Functor.const J)
    where
  obj
    K :=
    { left := K ⋙ Over.forget X
      right := X
      hom.app a := (K.obj a).hom }
  map
    f :=
    { left := Functor.whiskerRight f (Over.forget X)
      right := 𝟙 X }
Похожие утверждения