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.NatTrans.mapElements_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} (φ : F G) :
      ∀ (x : F.Elements), (CategoryTheory.NatTrans.mapElements φ).obj x = match x with | X, x => X, φ.app X x
      @[simp]
      theorem CategoryTheory.NatTrans.mapElements_map_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} (φ : F G) {p : F.Elements} {q : F.Elements} :
      ∀ (x : p q), ((CategoryTheory.NatTrans.mapElements φ).map x) = x

      Natural transformations are mapped to functors between category of elements

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.Functor.elementsFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] :
        ∀ {X Y : CategoryTheory.Functor C (Type w)} (n : X Y), CategoryTheory.Functor.elementsFunctor.map n = CategoryTheory.NatTrans.mapElements n
        @[simp]
        theorem CategoryTheory.Functor.elementsFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) :
        CategoryTheory.Functor.elementsFunctor.obj F = CategoryTheory.Cat.of F.Elements

        The functor mapping functors C ⥤ Type w to their category of elements

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[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_iff {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} :
            f = g f = g
            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
            @[simp]
            theorem CategoryTheory.CategoryOfElements.isoMk_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x : F.Elements) (y : F.Elements) (e : x.fst y.fst) (he : F.map e.hom x.snd = y.snd) :
            @[simp]
            theorem CategoryTheory.CategoryOfElements.isoMk_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x : F.Elements) (y : F.Elements) (e : x.fst y.fst) (he : F.map e.hom x.snd = y.snd) :
            def CategoryTheory.CategoryOfElements.isoMk {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x : F.Elements) (y : F.Elements) (e : x.fst y.fst) (he : F.map e.hom x.snd = y.snd) :
            x y

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

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

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

              Equations
              Instances For
                @[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) :
                @[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_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₂) :

                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

                      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

                            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

                              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