Documentation

GroupoidModel.Pointed.IsPullback

Pointed groupoids as the pullback of pointed categories #

This file shows that PGrpd.forgetToGrpd is the pullback along Grpd.forgetToCat of PCat.forgetToCat.

Main statements #

source
def CategoryTheory.PGrpd.isoGrothendieckForgetToCatHom :
Functor PGrpd (Grothendieck Grpd.forgetToCat)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.PGrpd.isoGrothendieckForgetToCatHom_obj_base (x : PGrpd) :
    (isoGrothendieckForgetToCatHom.obj x).base = Grpd.of ↑x
    source
    @[simp]
    theorem CategoryTheory.PGrpd.isoGrothendieckForgetToCatHom_obj_fiber (x : PGrpd) :
    (isoGrothendieckForgetToCatHom.obj x).fiber = PointedGroupoid.pt
    source
    @[simp]
    theorem CategoryTheory.PGrpd.isoGrothendieckForgetToCatHom_map_base {X✝ Y✝ : PGrpd} (f : X✝ ⟶ Y✝) :
    (isoGrothendieckForgetToCatHom.map f).base = f.toFunctor
    source
    @[simp]
    theorem CategoryTheory.PGrpd.isoGrothendieckForgetToCatHom_map_fiber {X✝ Y✝ : PGrpd} (f : X✝ ⟶ Y✝) :
    (isoGrothendieckForgetToCatHom.map f).fiber = f.point
    source
    def CategoryTheory.PGrpd.isoGrothendieckForgetToCatInv :
    Functor (Grothendieck Grpd.forgetToCat) PGrpd
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.PGrpd.isoGrothendieckForgetToCat :
      Cat.of PGrpd ≅ Cat.of (Grothendieck Grpd.forgetToCat)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.PGrpd.isoGrothendieckForgetToCat_inv :
        isoGrothendieckForgetToCat.inv = isoGrothendieckForgetToCatInv
        source
        @[simp]
        theorem CategoryTheory.PGrpd.isoGrothendieckForgetToCat_hom :
        isoGrothendieckForgetToCat.hom = isoGrothendieckForgetToCatHom
        source
        def CategoryTheory.PGrpd.IsMegaPullback.comm_sq :
        forgetToPCat.comp PCat.forgetToCat = forgetToGrpd.comp Grpd.forgetToCat
        Equations
        Instances For
          source
          def CategoryTheory.PGrpd.IsMegaPullback.lift {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (snd : Functor C Grpd) (w : fst.comp PCat.forgetToCat = snd.comp Grpd.forgetToCat) :
          Functor C PGrpd
          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.PGrpd.IsMegaPullback.fac_left {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (snd : Functor C Grpd) (w : fst.comp PCat.forgetToCat = snd.comp Grpd.forgetToCat) :
            (lift fst snd w).comp forgetToPCat = fst
            source
            @[simp]
            theorem CategoryTheory.PGrpd.IsMegaPullback.fac_right {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (snd : Functor C Grpd) (w : fst.comp PCat.forgetToCat = snd.comp Grpd.forgetToCat) :
            (lift fst snd w).comp forgetToGrpd = snd
            source
            theorem CategoryTheory.PGrpd.IsMegaPullback.lift_uniq {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (snd : Functor C Grpd) (w : fst.comp PCat.forgetToCat = snd.comp Grpd.forgetToCat) (m : Functor C PGrpd) (hl : m.comp forgetToPCat = fst) (hr : m.comp forgetToGrpd = snd) :
            m = lift fst snd w
            source
            theorem CategoryTheory.PGrpd.IsPullback.isPullback_forgetToGrpd_uLiftGrothendieckForget_commSq :
            CommSq (isoGrothendieckForgetToCat ≪≫ Cat.ULift_iso_self.symm).hom (Cat.homOf forgetToGrpd) (Grothendieck.IsPullback.uLiftGrothendieckForget Grpd.forgetToCat) Cat.ULift_iso_self.symm.hom
            source
            theorem CategoryTheory.PGrpd.IsPullback.isPullback_forgetToGrpd_uLiftGrothendieckForget :
            IsPullback (isoGrothendieckForgetToCat ≪≫ Cat.ULift_iso_self.symm).hom (Cat.homOf forgetToGrpd) (Grothendieck.IsPullback.uLiftGrothendieckForget Grpd.forgetToCat) Cat.ULift_iso_self.inv

            Here we show the following pullback square in Cat.{u,u+1}, where ↑ denotes some kind of ULift operation into Cat.{u,u+1}. Note that these ULifts "do nothing" since the categories are already at the target universe level. PGrpd.{u,u} -----≅--->↑Grothendieck Grpd.forgetToCat.{u,u} | | | | PGrpd.forgetToGrpd ↑ Grothendieck.forget | | v v Grpd.{u,u}------≅---->↑Grpd.{u,u}

            source
            theorem CategoryTheory.PGrpd.IsPullback.isPullback_uLiftGrothendieckForget_forgetToGrpd :
            IsPullback (Cat.ULift_iso_self ≪≫ isoGrothendieckForgetToCat.symm).hom (Grothendieck.IsPullback.uLiftGrothendieckForget Grpd.forgetToCat) (Cat.homOf forgetToGrpd) Cat.ULift_iso_self.hom
            source
            theorem CategoryTheory.PGrpd.IsPullback.isPullback_grothendieckForget_forgetToCat :
            IsPullback (Grothendieck.IsPullback.uLiftToPCat Grpd.forgetToCat) (Grothendieck.IsPullback.uLiftGrothendieckForget Grpd.forgetToCat) Grothendieck.IsPullback.uLiftPCatForgetToCat (Grothendieck.IsPullback.uLiftA Grpd.forgetToCat)
            source
            theorem CategoryTheory.PGrpd.IsPullback.isPullback_uLiftPCatForgetToCat_forgetToCat :
            IsPullback Cat.ULift_iso_self.hom Grothendieck.IsPullback.uLiftPCatForgetToCat (Cat.homOf PCat.forgetToCat) Cat.ULift_iso_self.hom

            Here we (roughly) show the following pullback square in Cat.{u,u+1}, where ↑ denotes some kind of ULift operation into Cat.{u,u+1} ↑PCat ---------≅-------> PCat | | | | ↑PCat.forgetToCat PCat.forgetToCat | | v v ↑Cat-----------≅---------->Cat

            source
            theorem CategoryTheory.PGrpd.isPullback_forgetToGrpd_forgetToCat :
            IsPullback (Cat.homOf forgetToPCat) (Cat.homOf forgetToGrpd) (Cat.homOf PCat.forgetToCat) (Cat.homOf Grpd.forgetToCat)

            The following square is a pullback

             PGrpd ------ toPCat ------> PCat
   |                           |
   |                           |

            PGrpd.forgetToGrpd PCat.forgetToCat | | v v Grpd------forgetToCat------->Cat