def CategoryTheory.Grothendieck.toPCatObj {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (x : Grothendieck A) : PCat

Equations

• x.toPCatObj = { α := ↑(A.obj x.base), str := CategoryTheory.PointedCategory.of (↑(A.obj x.base)) x.fiber }

@[simp]

theorem CategoryTheory.Grothendieck.toPCatObj_α {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (x : Grothendieck A) : ↑x.toPCatObj = ↑(A.obj x.base)

@[simp]

theorem CategoryTheory.Grothendieck.toPCatObj_str {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (x : Grothendieck A) : x.toPCatObj.str = PointedCategory.of (↑(A.obj x.base)) x.fiber

def CategoryTheory.Grothendieck.toPCatMap {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {x y : Grothendieck A} (f : x ⟶ y) : x.toPCatObj ⟶ y.toPCatObj

Equations

• CategoryTheory.Grothendieck.toPCatMap f = { toFunctor := A.map f.base, point := f.fiber }

def CategoryTheory.Grothendieck.toPCat {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : Functor (Grothendieck A) PCat

Equations

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

theorem CategoryTheory.Grothendieck.toPCat_comp_forgetPoint {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : (toPCat A).comp PCat.forgetToCat = (forget A).comp A

theorem CategoryTheory.Grothendieck.toPCatObj_fiber_inj {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) {x y : Grothendieck A} (h : HEq PointedCategory.pt PointedCategory.pt) : HEq x.fiber y.fiber

theorem CategoryTheory.Grothendieck.comm_sq {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : (toPCat A).comp PCat.forgetToCat = (forget A).comp A

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsMegaPullback.pt {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (x : C) : ↑(fst.obj x)

Equations

• CategoryTheory.Grothendieck.IsMegaPullback.pt fst x = CategoryTheory.PointedCategory.pt

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsMegaPullback.point {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) {x y : C} (f : x ⟶ y) : (fst.map f).obj (pt fst x) ⟶ pt fst y

Equations

• CategoryTheory.Grothendieck.IsMegaPullback.point fst f = (fst.map f).point

def CategoryTheory.Grothendieck.IsMegaPullback.lift_obj {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) (x : C) : Grothendieck A

Equations

• CategoryTheory.Grothendieck.IsMegaPullback.lift_obj w x = { base := snd.obj x, fiber := ((CategoryTheory.eqToHom w).app x).obj (CategoryTheory.Grothendieck.IsMegaPullback.pt fst x) }

def CategoryTheory.Grothendieck.IsMegaPullback.lift_map {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {x y : C} (f : x ⟶ y) : lift_obj w x ⟶ lift_obj w y

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_map_base {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {x y : C} (f : x ⟶ y) : (lift_map w f).base = snd.map f

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_map_fiber {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {x y : C} (f : x ⟶ y) : (lift_map w f).fiber = CategoryStruct.comp ((eqToHom ⋯).app (pt fst x)) (((eqToHom w).app y).map (point fst f))

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_map_fiber_pf3 {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {y : C} : Cat.of ↑(fst.obj y) = A.obj (snd.obj y)

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_map_fiber_pf2 {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {x y : C} (f : x ⟶ y) : (A.map (snd.map f)).obj (((eqToHom w).app x).obj (pt fst x)) = (eqToHom ⋯).obj ((fst.map f).obj (pt fst x))

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_map_fiber_pf0 {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {y : C} : (eqToHom ⋯).obj (pt fst y) = ((eqToHom w).app y).obj (pt fst y)

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_map_fiber_pf1 {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {x y : C} (f : x ⟶ y) : ((fst.map f).obj (pt fst x) ⟶ pt fst y) = ((eqToHom ⋯).obj ((fst.map f).obj (pt fst x)) ⟶ (eqToHom ⋯).obj (pt fst y))

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_map_fiber' {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {x y : C} (f : x ⟶ y) : (lift_map w f).fiber = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (cast ⋯ (point fst f)) (eqToHom ⋯))

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_aux {C D : Cat} {X Y : ↑C} (pf1 : C = D) (pf2 : X = Y) (pf3 : (eqToHom pf1).obj X = (eqToHom pf1).obj Y) : HEq (eqToHom pf2) (eqToHom pf3)

def CategoryTheory.Grothendieck.IsMegaPullback.lift {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (snd : Functor C Γ) (w : fst.comp PCat.forgetToCat = snd.comp A) : Functor C (Grothendieck A)

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.IsMegaPullback.fac_right {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (snd : Functor C Γ) (w : fst.comp PCat.forgetToCat = snd.comp A) : (lift fst snd w).comp (forget A) = snd

@[simp]

theorem CategoryTheory.Grothendieck.IsMegaPullback.fac_left {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (snd : Functor C Γ) (w : fst.comp PCat.forgetToCat = snd.comp A) : (lift fst snd w).comp (toPCat A) = fst

theorem CategoryTheory.Grothendieck.IsMegaPullback.lift_uniq {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u₂} [Category.{v₂, u₂} C] (fst : Functor C PCat) (snd : Functor C Γ) (w : fst.comp PCat.forgetToCat = snd.comp A) (m : Functor C (Grothendieck A)) (hl : m.comp (toPCat A) = fst) (hr : m.comp (forget A) = snd) : m = lift fst snd w

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.uLiftGrothendieck {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : Cat

Equations

• CategoryTheory.Grothendieck.IsPullback.uLiftGrothendieck A = CategoryTheory.Cat.ofULift (CategoryTheory.Grothendieck A)

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.uLiftGrothendieckForget {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : uLiftGrothendieck A ⟶ Cat.ofULift Γ

Equations

• CategoryTheory.Grothendieck.IsPullback.uLiftGrothendieckForget A = CategoryTheory.ULift.downFunctor.comp ((CategoryTheory.Grothendieck.forget A).comp CategoryTheory.ULift.upFunctor)

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.uLiftCat : Cat

Equations

• CategoryTheory.Grothendieck.IsPullback.uLiftCat = CategoryTheory.Cat.ofULift CategoryTheory.Cat

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.uLiftPCat : Cat

Equations

• CategoryTheory.Grothendieck.IsPullback.uLiftPCat = CategoryTheory.Cat.ofULift CategoryTheory.PCat

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.uLiftPCatForgetToCat : uLiftPCat ⟶ uLiftCat

Equations

• CategoryTheory.Grothendieck.IsPullback.uLiftPCatForgetToCat = CategoryTheory.ULift.downFunctor.comp (CategoryTheory.PCat.forgetToCat.comp CategoryTheory.ULift.upFunctor)

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.uLiftToPCat {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : uLiftGrothendieck A ⟶ uLiftPCat

Equations

• CategoryTheory.Grothendieck.IsPullback.uLiftToPCat A = CategoryTheory.ULift.downFunctor.comp ((CategoryTheory.Grothendieck.toPCat A).comp CategoryTheory.ULift.upFunctor)

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.uLiftA {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : Functor ↑(Cat.ofULift Γ) ↑uLiftCat

Equations

• CategoryTheory.Grothendieck.IsPullback.uLiftA A = CategoryTheory.ULift.downFunctor.comp (A.comp CategoryTheory.ULift.upFunctor)

theorem CategoryTheory.Grothendieck.IsPullback.comm_sq {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} : CategoryStruct.comp (uLiftToPCat A) uLiftPCatForgetToCat = CategoryStruct.comp (uLiftGrothendieckForget A) (uLiftA A)

def CategoryTheory.Grothendieck.IsPullback.cone {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.pt' {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {s : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)} (x : ↑s.pt) : ↑(ULift.downFunctor.obj (s.fst.obj x))

Equations

• CategoryTheory.Grothendieck.IsPullback.pt' x = CategoryTheory.PointedCategory.pt

theorem CategoryTheory.Grothendieck.IsPullback.condition' {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {s : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)} : Functor.comp s.fst (ULift.downFunctor.comp PCat.forgetToCat) = Functor.comp s.snd (ULift.downFunctor.comp A)

def CategoryTheory.Grothendieck.IsPullback.lift {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (s : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)) : Functor (↑s.pt) (Grothendieck A)

Equations

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

def CategoryTheory.Grothendieck.IsPullback.lift' {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (s : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)) : s.pt ⟶ uLiftGrothendieck A

Equations

• CategoryTheory.Grothendieck.IsPullback.lift' s = (CategoryTheory.Grothendieck.IsPullback.lift s).comp CategoryTheory.ULift.upFunctor

theorem CategoryTheory.Grothendieck.IsPullback.fac_left {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (s : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)) : (lift s).comp ((toPCat A).comp ULift.upFunctor) = s.fst

theorem CategoryTheory.Grothendieck.IsPullback.fac_right {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (s : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)) : (lift s).comp ((forget A).comp ULift.upFunctor) = s.snd

theorem CategoryTheory.Grothendieck.IsPullback.lift_uniq {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (s : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)) (m : Functor (↑s.pt) (Grothendieck A)) (hl : m.comp (toPCat A) = Functor.comp s.fst ULift.downFunctor) (hr : m.comp (forget A) = Functor.comp s.snd ULift.downFunctor) : m = lift s

theorem CategoryTheory.Grothendieck.IsPullback.lift_uniq' {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} (s : Limits.PullbackCone uLiftPCatForgetToCat (uLiftA A)) (m : s.pt ⟶ uLiftGrothendieck A) (hl : CategoryStruct.comp m (uLiftToPCat A) = s.fst) (hr : CategoryStruct.comp m (uLiftGrothendieckForget A) = s.snd) : m = lift' s

def CategoryTheory.Grothendieck.IsPullback.isLimit {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : Limits.IsLimit (cone A)

Equations

• CategoryTheory.Grothendieck.IsPullback.isLimit A = CategoryTheory.Limits.PullbackCone.IsLimit.mk ⋯ CategoryTheory.Grothendieck.IsPullback.lift' ⋯ ⋯ ⋯

theorem CategoryTheory.Grothendieck.isPullback {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) : IsPullback (IsPullback.uLiftToPCat A) (IsPullback.uLiftGrothendieckForget A) IsPullback.uLiftPCatForgetToCat (IsPullback.uLiftA A)