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).

Equations
  • F.Elements = ((c : C) × F.obj c)
Instances For
    @[reducible, inline]
    abbrev CategoryTheory.Functor.elementsMk {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (X : C) (x : F.obj X) :
    F.Elements

    Constructor for the type F.Elements when F is a functor to types.

    Equations
    • F.elementsMk X x = X, x
    Instances For
      theorem CategoryTheory.Functor.Elements.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x : F.Elements) (y : F.Elements) (h₁ : x.fst = y.fst) (h₂ : F.map (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.

      Equations
      @[simp]
      theorem CategoryTheory.CategoryOfElements.homMk_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x : F.Elements) (y : F.Elements) (f : x.fst y.fst) (hf : F.map f x.snd = y.snd) :
      def CategoryTheory.CategoryOfElements.homMk {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x : F.Elements) (y : F.Elements) (f : x.fst y.fst) (hf : F.map f x.snd = y.snd) :
      x y

      Constructor for morphisms in the category of elements of a functor to types.

      Equations
      Instances For
        theorem CategoryTheory.CategoryOfElements.ext {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {x : F.Elements} {y : F.Elements} (f : x y) (g : x y) (w : f = g) :
        f = g
        @[simp]
        theorem CategoryTheory.CategoryOfElements.comp_val {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {p : F.Elements} {q : F.Elements} {r : F.Elements} {f : p q} {g : q r} :
        @[simp]
        theorem CategoryTheory.CategoryOfElements.map_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {p : F.Elements} {q : F.Elements} (f : p q) :
        F.map (f) p.snd = q.snd

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

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.CategoryOfElements.map_map_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ F₂) {t₁ : F₁.Elements} {t₂ : F₁.Elements} (k : t₁ t₂) :
          @[simp]
          theorem CategoryTheory.CategoryOfElements.map_obj_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ F₂) (t : F₁.Elements) :
          ((CategoryTheory.CategoryOfElements.map α).obj t).snd = α.app t.fst t.snd
          @[simp]
          theorem CategoryTheory.CategoryOfElements.map_obj_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ F₂) (t : F₁.Elements) :

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

          Equations
          • CategoryTheory.CategoryOfElements.map α = { obj := fun (t : F₁.Elements) => t.fst, α.app t.fst t.snd, map := fun {t₁ t₂ : F₁.Elements} (k : t₁ t₂) => k, , map_id := , map_comp := }
          Instances For

            The forward direction of the equivalence F.Elements ≅ (*, F).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The reverse direction of the equivalence F.Elements ≅ (*, F).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[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.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : F.Elements) => CategoryTheory.Iso.refl X) ).hom ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toStructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) ((CategoryTheory.CategoryOfElements.fromStructuredArrow F).associator (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 PUnit.{w + 1} F) => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ) ).hom (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F).leftUnitor.hom) (CategoryTheory.NatIso.ofComponents (fun (X : F.Elements) => CategoryTheory.Iso.refl X) ).inv)))))
                @[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 : F.Elements) => CategoryTheory.Iso.refl X) ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F).leftUnitor.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.StructuredArrow PUnit.{w + 1} F) => CategoryTheory.StructuredArrow.isoMk (CategoryTheory.Iso.refl X.right) ) ).inv (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toStructuredArrow F) ((CategoryTheory.CategoryOfElements.fromStructuredArrow F).associator (CategoryTheory.CategoryOfElements.toStructuredArrow F) (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).hom) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toStructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromStructuredArrow F) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatIso.ofComponents (fun (X : F.Elements) => CategoryTheory.Iso.refl X) ).inv ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F))) ((CategoryTheory.CategoryOfElements.toStructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromStructuredArrow F)).leftUnitor.hom)))))

                The equivalence between the category of elements F.Elements and the comma category (*, F).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    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.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom )) ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.associator (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.eqToHom ) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.leftUnitor.hom) (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom )))))))

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      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.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.leftUnitor.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.whiskerRight (CategoryTheory.eqToHom ) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (CategoryTheory.CategoryOfElements.toCostructuredArrow F) ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp.associator (CategoryTheory.CategoryOfElements.toCostructuredArrow F) (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).hom) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).associator (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.NatTrans.op (CategoryTheory.eqToHom )) ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp)) ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).comp (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).rightOp).leftUnitor.hom)))))

                        The equivalence F.elementsᵒᵖ ≌ (yoneda, F) is compatible with the forgetful functors.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The equivalence F.elementsᵒᵖ ≌ (yoneda, F) is compatible with the forgetful functors.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def CategoryTheory.Functor.Elements.initial {C : Type u} [CategoryTheory.Category.{v, u} C] (A : C) :
                            (CategoryTheory.yoneda.obj A).Elements

                            The initial object in the category of elements for a representable functor. In isInitial it is shown that this is initial.

                            Equations
                            Instances For

                              Show that Elements.initial A is initial in the category of elements for the yoneda functor.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For