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
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