Theorems · Definition · category theory

CategoryTheory.Over.conePostIso

{J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          (i : J) →
            (CategoryTheory.Over.conePost F i).comp
                (CategoryTheory.Limits.Cone.functoriality (CategoryTheory.Over.post F)
                  (CategoryTheory.Over.forget (F.obj i))) ≅
              CategoryTheory.Limits.Cone.whiskering (CategoryTheory.Over.forget i)

conePost is compatible with the forgetful functors on over categories.

Defined in

Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Cited by

2 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category