Documentation

Mathlib.CategoryTheory.Elements

The category of elements #

This file defines the category of elements, also known as (a special case of) the Grothendieck construction.

Given a functor F : C ⥤ Type, an object of F.Elements is a pair (X : C, x : F.obj X). A morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C, so F.map f takes x to y.

Implementation notes #

This construction is equivalent to a special case of a comma construction, so this is mostly just a more convenient API. We prove the equivalence in CategoryTheory.CategoryOfElements.structuredArrowEquivalence.

References #

Tags #

category of elements, Grothendieck construction, comma category

The type of objects for the category of elements of a functor F : C ⥤ Type is a pair (X : C, x : F.obj X).

Instances For
    theorem CategoryTheory.Functor.Elements.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x : CategoryTheory.Functor.Elements F) (y : CategoryTheory.Functor.Elements F) (h₁ : x.fst = y.fst) (h₂ : C.map CategoryTheory.CategoryStruct.toQuiver (Type w) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor x.fst y.fst (CategoryTheory.eqToHom h₁) x.snd = y.snd) :
    x = y

    The category structure on F.Elements, for F : C ⥤ Type. A morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C, so F.map f takes x to y.

    The functor out of the category of elements which forgets the element.

    Instances For
      @[simp]

      A natural transformation between functors induces a functor between the categories of elements.

      Instances For
        @[simp]
        theorem CategoryTheory.CategoryOfElements.fromStructuredArrow_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : CategoryTheory.StructuredArrow PUnit.{w + 1} F} {Y : CategoryTheory.StructuredArrow PUnit.{w + 1} F} (f : X Y) :
        (CategoryTheory.CategoryOfElements.fromStructuredArrow F).map f = { val := f.right, property := (_ : CategoryTheory.CategoryStruct.comp (Type w) CategoryTheory.Category.toCategoryStruct ((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj X.left) (F.obj X.right) (F.obj Y.right) X.hom (F.map f.right) PUnit.unit = CategoryTheory.CategoryStruct.comp (Type w) CategoryTheory.Category.toCategoryStruct ((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj X.left) ((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj Y.left) (F.obj Y.right) ((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).map f.left) Y.hom PUnit.unit) }
        @[simp]
        theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) :
        (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).unitIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Iso.refl X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.Functor.leftUnitor (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right)).inv (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F) (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Iso.refl X).inv (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).hom)))))
        @[simp]
        theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_unitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) :
        (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).unitIso.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Iso.refl X).hom (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F) (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right)).hom (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.Functor.leftUnitor (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).hom) (CategoryTheory.NatIso.ofComponents fun X => CategoryTheory.Iso.refl X).inv)))))
        @[simp]
        theorem CategoryTheory.CategoryOfElements.structuredArrowEquivalence_inverse_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) :
        ∀ {X Y : CategoryTheory.StructuredArrow PUnit.{w + 1} F} (f : X Y), (CategoryTheory.CategoryOfElements.structuredArrowEquivalence F).inverse.map f = { val := f.right, property := (_ : CategoryTheory.CategoryStruct.comp (Type w) CategoryTheory.Category.toCategoryStruct ((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj X.left) (F.obj X.right) (F.obj Y.right) X.hom (F.map f.right) PUnit.unit = CategoryTheory.CategoryStruct.comp (Type w) CategoryTheory.Category.toCategoryStruct ((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj X.left) ((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).obj Y.left) (F.obj Y.right) ((CategoryTheory.Functor.fromPUnit PUnit.{w + 1} ).map f.left) Y.hom PUnit.unit) }

        The forward direction of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F), given by CategoryTheory.yonedaSections.

        Instances For

          The reverse direction of the equivalence F.Elementsᵒᵖ ≅ (yoneda, F), given by CategoryTheory.yonedaEquiv.

          Instances For
            @[simp]
            theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) :
            (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).unitIso.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom (_ : CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.Functor.Elements F)))) (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.eqToHom (_ : CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F))) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.Functor.leftUnitor (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).hom) (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom (_ : CategoryTheory.Functor.id (CategoryTheory.Functor.Elements F) = CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F)))))))))

            The equivalence F.Elementsᵒᵖ ≅ (yoneda, F) given by yoneda lemma.

            Instances For
              @[simp]
              theorem CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) :
              (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).unitIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom (_ : CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F) = CategoryTheory.Functor.id (CategoryTheory.Functor.Elements F)))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.Functor.leftUnitor (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.eqToHom (_ : CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F) = CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.toCostructuredArrow F))) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom (_ : CategoryTheory.Functor.id (CategoryTheory.Functor.Elements F) = CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F).rightOp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F)))) (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.Functor.leftUnitor (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).hom)))))