Theorems · Theorem · category theory

CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_counitIso

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v))),
  (CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence F).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.CostructuredArrow.isoMk
          (CategoryTheory.Iso.refl
            (({ obj := fun X => Opposite.op (F.elementsMk (Opposite.op X.left) (CategoryTheory.uliftYonedaEquiv X.hom)),
                        map := fun {X Y} f =>
                          (CategoryTheory.CategoryOfElements.homMk
                              (F.elementsMk (Opposite.op Y.left) (CategoryTheory.uliftYonedaEquiv Y.hom))
                              (F.elementsMk (Opposite.op X.left) (CategoryTheory.uliftYonedaEquiv X.hom)) f.left.op
                              ⋯).op,
                        map_id := ⋯, map_comp := ⋯ }.comp
                    {
                      obj := fun x =>
                        CategoryTheory.CostructuredArrow.mk
                          (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd),
                      map := fun {X Y} f => CategoryTheory.CostructuredArrow.homMk (↑(Opposite.unop f)).unop ⋯,
                      map_id := ⋯, map_comp := ⋯ }).obj
                X).left)
          ⋯)
      ⋯

Defined in

Mathlib.CategoryTheory.Elements

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category