Documentation

Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Pullbacks in functor categories #

We prove the isomorphism (pullback f g).obj d ≅ pullback (f.app d) (g.app d).

source
def CategoryTheory.Limits.PullbackCone.combine {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} (f : F ⟶ H) (g : G ⟶ H) (c : (X : D) → PullbackCone (f.app X) (g.app X)) (hc : (X : D) → IsLimit (c X)) :
PullbackCone f g

Given functors F G H and natural transformations f : F ⟶ H and g : g : G ⟶ H, together with a collection of limiting pullback cones for each cospan F X ⟶ H X, G X ⟶ H X, we can stitch them together to give a pullback cone for the cospan formed by f and g. combinePullbackConesIsLimit shows that this pullback cone is limiting.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.PullbackCone.combine_π_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} (f : F ⟶ H) (g : G ⟶ H) (c : (X : D) → PullbackCone (f.app X) (g.app X)) (hc : (X : D) → IsLimit (c X)) (j : WalkingCospan) :
    (combine f g c hc).π.app j = Option.rec (CategoryStruct.comp { app := fun (X : D) => (c X).fst, naturality := ⋯ } f) (fun (val : WalkingPair) => WalkingPair.rec { app := fun (X : D) => (c X).fst, naturality := ⋯ } { app := fun (X : D) => (c X).snd, naturality := ⋯ } val) j
    source
    @[simp]
    theorem CategoryTheory.Limits.PullbackCone.combine_pt_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} (f : F ⟶ H) (g : G ⟶ H) (c : (X : D) → PullbackCone (f.app X) (g.app X)) (hc : (X : D) → IsLimit (c X)) {X Y : D} (h : X ⟶ Y) :
    (combine f g c hc).pt.map h = (hc Y).lift { pt := (c X).pt, π := CategoryStruct.comp (c X).π (cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯) }
    source
    @[simp]
    theorem CategoryTheory.Limits.PullbackCone.combine_pt_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} (f : F ⟶ H) (g : G ⟶ H) (c : (X : D) → PullbackCone (f.app X) (g.app X)) (hc : (X : D) → IsLimit (c X)) (X : D) :
    (combine f g c hc).pt.obj X = (c X).pt
    source
    def CategoryTheory.Limits.PullbackCone.combineIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} (f : F ⟶ H) (g : G ⟶ H) (c : (X : D) → PullbackCone (f.app X) (g.app X)) (hc : (X : D) → IsLimit (c X)) :
    IsLimit (combine f g c hc)

    The pullback cone combinePullbackCones is limiting.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def CategoryTheory.Limits.pullbackObjIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) :
      (pullback f g).obj d ≅ pullback (f.app d) (g.app d)

      Evaluating a pullback amounts to taking the pullback of the evaluations.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Limits.pullbackObjIso_hom_comp_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) :
        CategoryStruct.comp (pullbackObjIso f g d).hom (pullback.fst (f.app d) (g.app d)) = (pullback.fst f g).app d
        source
        @[simp]
        theorem CategoryTheory.Limits.pullbackObjIso_hom_comp_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) {Z : C} (h : F.obj d ⟶ Z) :
        CategoryStruct.comp (pullbackObjIso f g d).hom (CategoryStruct.comp (pullback.fst (f.app d) (g.app d)) h) = CategoryStruct.comp ((pullback.fst f g).app d) h
        source
        @[simp]
        theorem CategoryTheory.Limits.pullbackObjIso_hom_comp_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) :
        CategoryStruct.comp (pullbackObjIso f g d).hom (pullback.snd (f.app d) (g.app d)) = (pullback.snd f g).app d
        source
        @[simp]
        theorem CategoryTheory.Limits.pullbackObjIso_hom_comp_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) {Z : C} (h : G.obj d ⟶ Z) :
        CategoryStruct.comp (pullbackObjIso f g d).hom (CategoryStruct.comp (pullback.snd (f.app d) (g.app d)) h) = CategoryStruct.comp ((pullback.snd f g).app d) h
        source
        @[simp]
        theorem CategoryTheory.Limits.pullbackObjIso_inv_comp_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) :
        CategoryStruct.comp (pullbackObjIso f g d).inv ((pullback.fst f g).app d) = pullback.fst (f.app d) (g.app d)
        source
        @[simp]
        theorem CategoryTheory.Limits.pullbackObjIso_inv_comp_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) {Z : C} (h : F.obj d ⟶ Z) :
        CategoryStruct.comp (pullbackObjIso f g d).inv (CategoryStruct.comp ((pullback.fst f g).app d) h) = CategoryStruct.comp (pullback.fst (f.app d) (g.app d)) h
        source
        @[simp]
        theorem CategoryTheory.Limits.pullbackObjIso_inv_comp_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) :
        CategoryStruct.comp (pullbackObjIso f g d).inv ((pullback.snd f g).app d) = pullback.snd (f.app d) (g.app d)
        source
        @[simp]
        theorem CategoryTheory.Limits.pullbackObjIso_inv_comp_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D) {Z : C} (h : G.obj d ⟶ Z) :
        CategoryStruct.comp (pullbackObjIso f g d).inv (CategoryStruct.comp ((pullback.snd f g).app d) h) = CategoryStruct.comp (pullback.snd (f.app d) (g.app d)) h
        source
        noncomputable def CategoryTheory.Limits.pushoutObjIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) :
        (pushout f g).obj d ≅ pushout (f.app d) (g.app d)

        Evaluating a pushout amounts to taking the pushout of the evaluations.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Limits.inl_comp_pushoutObjIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) :
          CategoryStruct.comp ((pushout.inl f g).app d) (pushoutObjIso f g d).hom = pushout.inl (f.app d) (g.app d)
          source
          @[simp]
          theorem CategoryTheory.Limits.inl_comp_pushoutObjIso_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) {Z : C} (h : pushout (f.app d) (g.app d) ⟶ Z) :
          CategoryStruct.comp ((pushout.inl f g).app d) (CategoryStruct.comp (pushoutObjIso f g d).hom h) = CategoryStruct.comp (pushout.inl (f.app d) (g.app d)) h
          source
          @[simp]
          theorem CategoryTheory.Limits.inr_comp_pushoutObjIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) :
          CategoryStruct.comp ((pushout.inr f g).app d) (pushoutObjIso f g d).hom = pushout.inr (f.app d) (g.app d)
          source
          @[simp]
          theorem CategoryTheory.Limits.inr_comp_pushoutObjIso_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) {Z : C} (h : pushout (f.app d) (g.app d) ⟶ Z) :
          CategoryStruct.comp ((pushout.inr f g).app d) (CategoryStruct.comp (pushoutObjIso f g d).hom h) = CategoryStruct.comp (pushout.inr (f.app d) (g.app d)) h
          source
          @[simp]
          theorem CategoryTheory.Limits.inl_comp_pushoutObjIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) :
          CategoryStruct.comp (pushout.inl (f.app d) (g.app d)) (pushoutObjIso f g d).inv = (pushout.inl f g).app d
          source
          @[simp]
          theorem CategoryTheory.Limits.inl_comp_pushoutObjIso_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) {Z : C} (h : (pushout f g).obj d ⟶ Z) :
          CategoryStruct.comp (pushout.inl (f.app d) (g.app d)) (CategoryStruct.comp (pushoutObjIso f g d).inv h) = CategoryStruct.comp ((pushout.inl f g).app d) h
          source
          @[simp]
          theorem CategoryTheory.Limits.inr_comp_pushoutObjIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) :
          CategoryStruct.comp (pushout.inr (f.app d) (g.app d)) (pushoutObjIso f g d).inv = (pushout.inr f g).app d
          source
          @[simp]
          theorem CategoryTheory.Limits.inr_comp_pushoutObjIso_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor D C} [HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D) {Z : C} (h : (pushout f g).obj d ⟶ Z) :
          CategoryStruct.comp (pushout.inr (f.app d) (g.app d)) (CategoryStruct.comp (pushoutObjIso f g d).inv h) = CategoryStruct.comp ((pushout.inr f g).app d) h