This file builds API for showing that a presheaf diagram is a pullback by its universal property among representable cones.

structure CategoryTheory.Limits.RepCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor J (Functor Cᵒᵖ (Type v₃))) : Type (max (max u₁ u₃) v₃)

A c : RepCone F is:

• an object c.pt and
• a natural transformation c.π : yoneda.obj c.pt ⟶ F from the constant yoneda.obj c.pt functor to F.

• pt : C

  An object of C

• π : (Functor.const J).obj (yoneda.obj self.pt) ⟶ F

  A natural transformation from the constant functor at X to F

@[reducible]

def CategoryTheory.Limits.RepCone.cone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} (s : RepCone F) : Cone F

Equations

• s.cone = { pt := CategoryTheory.yoneda.obj s.pt, π := s.π }

structure CategoryTheory.Limits.RepIsLimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} (t : Cone F) : Type (max (max u₁ u₃) v₃)

• lift (s : RepCone F) : s.cone.pt ⟶ t.pt
• fac (s : RepCone F) (j : J) : CategoryStruct.comp (self.lift s) (t.π.app j) = s.cone.π.app j
• uniq (s : RepCone F) (m : s.cone.pt ⟶ t.pt) : (∀ (j : J), CategoryStruct.comp m (t.π.app j) = s.cone.π.app j) → m = self.lift s

  It is the unique such map to do this

def CategoryTheory.Limits.repConeOfConeMap {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} (s : Cone F) (c : C) (x' : yoneda.obj c ⟶ s.pt) : RepCone F

Equations

• CategoryTheory.Limits.repConeOfConeMap s c x' = { pt := c, π := { app := fun (j : J) => CategoryTheory.CategoryStruct.comp x' (s.π.app j), naturality := ⋯ } }

def CategoryTheory.Limits.RepIsLimit.lift' {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} {t : Cone F} (P : RepIsLimit t) {s : Cone F} (c : C) (x' : yoneda.obj c ⟶ s.pt) : yoneda.obj c ⟶ t.pt

Equations

• P.lift' c x' = P.lift (CategoryTheory.Limits.repConeOfConeMap s c x')

@[simp]

theorem CategoryTheory.Limits.RepIsLimit.lift'_naturality {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} {t : Cone F} (P : RepIsLimit t) {s : Cone F} {c d : C} (f : c ⟶ d) (x' : yoneda.obj d ⟶ s.pt) : P.lift' c (CategoryStruct.comp (yoneda.map f) x') = CategoryStruct.comp (yoneda.map f) (P.lift' d x')

def CategoryTheory.Limits.RepIsLimit.lift''_app {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} {t : Cone F} (P : RepIsLimit t) (s : Cone F) (c : C) : s.pt.obj (Opposite.op c) → t.pt.obj (Opposite.op c)

Equations

• P.lift''_app s c = ⇑CategoryTheory.yonedaEquiv ∘ P.lift' c ∘ ⇑CategoryTheory.yonedaEquiv.symm

theorem CategoryTheory.Limits.RepIsLimit.lift''_app_naturality {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} {t : Cone F} (P : RepIsLimit t) {s : Cone F} {c d : C} (f : c ⟶ d) : CategoryStruct.comp (s.pt.map f.op) (P.lift''_app s c) = CategoryStruct.comp (P.lift''_app s d) (t.pt.map (Opposite.op f))

def CategoryTheory.Limits.RepIsLimit.lift'' {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} {t : Cone F} (P : RepIsLimit t) (s : Cone F) : s.pt ⟶ t.pt

Equations

• P.lift'' s = { app := fun (c : Cᵒᵖ) => P.lift''_app s (Opposite.unop c), naturality := ⋯ }

theorem CategoryTheory.Limits.RepIsLimit.fac_ext {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} {t : Cone F} (P : RepIsLimit t) (s : Cone F) (j : J) (c : C) (x : s.pt.obj (Opposite.op c)) : (CategoryStruct.comp (P.lift'' s) (t.π.app j)).app (Opposite.op c) x = (s.π.app j).app (Opposite.op c) x

theorem CategoryTheory.Limits.RepIsLimit.uniq_ext {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} {t : Cone F} (P : RepIsLimit t) (s : Cone F) (m : s.pt ⟶ t.pt) (hm : ∀ (j : J), CategoryStruct.comp m (t.π.app j) = s.π.app j) (c : C) (x : s.pt.obj (Opposite.op c)) : m.app (Opposite.op c) x = (P.lift'' s).app (Opposite.op c) x

def CategoryTheory.Limits.RepIsLimit.IsLimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J (Functor Cᵒᵖ (Type v₃))} {t : Cone F} (P : RepIsLimit t) : Limits.IsLimit t

Equations

• P.IsLimit = { lift := P.lift'', fac := ⋯, uniq := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.Limits.RepPullbackCone {C : Type u₃} [Category.{v₃, u₃} C] {X Y Z : Functor Cᵒᵖ (Type v₃)} (f : X ⟶ Z) (g : Y ⟶ Z) : Type (max u₃ v₃)

Equations

• CategoryTheory.Limits.RepPullbackCone f g = CategoryTheory.Limits.RepCone (CategoryTheory.Limits.cospan f g)

def CategoryTheory.Limits.RepPullbackCone.mk {C : Type u₃} [Category.{v₃, u₃} C] {X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} (W : C) (fst : yoneda.obj W ⟶ X) (snd : yoneda.obj W ⟶ Y) (h : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : RepPullbackCone f g

Equations

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

def CategoryTheory.Limits.RepPullbackCone.pullbackCone {C : Type u₃} [Category.{v₃, u₃} C] {X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} (t : RepPullbackCone f g) : PullbackCone f g

Equations

• t.pullbackCone = { pt := CategoryTheory.yoneda.obj t.pt, π := t.π }

@[reducible, inline]

abbrev CategoryTheory.Limits.RepPullbackCone.fst {C : Type u₃} [Category.{v₃, u₃} C] {X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} (t : RepPullbackCone f g) : yoneda.obj t.pt ⟶ X

The first projection of a pullback cone.

Equations

• t.fst = t.pullbackCone.fst

@[reducible, inline]

abbrev CategoryTheory.Limits.RepPullbackCone.snd {C : Type u₃} [Category.{v₃, u₃} C] {X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} (t : RepPullbackCone f g) : yoneda.obj t.pt ⟶ Y

The second projection of a pullback cone.

Equations

• t.snd = t.pullbackCone.snd

theorem CategoryTheory.Limits.RepPullbackCone.condition {C : Type u₃} [Category.{v₃, u₃} C] {X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} (t : RepPullbackCone f g) : CategoryStruct.comp t.fst f = CategoryStruct.comp t.snd g

theorem CategoryTheory.Limits.RepPullbackCone.condition_assoc {C : Type u₃} [Category.{v₃, u₃} C] {X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} (t : RepPullbackCone f g) {Z✝ : Functor Cᵒᵖ (Type v₃)} (h : Z ⟶ Z✝) : CategoryStruct.comp t.fst (CategoryStruct.comp f h) = CategoryStruct.comp t.snd (CategoryStruct.comp g h)

def CategoryTheory.Limits.RepPullbackCone.repIsLimitAux {C : Type u₃} [Category.{v₃, u₃} C] {X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) (lift : (s : RepPullbackCone f g) → yoneda.obj s.pt ⟶ t.pt) (fac_left : ∀ (s : RepPullbackCone f g), CategoryStruct.comp (lift s) t.fst = s.fst) (fac_right : ∀ (s : RepPullbackCone f g), CategoryStruct.comp (lift s) t.snd = s.snd) (uniq : ∀ (s : RepPullbackCone f g) (m : yoneda.obj s.pt ⟶ t.pt), (∀ (j : WalkingCospan), CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s) : RepIsLimit t

Equations

• CategoryTheory.Limits.RepPullbackCone.repIsLimitAux t lift fac_left fac_right uniq = { lift := lift, fac := ⋯, uniq := uniq }

def CategoryTheory.Limits.RepPullbackCone.RepIsLimit.mk {C : Type u₃} [Category.{v₃, u₃} C] {W X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} {fst : W ⟶ X} {snd : W ⟶ Y} (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) (lift : (s : RepPullbackCone f g) → yoneda.obj s.pt ⟶ W) (fac_left : ∀ (s : RepPullbackCone f g), CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : RepPullbackCone f g), CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : RepPullbackCone f g) (m : yoneda.obj s.pt ⟶ W), CategoryStruct.comp m fst = s.fst → CategoryStruct.comp m snd = s.snd → m = lift s) : IsLimit (PullbackCone.mk fst snd eq)

To show that a PullbackCone in a presheaf category constructed using PullbackCone.mk is a limit cone, it suffices to show its universal property among representable cones.

Equations

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

theorem CategoryTheory.Limits.RepPullbackCone.is_pullback {C : Type u₃} [Category.{v₃, u₃} C] {W X Y Z : Functor Cᵒᵖ (Type v₃)} {f : X ⟶ Z} {g : Y ⟶ Z} {fst : W ⟶ X} {snd : W ⟶ Y} (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) (lift : (s : RepPullbackCone f g) → yoneda.obj s.pt ⟶ W) (fac_left : ∀ (s : RepPullbackCone f g), CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : RepPullbackCone f g), CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : RepPullbackCone f g) (m : yoneda.obj s.pt ⟶ W), CategoryStruct.comp m fst = s.fst → CategoryStruct.comp m snd = s.snd → m = lift s) : IsPullback fst snd f g