Documentation

Mathlib.CategoryTheory.Sigma.Basic

Disjoint union of categories #

We define the category structure on a sigma-type (disjoint union) of categories.

inductive CategoryTheory.Sigma.SigmaHom {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] :
(i : I) × C i(i : I) × C iType (max w₁ v₁ u₁)

The type of morphisms of a disjoint union of categories: for X : C i and Y : C j, a morphism (i, X) ⟶ (j, Y) if i = j is just a morphism X ⟶ Y, and if i ≠ j there are no such morphisms.

Instances For
    def CategoryTheory.Sigma.SigmaHom.id {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (X : (i : I) × C i) :

    The identity morphism on an object.

    Equations
    Instances For
      def CategoryTheory.Sigma.SigmaHom.comp {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) × C i} {Y : (i : I) × C i} {Z : (i : I) × C i} :

      Composition of sigma homomorphisms.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        theorem CategoryTheory.Sigma.SigmaHom.assoc {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) × C i} {Y : (i : I) × C i} {Z : (i : I) × C i} {W : (i : I) × C i} (f : X Y) (g : Y Z) (h : Z W) :
        theorem CategoryTheory.Sigma.SigmaHom.id_comp {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) × C i} {Y : (i : I) × C i} (f : X Y) :
        theorem CategoryTheory.Sigma.SigmaHom.comp_id {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X : (i : I) × C i} {Y : (i : I) × C i} (f : X Y) :
        Equations
        @[simp]
        theorem CategoryTheory.Sigma.incl_map {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) :
        ∀ {X Y : C i} (a : X Y), (CategoryTheory.Sigma.incl i).map a = CategoryTheory.Sigma.SigmaHom.mk a
        def CategoryTheory.Sigma.incl {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I) :
        CategoryTheory.Functor (C i) ((i : I) × C i)

        The inclusion functor into the disjoint union of categories.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Sigma.incl_obj {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i : I} (X : C i) :
          (CategoryTheory.Sigma.incl i).obj X = { fst := i, snd := X }
          Equations
          • One or more equations did not get rendered due to their size.

          To build a natural transformation over the sigma category, it suffices to specify it restricted to each subcategory.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Sigma.natTrans_app {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor ((i : I) × C i) D} {G : CategoryTheory.Functor ((i : I) × C i) D} (h : (i : I) → CategoryTheory.Functor.comp (CategoryTheory.Sigma.incl i) F CategoryTheory.Functor.comp (CategoryTheory.Sigma.incl i) G) (i : I) (X : C i) :
            (CategoryTheory.Sigma.natTrans h).app { fst := i, snd := X } = (h i).app X
            def CategoryTheory.Sigma.descMap {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (X : (i : I) × C i) (Y : (i : I) × C i) :
            (X Y)((F X.fst).obj X.snd (F Y.fst).obj Y.snd)

            (Implementation). An auxiliary definition to build the functor desc.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CategoryTheory.Sigma.desc_obj {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (X : (i : I) × C i) :
              (CategoryTheory.Sigma.desc F).obj X = (F X.fst).obj X.snd
              def CategoryTheory.Sigma.desc {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) :
              CategoryTheory.Functor ((i : I) × C i) D

              Given a collection of functors F i : C i ⥤ D, we can produce a functor (Σ i, C i) ⥤ D.

              The produced functor desc F satisfies: incl i ⋙ desc F ≅ F i, i.e. restricted to just the subcategory C i, desc F agrees with F i, and it is unique (up to natural isomorphism) with this property.

              This witnesses that the sigma-type is the coproduct in Cat.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Sigma.desc_map_mk {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) {i : I} (X : C i) (Y : C i) (f : X Y) :

                This shows that when desc F is restricted to just the subcategory C i, desc F agrees with F i.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.Sigma.inclDesc_hom_app {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (i : I) (X : C i) :
                  @[simp]
                  theorem CategoryTheory.Sigma.inclDesc_inv_app {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (i : I) (X : C i) :
                  def CategoryTheory.Sigma.descUniq {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (q : CategoryTheory.Functor ((i : I) × C i) D) (h : (i : I) → CategoryTheory.Functor.comp (CategoryTheory.Sigma.incl i) q F i) :

                  If q when restricted to each subcategory C i agrees with F i, then q is isomorphic to desc F.

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Sigma.descUniq_hom_app {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (q : CategoryTheory.Functor ((i : I) × C i) D) (h : (i : I) → CategoryTheory.Functor.comp (CategoryTheory.Sigma.incl i) q F i) (i : I) (X : C i) :
                    (CategoryTheory.Sigma.descUniq F q h).hom.app { fst := i, snd := X } = (h i).hom.app X
                    @[simp]
                    theorem CategoryTheory.Sigma.descUniq_inv_app {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (q : CategoryTheory.Functor ((i : I) × C i) D) (h : (i : I) → CategoryTheory.Functor.comp (CategoryTheory.Sigma.incl i) q F i) (i : I) (X : C i) :
                    (CategoryTheory.Sigma.descUniq F q h).inv.app { fst := i, snd := X } = (h i).inv.app X
                    @[simp]
                    @[simp]
                    def CategoryTheory.Sigma.natIso {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {q₁ : CategoryTheory.Functor ((i : I) × C i) D} {q₂ : CategoryTheory.Functor ((i : I) × C i) D} (h : (i : I) → CategoryTheory.Functor.comp (CategoryTheory.Sigma.incl i) q₁ CategoryTheory.Functor.comp (CategoryTheory.Sigma.incl i) q₂) :
                    q₁ q₂

                    If q₁ and q₂ when restricted to each subcategory C i agree, then q₁ and q₂ are isomorphic.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def CategoryTheory.Sigma.map {I : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : JI) :
                      CategoryTheory.Functor ((j : J) × C (g j)) ((i : I) × C i)

                      A function J → I induces a functor Σ j, C (g j) ⥤ Σ i, C i.

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.Sigma.map_obj {I : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : JI) (j : J) (X : C (g j)) :
                        (CategoryTheory.Sigma.map C g).obj { fst := j, snd := X } = { fst := g j, snd := X }
                        @[simp]
                        theorem CategoryTheory.Sigma.map_map {I : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : JI) {j : J} {X : C (g j)} {Y : C (g j)} (f : X Y) :
                        @[simp]
                        theorem CategoryTheory.Sigma.inclCompMap_hom_app {I : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : JI) (j : J) (X : C (g j)) :
                        (CategoryTheory.Sigma.inclCompMap C g j).hom.app X = CategoryTheory.CategoryStruct.id { fst := g j, snd := X }
                        @[simp]
                        theorem CategoryTheory.Sigma.inclCompMap_inv_app {I : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : JI) (j : J) (X : C (g j)) :
                        (CategoryTheory.Sigma.inclCompMap C g j).inv.app X = CategoryTheory.CategoryStruct.id { fst := g j, snd := X }

                        The functor Sigma.map C g restricted to the subcategory C j acts as the inclusion of g j.

                        Equations
                        Instances For
                          @[simp]
                          theorem CategoryTheory.Sigma.mapId_hom_app (I : Type w₁) (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] :
                          ∀ (x : (i : I) × (fun (i : I) => (fun (i : I) => C (id i)) i) i), (CategoryTheory.Sigma.mapId I C).hom.app x = CategoryTheory.CategoryStruct.id { fst := x.fst, snd := x.snd }
                          @[simp]
                          theorem CategoryTheory.Sigma.mapId_inv_app (I : Type w₁) (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] :
                          ∀ (x : (i : I) × (fun (i : I) => (fun (i : I) => C (id i)) i) i), (CategoryTheory.Sigma.mapId I C).inv.app x = CategoryTheory.CategoryStruct.id { fst := x.fst, snd := x.snd }

                          The functor Sigma.map applied to the identity function is just the identity functor.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Sigma.mapComp_hom_app {I : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} {K : Type w₃} (f : KJ) (g : JI) (X : (i : K) × (fun (i : K) => C (g (f i))) i) :
                            (CategoryTheory.Sigma.mapComp C f g).hom.app X = CategoryTheory.CategoryStruct.id { fst := g (f X.fst), snd := X.snd }
                            @[simp]
                            theorem CategoryTheory.Sigma.mapComp_inv_app {I : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} {K : Type w₃} (f : KJ) (g : JI) (X : (i : K) × (fun (i : K) => C (g (f i))) i) :
                            (CategoryTheory.Sigma.mapComp C f g).inv.app X = CategoryTheory.CategoryStruct.id { fst := g (f X.fst), snd := X.snd }
                            def CategoryTheory.Sigma.mapComp {I : Type w₁} (C : IType u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} {K : Type w₃} (f : KJ) (g : JI) :

                            The functor Sigma.map applied to a composition is a composition of functors.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def CategoryTheory.Sigma.Functor.sigma {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (D i)] (F : (i : I) → CategoryTheory.Functor (C i) (D i)) :
                              CategoryTheory.Functor ((i : I) × C i) ((i : I) × D i)

                              Assemble an I-indexed family of functors into a functor between the sigma types.

                              Equations
                              Instances For
                                def CategoryTheory.Sigma.natTrans.sigma {I : Type w₁} {C : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : IType u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (D i)] {F : (i : I) → CategoryTheory.Functor (C i) (D i)} {G : (i : I) → CategoryTheory.Functor (C i) (D i)} (α : (i : I) → F i G i) :

                                Assemble an I-indexed family of natural transformations into a single natural transformation.

                                Equations
                                Instances For