Leibniz Constructions

Let F : C₁ ⥤ C₂ ⥤ C₃. Given morphisms f₁ : X₁ ⟶ Y₁ in C₁ and f₂ : X₂ ⟶ Y₂ in C₂, we introduce a structure F.PushoutObjObj f₁ f₂ which contains the data of a pushout of (F.obj Y₁).obj X₂ and (F.obj X₁).obj Y₂ along (F.obj X₁).obj X₂. If sq₁₂ : F.PushoutObjObj f₁ f₂, we have a canonical "inclusion" sq₁₂.ι : sq₁₂.pt ⟶ (F.obj Y₁).obj Y₂.

If C₃ has pushouts, then we define the Leibniz pushout (often called pushout-product) as the canonical inclusion (PushoutObjObj.ofHasPushout F f₁ f₂).ι. This defines a bifunctor F.leibnizPushout : Arrow C₁ ⥤ Arrow C₂ ⥤ Arrow C₃.

Similarly, if we have a bifunctor G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂, and morphisms f₁ : X₁ ⟶ Y₁ in C₁ and f₃ : X₃ ⟶ Y₃ in C₃, we introduce a structure F.PullbackObjObj f₁ f₃ which contains the data of a pullback of (G.obj (op X₁)).obj X₃ and (G.obj (op Y₁)).obj Y₃ over (G.obj (op X₁)).obj Y₃. If sq₁₃ : F.PullbackObjObj f₁ f₃, we have a canonical projection sq₁₃.π : (G.obj Y₁).obj X₃ ⟶ sq₁₃.pt.

If C₂ has pullbacks, then we define the Leibniz pullback (often called pullback-hom) as the canonical projection (PullbackObjObj.ofHasPullback G f₁ f₃).π. This defines a bifunctor G.leibnizPullback : (Arrow C₁)ᵒᵖ ⥤ Arrow C₃ ⥤ Arrow C₂.

References

• [Emily Riehl, Dominic Verity, Elements of ∞-Category Theory, Definition C.2.8][RV22]
• https://ncatlab.org/nlab/show/pushout-product
• https://ncatlab.org/nlab/show/pullback-power

Tags

pushout-product, pullback-hom, pullback-power, Leibniz

structure CategoryTheory.Functor.PushoutObjObj {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) : Type (max u₃ v₃)

Given a bifunctor F : C₁ ⥤ C₂ ⥤ C₃, and morphisms f₁ : X₁ ⟶ Y₁ in C₁ and f₂ : X₂ ⟶ Y₂ in C₂, this structure contains the data of a pushout of (F.obj Y₁).obj X₂ and (F.obj X₁).obj Y₂ along (F.obj X₁).obj X₂.

• pt : C₃

  the pushout

• inl : (F.obj Y₁).obj X₂ ⟶ self.pt

  the first inclusion

• inr : (F.obj X₁).obj Y₂ ⟶ self.pt

  the second inclusion

• isPushout : IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) self.inl self.inr

noncomputable def CategoryTheory.Functor.PushoutObjObj.ofHasPushout {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] : F.PushoutObjObj f₁ f₂

The PushoutObjObj structure given by the pushout of the colimits API.

Equations

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

theorem CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inl {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] : (ofHasPushout F f₁ f₂).inl = Limits.pushout.inl ((F.map f₁).app X₂) ((F.obj X₁).map f₂)

theorem CategoryTheory.Functor.PushoutObjObj.ofHasPushout_pt {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] : (ofHasPushout F f₁ f₂).pt = Limits.pushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)

theorem CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inr {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] : (ofHasPushout F f₁ f₂).inr = Limits.pushout.inr ((F.map f₁).app X₂) ((F.obj X₁).map f₂)

noncomputable def CategoryTheory.Functor.PushoutObjObj.ι {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) : sq.pt ⟶ (F.obj Y₁).obj Y₂

The "inclusion" sq.pt ⟶ (F.obj Y₁).obj Y₂ when sq : F.PushoutObjObj f₁ f₂.

Equations

• sq.ι = ⋯.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.inl_ι {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) : CategoryStruct.comp sq.inl sq.ι = (F.obj Y₁).map f₂

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.inl_ι_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) {Z : C₃} (h : (F.obj Y₁).obj Y₂ ⟶ Z) : CategoryStruct.comp sq.inl (CategoryStruct.comp sq.ι h) = CategoryStruct.comp ((F.obj Y₁).map f₂) h

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.inr_ι {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) : CategoryStruct.comp sq.inr sq.ι = (F.map f₁).app Y₂

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.inr_ι_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) {Z : C₃} (h : (F.obj Y₁).obj Y₂ ⟶ Z) : CategoryStruct.comp sq.inr (CategoryStruct.comp sq.ι h) = CategoryStruct.comp ((F.map f₁).app Y₂) h

theorem CategoryTheory.Functor.PushoutObjObj.hom_ext {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) {X₃ : C₃} {f g : sq.pt ⟶ X₃} (hₗ : CategoryStruct.comp sq.inl f = CategoryStruct.comp sq.inl g) (hᵣ : CategoryStruct.comp sq.inr f = CategoryStruct.comp sq.inr g) : f = g

theorem CategoryTheory.Functor.PushoutObjObj.hom_ext_iff {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {sq : F.PushoutObjObj f₁ f₂} {X₃ : C₃} {f g : sq.pt ⟶ X₃} : f = g ↔ CategoryStruct.comp sq.inl f = CategoryStruct.comp sq.inl g ∧ CategoryStruct.comp sq.inr f = CategoryStruct.comp sq.inr g

def CategoryTheory.Functor.PushoutObjObj.flip {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) : F.flip.PushoutObjObj f₂ f₁

Given sq : F.PushoutObjObj f₁ f₂, flipping the pushout square gives sq.flip : F.flip.PushoutObjObj f₂ f₁.

Equations

• sq.flip = { pt := sq.pt, inl := sq.inr, inr := sq.inl, isPushout := ⋯ }

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.flip_inl {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) : sq.flip.inl = sq.inr

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.flip_inr {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) : sq.flip.inr = sq.inl

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.flip_pt {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) : sq.flip.pt = sq.pt

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.ι_flip {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (sq : F.PushoutObjObj f₁ f₂) : sq.flip.ι = sq.ι

theorem CategoryTheory.Functor.PushoutObjObj.ofHasPushout_ι {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} [Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)] : (ofHasPushout F f₁ f₂).ι = Limits.pushout.desc ((F.obj Y₁).map f₂) ((F.map f₁).app Y₂) ⋯

def CategoryTheory.Functor.PushoutObjObj.mapArrowLeft {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ f₁' : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) (sq : f₁ ⟶ f₁') : Arrow.mk sq₁₂.ι ⟶ Arrow.mk sq₁₂'.ι

Given a PushoutObjObj of f₁ : Arrow C₁ and f₂ : Arrow C₂, a PushoutObjObj of f₁' and f₂ : Arrow C₂, and a morphism f₁ ⟶ f₁', this defines a morphism between the induced pushout maps.

Equations

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

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ f₁' : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) (sq : f₁ ⟶ f₁') : (sq₁₂.mapArrowLeft sq₁₂' sq).left = ⋯.desc (CategoryStruct.comp ((F.map sq.right).app f₂.left) sq₁₂'.inl) (CategoryStruct.comp ((F.map sq.left).app f₂.right) sq₁₂'.inr) ⋯

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_right {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ f₁' : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) (sq : f₁ ⟶ f₁') : (sq₁₂.mapArrowLeft sq₁₂' sq).right = (F.map sq.right).app f₂.right

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_id {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) : sq₁₂.mapArrowLeft sq₁₂ (CategoryStruct.id f₁) = CategoryStruct.id (Arrow.mk sq₁₂.ι)

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_comp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ f₁' : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) {f₁'' : Arrow C₁} (sq₁₂'' : F.PushoutObjObj f₁''.hom f₂.hom) (sq : f₁ ⟶ f₁') (sq' : f₁' ⟶ f₁'') : CategoryStruct.comp (sq₁₂.mapArrowLeft sq₁₂' sq) (sq₁₂'.mapArrowLeft sq₁₂'' sq') = sq₁₂.mapArrowLeft sq₁₂'' (CategoryStruct.comp sq sq')

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_comp_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ f₁' : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) {f₁'' : Arrow C₁} (sq₁₂'' : F.PushoutObjObj f₁''.hom f₂.hom) (sq : f₁ ⟶ f₁') (sq' : f₁' ⟶ f₁'') {Z : Arrow C₃} (h : Arrow.mk sq₁₂''.ι ⟶ Z) : CategoryStruct.comp (sq₁₂.mapArrowLeft sq₁₂' sq) (CategoryStruct.comp (sq₁₂'.mapArrowLeft sq₁₂'' sq') h) = CategoryStruct.comp (sq₁₂.mapArrowLeft sq₁₂'' (CategoryStruct.comp sq sq')) h

def CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ f₁' : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) (iso : f₁ ≅ f₁') : Arrow.mk sq₁₂.ι ≅ Arrow.mk sq₁₂'.ι

Given a PushoutObjObj of f₁ : Arrow C₁ and f₂ : Arrow C₂, a PushoutObjObj of f₁' and f₂ : Arrow C₂, and an isomorphism f₁ ≅ f₁', this defines an isomorphism of the induced pushout maps.

Equations

• sq₁₂.ι_iso_of_iso_left sq₁₂' iso = { hom := sq₁₂.mapArrowLeft sq₁₂' iso.hom, inv := sq₁₂'.mapArrowLeft sq₁₂ iso.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_left_hom {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ f₁' : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) (iso : f₁ ≅ f₁') : (sq₁₂.ι_iso_of_iso_left sq₁₂' iso).hom = sq₁₂.mapArrowLeft sq₁₂' iso.hom

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_left_inv {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ f₁' : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) (iso : f₁ ≅ f₁') : (sq₁₂.ι_iso_of_iso_left sq₁₂' iso).inv = sq₁₂'.mapArrowLeft sq₁₂ iso.inv

def CategoryTheory.Functor.PushoutObjObj.mapArrowRight {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ f₂' : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) (sq : f₂ ⟶ f₂') : Arrow.mk sq₁₂.ι ⟶ Arrow.mk sq₁₂'.ι

Given a PushoutObjObj of f₁ : Arrow C₁ and f₂ : Arrow C₂, a PushoutObjObj of f₁ and f₂' : Arrow C₂, and a morphism f₂ ⟶ f₂', this defines a morphism between the induced pushout maps.

Equations

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

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowRight_right {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ f₂' : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) (sq : f₂ ⟶ f₂') : (sq₁₂.mapArrowRight sq₁₂' sq).right = (F.obj f₁.right).map sq.right

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowRight_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ f₂' : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) (sq : f₂ ⟶ f₂') : (sq₁₂.mapArrowRight sq₁₂' sq).left = ⋯.desc (CategoryStruct.comp ((F.obj f₁.right).map sq.left) sq₁₂'.inl) (CategoryStruct.comp ((F.obj f₁.left).map sq.right) sq₁₂'.inr) ⋯

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowRight_id {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) : sq₁₂.mapArrowRight sq₁₂ (CategoryStruct.id f₂) = CategoryStruct.id (Arrow.mk sq₁₂.ι)

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowRight_comp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ f₂' : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) {f₂'' : Arrow C₂} (sq₁₂'' : F.PushoutObjObj f₁.hom f₂''.hom) (sq : f₂ ⟶ f₂') (sq' : f₂' ⟶ f₂'') : CategoryStruct.comp (sq₁₂.mapArrowRight sq₁₂' sq) (sq₁₂'.mapArrowRight sq₁₂'' sq') = sq₁₂.mapArrowRight sq₁₂'' (CategoryStruct.comp sq sq')

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.mapArrowRight_comp_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ f₂' : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) {f₂'' : Arrow C₂} (sq₁₂'' : F.PushoutObjObj f₁.hom f₂''.hom) (sq : f₂ ⟶ f₂') (sq' : f₂' ⟶ f₂'') {Z : Arrow C₃} (h : Arrow.mk sq₁₂''.ι ⟶ Z) : CategoryStruct.comp (sq₁₂.mapArrowRight sq₁₂' sq) (CategoryStruct.comp (sq₁₂'.mapArrowRight sq₁₂'' sq') h) = CategoryStruct.comp (sq₁₂.mapArrowRight sq₁₂'' (CategoryStruct.comp sq sq')) h

def CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_right {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ f₂' : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) (iso : f₂ ≅ f₂') : Arrow.mk sq₁₂.ι ≅ Arrow.mk sq₁₂'.ι

Given a PushoutObjObj of f₁ : Arrow C₁ and f₂ : Arrow C₂, a PushoutObjObj of f₁ and f₂' : Arrow C₂, and an isomorphism f₂ ≅ f₂', this defines an isomorphism of the induced pushout maps.

Equations

• sq₁₂.ι_iso_of_iso_right sq₁₂' iso = { hom := sq₁₂.mapArrowRight sq₁₂' iso.hom, inv := sq₁₂'.mapArrowRight sq₁₂ iso.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_right_inv {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ f₂' : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) (iso : f₂ ≅ f₂') : (sq₁₂.ι_iso_of_iso_right sq₁₂' iso).inv = sq₁₂'.mapArrowRight sq₁₂ iso.inv

@[simp]

theorem CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_right_hom {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {F : Functor C₁ (Functor C₂ C₃)} {f₁ : Arrow C₁} {f₂ f₂' : Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom) (iso : f₂ ≅ f₂') : (sq₁₂.ι_iso_of_iso_right sq₁₂' iso).hom = sq₁₂.mapArrowRight sq₁₂' iso.hom

noncomputable def CategoryTheory.Functor.leibnizPushout {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) [Limits.HasPushouts C₃] : Functor (Arrow C₁) (Functor (Arrow C₂) (Arrow C₃))

Given a bifunctor F : C₁ ⥤ C₂ ⥤ C₃ to a category C₃ which has pushouts, the Leibniz pushout (pushout-product) of f₁ : X₁ ⟶ Y₁ in C₁ and f₂ : X₂ ⟶ Y₂ in C₂ is the map pushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ⟶ (F.obj Y₁).obj Y₂ induced by the diagram

  `(F.obj X₁).obj X₂` ----> `(F.obj Y₁).obj X₂`
          |                            |
          |                            |
          v                            v
  `(F.obj X₁).obj Y₂` ----> `(F.obj Y₁).obj Y₂`

Equations

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

@[simp]

theorem CategoryTheory.Functor.leibnizPushout_obj_obj {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) [Limits.HasPushouts C₃] (f₁ : Arrow C₁) (f₂ : Arrow C₂) : (F.leibnizPushout.obj f₁).obj f₂ = Arrow.mk (PushoutObjObj.ofHasPushout F f₁.hom f₂.hom).ι

@[simp]

theorem CategoryTheory.Functor.leibnizPushout_map_app {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) [Limits.HasPushouts C₃] {X✝ Y✝ : Arrow C₁} (sq : X✝ ⟶ Y✝) (f₂ : Arrow C₂) : (F.leibnizPushout.map sq).app f₂ = (PushoutObjObj.ofHasPushout F X✝.hom f₂.hom).mapArrowLeft (PushoutObjObj.ofHasPushout F Y✝.hom f₂.hom) sq

@[simp]

theorem CategoryTheory.Functor.leibnizPushout_obj_map {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (F : Functor C₁ (Functor C₂ C₃)) [Limits.HasPushouts C₃] (f₁ : Arrow C₁) {X✝ Y✝ : Arrow C₂} (sq : X✝ ⟶ Y✝) : (F.leibnizPushout.obj f₁).map sq = (PushoutObjObj.ofHasPushout F f₁.hom X✝.hom).mapArrowRight (PushoutObjObj.ofHasPushout F f₁.hom Y✝.hom) sq

structure CategoryTheory.Functor.PullbackObjObj {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) : Type (max u₂ v₂)

Given a bifunctor G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂, and morphisms f₁ : X₁ ⟶ Y₁ in C₁ and f₃ : X₃ ⟶ Y₃ in C₃, this structure contains the data of a pullback of (G.obj (op X₁)).obj X₃ and (G.obj (op Y₁)).obj Y₃ over (G.obj (op X₁)).obj Y₃.

• pt : C₂

  the pullback

• fst : self.pt ⟶ (G.obj (Opposite.op X₁)).obj X₃

  the first projection

• snd : self.pt ⟶ (G.obj (Opposite.op Y₁)).obj Y₃

  the second projection

• isPullback : IsPullback self.fst self.snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)

noncomputable def CategoryTheory.Functor.PullbackObjObj.ofHasPullback {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] : G.PullbackObjObj f₁ f₃

The PullbackObjObj structure given by the pullback of the limits API.

Equations

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

theorem CategoryTheory.Functor.PullbackObjObj.ofHasPullback_snd {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] : (ofHasPullback G f₁ f₃).snd = Limits.pullback.snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)

theorem CategoryTheory.Functor.PullbackObjObj.ofHasPullback_pt {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] : (ofHasPullback G f₁ f₃).pt = Limits.pullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)

theorem CategoryTheory.Functor.PullbackObjObj.ofHasPullback_fst {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] : (ofHasPullback G f₁ f₃).fst = Limits.pullback.fst ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)

noncomputable def CategoryTheory.Functor.PullbackObjObj.π {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) : (G.obj (Opposite.op Y₁)).obj X₃ ⟶ sq.pt

The projection (G.obj (op Y₁)).obj X₃ ⟶ sq.pt when sq : G.PullbackObjObj f₁ f₃.

Equations

• sq.π = ⋯.lift ((G.map f₁.op).app X₃) ((G.obj (Opposite.op Y₁)).map f₃) ⋯

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.π_fst {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) : CategoryStruct.comp sq.π sq.fst = (G.map f₁.op).app X₃

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.π_fst_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) {Z : C₂} (h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z) : CategoryStruct.comp sq.π (CategoryStruct.comp sq.fst h) = CategoryStruct.comp ((G.map f₁.op).app X₃) h

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.π_snd {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) : CategoryStruct.comp sq.π sq.snd = (G.obj (Opposite.op Y₁)).map f₃

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.π_snd_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) {Z : C₂} (h : (G.obj (Opposite.op Y₁)).obj Y₃ ⟶ Z) : CategoryStruct.comp sq.π (CategoryStruct.comp sq.snd h) = CategoryStruct.comp ((G.obj (Opposite.op Y₁)).map f₃) h

theorem CategoryTheory.Functor.PullbackObjObj.hom_ext {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq : G.PullbackObjObj f₁ f₃) {X₂ : C₂} {f g : X₂ ⟶ sq.pt} (h₁ : CategoryStruct.comp f sq.fst = CategoryStruct.comp g sq.fst) (h₂ : CategoryStruct.comp f sq.snd = CategoryStruct.comp g sq.snd) : f = g

theorem CategoryTheory.Functor.PullbackObjObj.hom_ext_iff {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} {sq : G.PullbackObjObj f₁ f₃} {X₂ : C₂} {f g : X₂ ⟶ sq.pt} : f = g ↔ CategoryStruct.comp f sq.fst = CategoryStruct.comp g sq.fst ∧ CategoryStruct.comp f sq.snd = CategoryStruct.comp g sq.snd

theorem CategoryTheory.Functor.PullbackObjObj.ofHasPullback_π {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} [Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)] : (ofHasPullback G f₁ f₃).π = Limits.pullback.lift ((G.map f₁.op).app X₃) ((G.obj (Opposite.op Y₁)).map f₃) ⋯

def CategoryTheory.Functor.PullbackObjObj.mapArrowLeft {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ f₁' : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) (sq : f₁' ⟶ f₁) : Arrow.mk sq₁₃.π ⟶ Arrow.mk sq₁₃'.π

Given a PullbackObjObj of f₁ : Arrow C₁ and f₃ : Arrow C₃, a PullbackObjObj of f₁' and f₃ : Arrow C₃, and a morphism f₁' ⟶ f₁, this defines a morphism between the induced pullback maps.

Equations

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

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_right {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ f₁' : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) (sq : f₁' ⟶ f₁) : (sq₁₃.mapArrowLeft sq₁₃' sq).right = ⋯.lift (CategoryStruct.comp sq₁₃.fst ((G.map sq.left.op).app f₃.left)) (CategoryStruct.comp sq₁₃.snd ((G.map sq.right.op).app f₃.right)) ⋯

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ f₁' : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) (sq : f₁' ⟶ f₁) : (sq₁₃.mapArrowLeft sq₁₃' sq).left = (G.map sq.right.op).app f₃.left

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_id {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) : sq₁₃.mapArrowLeft sq₁₃ (CategoryStruct.id f₁) = CategoryStruct.id (Arrow.mk sq₁₃.π)

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_comp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ f₁' : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) {f₁'' : Arrow C₁} (sq₁₃'' : G.PullbackObjObj f₁''.hom f₃.hom) (sq' : f₁'' ⟶ f₁') (sq : f₁' ⟶ f₁) : CategoryStruct.comp (sq₁₃.mapArrowLeft sq₁₃' sq) (sq₁₃'.mapArrowLeft sq₁₃'' sq') = sq₁₃.mapArrowLeft sq₁₃'' (CategoryStruct.comp sq' sq)

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_comp_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ f₁' : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) {f₁'' : Arrow C₁} (sq₁₃'' : G.PullbackObjObj f₁''.hom f₃.hom) (sq' : f₁'' ⟶ f₁') (sq : f₁' ⟶ f₁) {Z : Arrow C₂} (h : Arrow.mk sq₁₃''.π ⟶ Z) : CategoryStruct.comp (sq₁₃.mapArrowLeft sq₁₃' sq) (CategoryStruct.comp (sq₁₃'.mapArrowLeft sq₁₃'' sq') h) = CategoryStruct.comp (sq₁₃.mapArrowLeft sq₁₃'' (CategoryStruct.comp sq' sq)) h

def CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ f₁' : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) (iso : f₁ ≅ f₁') : Arrow.mk sq₁₃.π ≅ Arrow.mk sq₁₃'.π

Given a PullbackObjObj of f₁ : Arrow C₁ and f₃ : Arrow C₃, a PullbackObjObj of f₁' and f₃ : Arrow C₃, and an isomorphism f₁ ≅ f₁', this defines an isomorphism of the induced pullback maps.

Equations

• sq₁₃.π_iso_of_iso_left sq₁₃' iso = { hom := sq₁₃.mapArrowLeft sq₁₃' iso.inv, inv := sq₁₃'.mapArrowLeft sq₁₃ iso.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_left_hom {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ f₁' : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) (iso : f₁ ≅ f₁') : (sq₁₃.π_iso_of_iso_left sq₁₃' iso).hom = sq₁₃.mapArrowLeft sq₁₃' iso.inv

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_left_inv {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ f₁' : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom) (iso : f₁ ≅ f₁') : (sq₁₃.π_iso_of_iso_left sq₁₃' iso).inv = sq₁₃'.mapArrowLeft sq₁₃ iso.hom

def CategoryTheory.Functor.PullbackObjObj.mapArrowRight {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ f₃' : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) (sq : f₃ ⟶ f₃') : Arrow.mk sq₁₃.π ⟶ Arrow.mk sq₁₃'.π

Given a PullbackObjObj of f₁ : Arrow C₁ and f₃ : Arrow C₃, a PullbackObjObj of f₁ and f₃' : Arrow C₃, and a morphism f₃ ⟶ f₃', this defines a morphism between the induced pullback maps.

Equations

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

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowRight_right {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ f₃' : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) (sq : f₃ ⟶ f₃') : (sq₁₃.mapArrowRight sq₁₃' sq).right = ⋯.lift (CategoryStruct.comp sq₁₃.fst ((G.obj (Opposite.op f₁.left)).map sq.left)) (CategoryStruct.comp sq₁₃.snd ((G.obj (Opposite.op f₁.right)).map sq.right)) ⋯

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowRight_left {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ f₃' : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) (sq : f₃ ⟶ f₃') : (sq₁₃.mapArrowRight sq₁₃' sq).left = (G.obj (Opposite.op f₁.right)).map sq.left

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowRight_id {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) : sq₁₃.mapArrowRight sq₁₃ (CategoryStruct.id f₃) = CategoryStruct.id (Arrow.mk sq₁₃.π)

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowRight_comp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ f₃' : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) {f₃'' : Arrow C₃} (sq₁₃'' : G.PullbackObjObj f₁.hom f₃''.hom) (sq : f₃ ⟶ f₃') (sq' : f₃' ⟶ f₃'') : CategoryStruct.comp (sq₁₃.mapArrowRight sq₁₃' sq) (sq₁₃'.mapArrowRight sq₁₃'' sq') = sq₁₃.mapArrowRight sq₁₃'' (CategoryStruct.comp sq sq')

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.mapArrowRight_comp_assoc {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ f₃' : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) {f₃'' : Arrow C₃} (sq₁₃'' : G.PullbackObjObj f₁.hom f₃''.hom) (sq : f₃ ⟶ f₃') (sq' : f₃' ⟶ f₃'') {Z : Arrow C₂} (h : Arrow.mk sq₁₃''.π ⟶ Z) : CategoryStruct.comp (sq₁₃.mapArrowRight sq₁₃' sq) (CategoryStruct.comp (sq₁₃'.mapArrowRight sq₁₃'' sq') h) = CategoryStruct.comp (sq₁₃.mapArrowRight sq₁₃'' (CategoryStruct.comp sq sq')) h

def CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_right {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ f₃' : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) (iso : f₃ ≅ f₃') : Arrow.mk sq₁₃.π ≅ Arrow.mk sq₁₃'.π

Given a PullbackObjObj of f₁ : Arrow C₁ and f₃ : Arrow C₃, a PullbackObjObj of f₁ and f₃' : Arrow C₃, and an isomorphism f₃ ≅ f₃', this defines an isomorphism of the induced pullback maps.

Equations

• sq₁₃.π_iso_of_iso_right sq₁₃' iso = { hom := sq₁₃.mapArrowRight sq₁₃' iso.hom, inv := sq₁₃'.mapArrowRight sq₁₃ iso.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_right_inv {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ f₃' : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) (iso : f₃ ≅ f₃') : (sq₁₃.π_iso_of_iso_right sq₁₃' iso).inv = sq₁₃'.mapArrowRight sq₁₃ iso.inv

@[simp]

theorem CategoryTheory.Functor.PullbackObjObj.π_iso_of_iso_right_hom {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {G : Functor C₁ᵒᵖ (Functor C₃ C₂)} {f₁ : Arrow C₁} {f₃ f₃' : Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) (iso : f₃ ≅ f₃') : (sq₁₃.π_iso_of_iso_right sq₁₃' iso).hom = sq₁₃.mapArrowRight sq₁₃' iso.hom

noncomputable def CategoryTheory.Functor.leibnizPullback {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) [Limits.HasPullbacks C₂] : Functor (Arrow C₁)ᵒᵖ (Functor (Arrow C₃) (Arrow C₂))

Given a bifunctor G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂ to a category C₂ which has pullbacks, the Leibniz pullback (pullback-power) of f₁ : X₁ ⟶ Y₁ in C₁ and f₃ : X₃ ⟶ Y₃ in C₃ is the map (G.obj (op Y₁)).obj X₃ ⟶ pullback ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃) induced by the diagram

  `(G.obj (op Y₁)).obj X₃` ----> `(G.obj (op X₁)).obj X₃`
              |                              |
              |                              |
              v                              v
  `(G.obj (op Y₁)).obj Y₃` ----> `(G.obj (op X₁)).obj Y₃`

Equations

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

@[simp]

theorem CategoryTheory.Functor.leibnizPullback_obj_obj {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) [Limits.HasPullbacks C₂] (f₁ : (Arrow C₁)ᵒᵖ) (f₃ : Arrow C₃) : (G.leibnizPullback.obj f₁).obj f₃ = Arrow.mk (PullbackObjObj.ofHasPullback G (Opposite.unop f₁).hom f₃.hom).π

@[simp]

theorem CategoryTheory.Functor.leibnizPullback_map_app {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) [Limits.HasPullbacks C₂] {X✝ Y✝ : (Arrow C₁)ᵒᵖ} (sq : X✝ ⟶ Y✝) (f₃ : Arrow C₃) : (G.leibnizPullback.map sq).app f₃ = (PullbackObjObj.ofHasPullback G (Opposite.unop X✝).hom f₃.hom).mapArrowLeft (PullbackObjObj.ofHasPullback G (Opposite.unop Y✝).hom f₃.hom) sq.unop

@[simp]

theorem CategoryTheory.Functor.leibnizPullback_obj_map {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] (G : Functor C₁ᵒᵖ (Functor C₃ C₂)) [Limits.HasPullbacks C₂] (f₁ : (Arrow C₁)ᵒᵖ) {X✝ Y✝ : Arrow C₃} (sq : X✝ ⟶ Y✝) : (G.leibnizPullback.obj f₁).map sq = (PullbackObjObj.ofHasPullback G (Opposite.unop f₁).hom X✝.hom).mapArrowRight (PullbackObjObj.ofHasPullback G (Opposite.unop f₁).hom Y✝.hom) sq