GroupoidModel.Grothendieck.IsPullback

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

Equations

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

Instances For

@[simp]

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

((toPCat A).obj x).base = A.obj x.base

source

@[simp]

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

((toPCat A).obj x).fiber = x.fiber

source

@[simp]

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

((toPCat A).map f).base = A.map f.base

source

@[simp]

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

((toPCat A).map f).fiber = f.fiber

source

theorem CategoryTheory.Grothendieck.toPCat_forgetToCat {Γ : Type u} [Category.{v, u} Γ] (A : Functor Γ Cat) :

(toPCat A).comp PCat.forgetToCat = (forget A).comp A

source

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.pt {C : Type u_1} [Category.{u_2, u_1} C] (fst : Functor C PCat) (x : C) :

↑((Functor.id Cat).obj (fst.obj x).base)

Equations

CategoryTheory.Grothendieck.IsPullback.pt fst x = (fst.obj x).fiber

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.Grothendieck.IsPullback.point {C : Type u_1} [Category.{u_2, u_1} C] (fst : Functor C PCat) {x y : C} (f : x ⟶ y) :

(PCat.forgetToCat.map (fst.map f)).obj (pt fst x) ⟶ pt fst y

Equations

CategoryTheory.Grothendieck.IsPullback.point fst f = (fst.map f).fiber

Instances For

source

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

↑(A.obj (snd.obj x))

Equations

CategoryTheory.Grothendieck.IsPullback.liftObjFiber w x = ((CategoryTheory.eqToHom w).app x).obj (CategoryTheory.Grothendieck.IsPullback.pt fst x)

Instances For

source

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

((snd.comp A).map f).obj (liftObjFiber w x) ⟶ liftObjFiber w y

Equations

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

Instances For

source

theorem CategoryTheory.Grothendieck.IsPullback.liftMapFiber_id {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_1} [Category.{u_2, u_1} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) (x : C) :

liftMapFiber w (CategoryStruct.id x) = eqToHom ⋯

source

theorem CategoryTheory.Grothendieck.IsPullback.liftMapFiber_comp {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_1} [Category.{u_2, u_1} C] {fst : Functor C PCat} {snd : Functor C Γ} (w : fst.comp PCat.forgetToCat = snd.comp A) {x y z : C} (f : x ⟶ y) (g : y ⟶ z) :

liftMapFiber w (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map (snd.map g)).map (liftMapFiber w f)) (liftMapFiber w g))

source

def CategoryTheory.Grothendieck.IsPullback.lift {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_1} [Category.{u_2, u_1} 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.

Instances For

source

@[simp]

theorem CategoryTheory.Grothendieck.IsPullback.lift_obj_base {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_1} [Category.{u_2, u_1} C] (fst : Functor C PCat) (snd : Functor C Γ) (w : fst.comp PCat.forgetToCat = snd.comp A) (x : C) :

((lift fst snd w).obj x).base = snd.obj x

source

@[simp]

theorem CategoryTheory.Grothendieck.IsPullback.lift_obj_fiber {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_1} [Category.{u_2, u_1} C] (fst : Functor C PCat) (snd : Functor C Γ) (w : fst.comp PCat.forgetToCat = snd.comp A) (x : C) :

((lift fst snd w).obj x).fiber = liftObjFiber w x

source

@[simp]

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

((lift fst snd w).map f).base = snd.map f

source

@[simp]

theorem CategoryTheory.Grothendieck.IsPullback.lift_map_fiber {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_1} [Category.{u_2, u_1} C] (fst : Functor C PCat) (snd : Functor C Γ) (w : fst.comp PCat.forgetToCat = snd.comp A) {x y : C} (f : x ⟶ y) :

((lift fst snd w).map f).fiber = liftMapFiber w f

source

@[simp]

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

(lift fst snd w).comp (forget A) = snd

source

@[simp]

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

(lift fst snd w).comp (toPCat A) = fst

source

theorem CategoryTheory.Grothendieck.IsPullback.lift_uniq {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_1} [Category.{u_2, u_1} 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

source

theorem CategoryTheory.Grothendieck.IsPullback.hom_ext {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_1} [Category.{u_2, u_1} C] {m n : Functor C (Grothendieck A)} (hl : m.comp (toPCat A) = n.comp (toPCat A)) (hr : m.comp (forget A) = n.comp (forget A)) :

m = n

source

def CategoryTheory.Grothendieck.IsPullback.aux {Γ : Type u} [Category.{v, u} Γ] {A : Functor Γ Cat} {C : Type u_2} [inst : Category.{u_3, u_2} C] (Cn : Functor C PCat) (Cw : Functor C Γ) (hC : Cn.comp (forget (Functor.id Cat)) = Cw.comp A) :

(lift : Functor C (Grothendieck A)) ×' lift.comp (toPCat A) = Cn ∧ lift.comp (forget A) = Cw ∧ ∀ {l0 l1 : Functor C (Grothendieck A)}, l0.comp (toPCat A) = l1.comp (toPCat A) → l0.comp (forget A) = l1.comp (forget A) → l0 = l1

Equations

CategoryTheory.Grothendieck.IsPullback.aux Cn Cw hC = ⟨CategoryTheory.Grothendieck.IsPullback.lift Cn Cw hC, ⋯⟩

Instances For

source

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

(toPCat A).IsPullback (forget A) (forget (Functor.id Cat)) A

The following square is a (meta-theoretic) pullback of functors Grothendieck A --- toPCat ----> PCat | | | | Grothendieck.forget PCat.forgetToCat | | v v Γ--------------A---------> Cat

Equations

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

Instances For