Universal colimits and van Kampen colimits #
Main definitions #
CategoryTheory.IsUniversalColimit: A (colimit) cocone over a diagramF : J ⥤ Cis universal if it is stable under pullbacks.CategoryTheory.IsVanKampenColimit: A (colimit) cocone over a diagramF : J ⥤ Cis van Kampen if for every coconec'over the pullback of the diagramF' : J ⥤ C',c'is colimiting iffc'is the pullback ofc.
References #
- https://ncatlab.org/nlab/show/van+Kampen+colimit
- [Stephen Lack and Paweł Sobociński, Adhesive Categories][adhesive2004]
def
CategoryTheory.NatTrans.Equifibered
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G : Functor J C}
(α : F ⟶ G)
:
A natural transformation is equifibered if every commutative square of the following form is a pullback.
F(X) → F(Y)
↓ ↓
G(X) → G(Y)
Equations
- CategoryTheory.NatTrans.Equifibered α = ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.IsPullback (F.map f) (α.app i) (α.app j) (G.map f)
Instances For
theorem
CategoryTheory.NatTrans.equifibered_of_isIso
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G : Functor J C}
(α : F ⟶ G)
[IsIso α]
:
theorem
CategoryTheory.NatTrans.Equifibered.comp
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G H : Functor J C}
{α : F ⟶ G}
{β : G ⟶ H}
(hα : Equifibered α)
(hβ : Equifibered β)
:
theorem
CategoryTheory.NatTrans.Equifibered.whiskerRight
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{D : Type u_2}
[Category.{u_3, u_2} D]
{F G : Functor J C}
{α : F ⟶ G}
(hα : Equifibered α)
(H : Functor C D)
[∀ (i j : J) (f : j ⟶ i), Limits.PreservesLimit (Limits.cospan (α.app i) (G.map f)) H]
:
theorem
CategoryTheory.NatTrans.Equifibered.whiskerLeft
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{K : Type u_3}
[Category.{u_4, u_3} K]
{F G : Functor J C}
{α : F ⟶ G}
(hα : Equifibered α)
(H : Functor K J)
:
theorem
CategoryTheory.mapPair_equifibered
{C : Type u}
[Category.{v, u} C]
{F F' : Functor (Discrete Limits.WalkingPair) C}
(α : F ⟶ F')
:
theorem
CategoryTheory.NatTrans.equifibered_of_discrete
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{F G : Functor (Discrete ι) C}
(α : F ⟶ G)
:
def
CategoryTheory.IsUniversalColimit
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F : Functor J C}
(c : Limits.Cocone F)
:
A (colimit) cocone over a diagram F : J ⥤ C is universal if it is stable under pullbacks.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.IsVanKampenColimit
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F : Functor J C}
(c : Limits.Cocone F)
:
A (colimit) cocone over a diagram F : J ⥤ C is van Kampen if for every cocone c' over the
pullback of the diagram F' : J ⥤ C', c' is colimiting iff c' is the pullback of c.
TODO: Show that this is iff the functor C ⥤ Catᵒᵖ sending x to C/x preserves it.
TODO: Show that this is iff the inclusion functor C ⥤ Span(C) preserves it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.IsVanKampenColimit.isUniversal
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F : Functor J C}
{c : Limits.Cocone F}
(H : IsVanKampenColimit c)
:
noncomputable def
CategoryTheory.IsUniversalColimit.isColimit
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F : Functor J C}
{c : Limits.Cocone F}
(h : IsUniversalColimit c)
:
A universal colimit is a colimit.
Instances For
noncomputable def
CategoryTheory.IsVanKampenColimit.isColimit
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F : Functor J C}
{c : Limits.Cocone F}
(h : IsVanKampenColimit c)
:
A van Kampen colimit is a colimit.
Instances For
theorem
CategoryTheory.IsInitial.isVanKampenColimit
{C : Type u}
[Category.{v, u} C]
[Limits.HasStrictInitialObjects C]
{X : C}
(h : Limits.IsInitial X)
:
theorem
CategoryTheory.IsUniversalColimit.of_iso
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F : Functor J C}
{c c' : Limits.Cocone F}
(hc : IsUniversalColimit c)
(e : c ≅ c')
:
theorem
CategoryTheory.IsVanKampenColimit.of_iso
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F : Functor J C}
{c c' : Limits.Cocone F}
(H : IsVanKampenColimit c)
(e : c ≅ c')
:
theorem
CategoryTheory.IsVanKampenColimit.precompose_isIso
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G : Functor J C}
(α : F ⟶ G)
[IsIso α]
{c : Limits.Cocone G}
(hc : IsVanKampenColimit c)
:
theorem
CategoryTheory.IsUniversalColimit.precompose_isIso
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G : Functor J C}
(α : F ⟶ G)
[IsIso α]
{c : Limits.Cocone G}
(hc : IsUniversalColimit c)
:
theorem
CategoryTheory.IsVanKampenColimit.precompose_isIso_iff
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G : Functor J C}
(α : F ⟶ G)
[IsIso α]
{c : Limits.Cocone G}
:
theorem
CategoryTheory.IsUniversalColimit.of_mapCocone
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{D : Type u_2}
[Category.{u_3, u_2} D]
(G : Functor C D)
{F : Functor J C}
{c : Limits.Cocone F}
[Limits.PreservesLimitsOfShape Limits.WalkingCospan G]
[Limits.ReflectsColimitsOfShape J G]
(hc : IsUniversalColimit (G.mapCocone c))
:
theorem
CategoryTheory.IsVanKampenColimit.of_mapCocone
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{D : Type u_2}
[Category.{u_3, u_2} D]
(G : Functor C D)
{F : Functor J C}
{c : Limits.Cocone F}
[∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), Limits.PreservesLimit (Limits.cospan f (F.map g)) G]
[∀ (i : J) (X : C) (f : X ⟶ c.pt), Limits.PreservesLimit (Limits.cospan f (c.ι.app i)) G]
[Limits.ReflectsLimitsOfShape Limits.WalkingCospan G]
[Limits.PreservesColimitsOfShape J G]
[Limits.ReflectsColimitsOfShape J G]
(H : IsVanKampenColimit (G.mapCocone c))
:
theorem
CategoryTheory.IsVanKampenColimit.mapCocone_iff
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{D : Type u_2}
[Category.{u_3, u_2} D]
(G : Functor C D)
{F : Functor J C}
{c : Limits.Cocone F}
[G.IsEquivalence]
:
theorem
CategoryTheory.IsUniversalColimit.whiskerEquivalence
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{K : Type u_3}
[Category.{u_4, u_3} K]
(e : J ≌ K)
{F : Functor K C}
{c : Limits.Cocone F}
(hc : IsUniversalColimit c)
:
theorem
CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{K : Type u_3}
[Category.{u_4, u_3} K]
(e : J ≌ K)
{F : Functor K C}
{c : Limits.Cocone F}
:
theorem
CategoryTheory.IsVanKampenColimit.whiskerEquivalence
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{K : Type u_3}
[Category.{u_4, u_3} K]
(e : J ≌ K)
{F : Functor K C}
{c : Limits.Cocone F}
(hc : IsVanKampenColimit c)
:
theorem
CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{K : Type u_3}
[Category.{u_4, u_3} K]
(e : J ≌ K)
{F : Functor K C}
{c : Limits.Cocone F}
:
theorem
CategoryTheory.isVanKampenColimit_of_evaluation
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{D : Type u_2}
[Category.{u_3, u_2} D]
[Limits.HasPullbacks D]
[Limits.HasColimitsOfShape J D]
(F : Functor J (Functor C D))
(c : Limits.Cocone F)
(hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c))
:
theorem
CategoryTheory.IsUniversalColimit.map_reflective
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{D : Type u_2}
[Category.{u_3, u_2} D]
{Gl : Functor C D}
{Gr : Functor D C}
(adj : Gl ⊣ Gr)
[Gr.Full]
[Gr.Faithful]
{F : Functor J D}
{c : Limits.Cocone (F.comp Gr)}
(H : IsUniversalColimit c)
[∀ (X : D) (f : X ⟶ Gl.obj c.pt), Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)]
[∀ (X : D) (f : X ⟶ Gl.obj c.pt), Limits.PreservesLimit (Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl]
:
IsUniversalColimit (Gl.mapCocone c)
theorem
CategoryTheory.IsVanKampenColimit.map_reflective
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{D : Type u_2}
[Category.{u_3, u_2} D]
[Limits.HasColimitsOfShape J C]
{Gl : Functor C D}
{Gr : Functor D C}
(adj : Gl ⊣ Gr)
[Gr.Full]
[Gr.Faithful]
{F : Functor J D}
{c : Limits.Cocone (F.comp Gr)}
(H : IsVanKampenColimit c)
[∀ (X : D) (f : X ⟶ Gl.obj c.pt), Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)]
[∀ (X : D) (f : X ⟶ Gl.obj c.pt), Limits.PreservesLimit (Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl]
[∀ (X : C) (i : J) (f : X ⟶ c.pt), Limits.PreservesLimit (Limits.cospan f (c.ι.app i)) Gl]
:
IsVanKampenColimit (Gl.mapCocone c)
theorem
CategoryTheory.hasStrictInitial_of_isUniversal
{C : Type u}
[Category.{v, u} C]
[Limits.HasInitial C]
(H : IsUniversalColimit (Limits.BinaryCofan.mk (CategoryStruct.id (⊥_ C)) (CategoryStruct.id (⊥_ C))))
:
theorem
CategoryTheory.isVanKampenColimit_of_isEmpty
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
[Limits.HasStrictInitialObjects C]
[IsEmpty J]
{F : Functor J C}
(c : Limits.Cocone F)
(hc : Limits.IsColimit c)
:
theorem
CategoryTheory.BinaryCofan.isVanKampen_iff
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(c : Limits.BinaryCofan X Y)
:
IsVanKampenColimit c ↔ ∀ {X' Y' : C} (c' : Limits.BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
CategoryStruct.comp αX c.inl = CategoryStruct.comp c'.inl f →
CategoryStruct.comp αY c.inr = CategoryStruct.comp c'.inr f →
(Nonempty (Limits.IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
theorem
CategoryTheory.BinaryCofan.isVanKampen_mk
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(c : Limits.BinaryCofan X Y)
(cofans : (X Y : C) → Limits.BinaryCofan X Y)
(colimits : (X Y : C) → Limits.IsColimit (cofans X Y))
(cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Limits.PullbackCone f g)
(limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Limits.IsLimit (cones f g))
(h₁ :
∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
CategoryStruct.comp αX c.inl = CategoryStruct.comp (cofans X' Y').inl f →
CategoryStruct.comp αY c.inr = CategoryStruct.comp (cofans X' Y').inr f →
IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr)
(h₂ : {Z : C} → (f : Z ⟶ c.pt) → Limits.IsColimit (Limits.BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst))
:
theorem
CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen
{C : Type u}
[Category.{v, u} C]
[Limits.HasInitial C]
{X Y : C}
{c : Limits.BinaryCofan X Y}
(h : IsVanKampenColimit c)
:
theorem
CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[Limits.HasInitial C]
{c : Limits.BinaryCofan X Y}
(h : IsVanKampenColimit c)
:
IsPullback (Limits.initial.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.left }))
(Limits.initial.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.right })) c.inl c.inr
theorem
CategoryTheory.isUniversalColimit_extendCofan
{C : Type u}
[Category.{v, u} C]
{n : ℕ}
(f : Fin (n + 1) → C)
{c₁ : Limits.Cofan fun (i : Fin n) => f i.succ}
{c₂ : Limits.BinaryCofan (f 0) c₁.pt}
(t₁ : IsUniversalColimit c₁)
(t₂ : IsUniversalColimit c₂)
[∀ {Z : C} (i : Z ⟶ c₂.pt), Limits.HasPullback c₂.inr i]
:
IsUniversalColimit (extendCofan c₁ c₂)
theorem
CategoryTheory.isVanKampenColimit_extendCofan
{C : Type u}
[Category.{v, u} C]
{n : ℕ}
(f : Fin (n + 1) → C)
{c₁ : Limits.Cofan fun (i : Fin n) => f i.succ}
{c₂ : Limits.BinaryCofan (f 0) c₁.pt}
(t₁ : IsVanKampenColimit c₁)
(t₂ : IsVanKampenColimit c₂)
[∀ {Z : C} (i : Z ⟶ c₂.pt), Limits.HasPullback c₂.inr i]
[Limits.HasFiniteCoproducts C]
:
IsVanKampenColimit (extendCofan c₁ c₂)
theorem
CategoryTheory.isPullback_of_cofan_isVanKampen
{C : Type u}
[Category.{v, u} C]
[Limits.HasInitial C]
{ι : Type u_3}
{X : ι → C}
{c : Limits.Cofan X}
(hc : IsVanKampenColimit c)
(i j : ι)
[DecidableEq ι]
:
IsPullback (if h : j = i then eqToHom ⋯ else CategoryStruct.comp (eqToHom ⋯) (Limits.initial.to (X i)))
(if h : j = i then eqToHom ⋯ else CategoryStruct.comp (eqToHom ⋯) (Limits.initial.to (X j))) (c.inj i) (c.inj j)
theorem
CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen
{C : Type u}
[Category.{v, u} C]
[Limits.HasInitial C]
{ι : Type u_3}
{F : Functor (Discrete ι) C}
{c : Limits.Cocone F}
(hc : IsVanKampenColimit c)
(i j : Discrete ι)
(hi : i ≠ j)
:
IsPullback (Limits.initial.to (F.obj i)) (Limits.initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
theorem
CategoryTheory.mono_of_cofan_isVanKampen
{C : Type u}
[Category.{v, u} C]
[Limits.HasInitial C]
{ι : Type u_3}
{F : Functor (Discrete ι) C}
{c : Limits.Cocone F}
(hc : IsVanKampenColimit c)
(i : Discrete ι)
:
theorem
CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{S B : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
(f : (i : ι) → X i ⟶ S)
(u : a.pt ⟶ S)
(v : B ⟶ S)
(s : (i : ι) → Limits.PullbackCone v (f i))
(hs : (i : ι) → Limits.IsLimit (s i))
(t : Limits.PullbackCone v u)
(ht : Limits.IsLimit t)
(d : Limits.Cofan fun (i : ι) => (s i).pt)
(e : d.pt ≅ t.pt)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
(he₁ : ∀ (i : ι), CategoryStruct.comp (d.inj i) (CategoryStruct.comp e.hom t.fst) = (s i).fst := by aesop_cat)
(he₂ :
∀ (i : ι),
CategoryStruct.comp (d.inj i) (CategoryStruct.comp e.hom t.snd) = CategoryStruct.comp (s i).snd (a.inj i) := by
aesop_cat)
:
Pullbacks distribute over universal coproducts on the left: This is the isomorphism
∐ (B ×[S] Xᵢ) ≅ B ×[S] (∐ Xᵢ).
theorem
CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{S B : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
(f : (i : ι) → X i ⟶ S)
(u : a.pt ⟶ S)
(v : B ⟶ S)
{P : ι → C}
(q₁ : (i : ι) → P i ⟶ B)
(q₂ : (i : ι) → P i ⟶ X i)
(hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i))
{Z : C}
{p₁ : Z ⟶ B}
{p₂ : Z ⟶ a.pt}
(h : IsPullback p₁ p₂ v u)
(d : Limits.Cofan P)
(e : d.pt ≅ Z)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
(he₁ : ∀ (i : ι), CategoryStruct.comp (d.inj i) (CategoryStruct.comp e.hom p₁) = q₁ i := by aesop_cat)
(he₂ :
∀ (i : ι), CategoryStruct.comp (d.inj i) (CategoryStruct.comp e.hom p₂) = CategoryStruct.comp (q₂ i) (a.inj i) := by
aesop_cat)
:
Pullbacks distribute over universal coproducts on the left: This is the isomorphism
∐ (B ×[S] Xᵢ) ≅ B ×[S] (∐ Xᵢ).
theorem
CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{S B : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
(f : (i : ι) → X i ⟶ S)
(u : a.pt ⟶ S)
(v : B ⟶ S)
{P : ι → C}
(q₁ : (i : ι) → P i ⟶ B)
(q₂ : (i : ι) → P i ⟶ X i)
(hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i))
{d : Limits.Cofan P}
(hd : Limits.IsColimit d)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
[Limits.HasPullback v u]
:
IsPullback (Limits.Cofan.IsColimit.desc hd q₁)
(Limits.Cofan.IsColimit.desc hd fun (x : ι) => CategoryStruct.comp (q₂ x) (a.inj x)) v u
Pullbacks distribute over universal coproducts on the left: This is the isomorphism
∐ (B ×[S] Xᵢ) ≅ B ×[S] (∐ Xᵢ).
theorem
CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{S B : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
(f : (i : ι) → X i ⟶ S)
(u : a.pt ⟶ S)
(v : B ⟶ S)
(s : (i : ι) → Limits.PullbackCone (f i) v)
(hs : (i : ι) → Limits.IsLimit (s i))
(t : Limits.PullbackCone u v)
(ht : Limits.IsLimit t)
(d : Limits.Cofan fun (i : ι) => (s i).pt)
(e : d.pt ≅ t.pt)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
(he₁ :
∀ (i : ι),
CategoryStruct.comp (d.inj i) (CategoryStruct.comp e.hom t.fst) = CategoryStruct.comp (s i).fst (a.inj i) := by
aesop_cat)
(he₂ : ∀ (i : ι), CategoryStruct.comp (d.inj i) (CategoryStruct.comp e.hom t.snd) = (s i).snd := by aesop_cat)
:
Pullbacks distribute over universal coproducts on the right: This is the isomorphism
∐ (Xᵢ ×[S] B) ≅ (∐ Xᵢ) ×[S] B.
theorem
CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{S B : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
(f : (i : ι) → X i ⟶ S)
(u : a.pt ⟶ S)
(v : B ⟶ S)
{P : ι → C}
(q₁ : (i : ι) → P i ⟶ X i)
(q₂ : (i : ι) → P i ⟶ B)
(hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v)
{Z : C}
{p₁ : Z ⟶ a.pt}
{p₂ : Z ⟶ B}
(h : IsPullback p₁ p₂ u v)
(d : Limits.Cofan P)
(e : d.pt ≅ Z)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
(he₁ :
∀ (i : ι), CategoryStruct.comp (d.inj i) (CategoryStruct.comp e.hom p₁) = CategoryStruct.comp (q₁ i) (a.inj i) := by
aesop_cat)
(he₂ : ∀ (i : ι), CategoryStruct.comp (d.inj i) (CategoryStruct.comp e.hom p₂) = q₂ i := by aesop_cat)
:
Pullbacks distribute over universal coproducts on the right: This is the isomorphism
∐ (Xᵢ ×[S] B) ≅ (∐ Xᵢ) ×[S] B.
theorem
CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_right
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{S B : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
(f : (i : ι) → X i ⟶ S)
(u : a.pt ⟶ S)
(v : B ⟶ S)
{P : ι → C}
(q₁ : (i : ι) → P i ⟶ X i)
(q₂ : (i : ι) → P i ⟶ B)
(hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v)
{d : Limits.Cofan P}
(hd : Limits.IsColimit d)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
[Limits.HasPullback u v]
:
IsPullback (Limits.Cofan.IsColimit.desc hd fun (x : ι) => CategoryStruct.comp (q₁ x) (a.inj x))
(Limits.Cofan.IsColimit.desc hd q₂) u v
Pullbacks distribute over universal coproducts on the right: This is the isomorphism
∐ (Xᵢ ×[S] B) ≅ (∐ Xᵢ) ×[S] B.
theorem
CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{ι' : Type u_4}
{S : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
{Y : ι' → C}
{b : Limits.Cofan Y}
(hbu : IsUniversalColimit b)
(f : (i : ι) → X i ⟶ S)
(g : (i : ι') → Y i ⟶ S)
(u : a.pt ⟶ S)
(v : b.pt ⟶ S)
[∀ (i : ι), Limits.HasPullback (f i) v]
(s : (i : ι) → (j : ι') → Limits.PullbackCone (f i) (g j))
(hs : (i : ι) → (j : ι') → Limits.IsLimit (s i j))
(t : Limits.PullbackCone u v)
(ht : Limits.IsLimit t)
{d : Limits.Cofan fun (p : ι × ι') => (s p.1 p.2).pt}
(e : d.pt ≅ t.pt)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
(hv : ∀ (i : ι'), CategoryStruct.comp (b.inj i) v = g i := by aesop_cat)
(he₁ :
∀ (i : ι) (j : ι'),
CategoryStruct.comp (d.inj (i, j)) (CategoryStruct.comp e.hom t.fst) = CategoryStruct.comp (s (i, j).1 (i, j).2).fst (a.inj (i, j).1) := by
aesop_cat)
(he₂ :
∀ (i : ι) (j : ι'),
CategoryStruct.comp (d.inj (i, j)) (CategoryStruct.comp e.hom t.snd) = CategoryStruct.comp (s (i, j).1 (i, j).2).snd (b.inj (i, j).2) := by
aesop_cat)
:
Pullbacks distribute over universal coproducts in both arguments: This is the isomorphism
∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ).
theorem
CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{ι' : Type u_4}
{S : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
{Y : ι' → C}
{b : Limits.Cofan Y}
(hbu : IsUniversalColimit b)
(f : (i : ι) → X i ⟶ S)
(g : (i : ι') → Y i ⟶ S)
(u : a.pt ⟶ S)
(v : b.pt ⟶ S)
[∀ (i : ι), Limits.HasPullback (f i) v]
{P : ι × ι' → C}
{q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i}
{q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j}
(hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j))
{Z : C}
{p₁ : Z ⟶ a.pt}
{p₂ : Z ⟶ b.pt}
(h : IsPullback p₁ p₂ u v)
{d : Limits.Cofan P}
(e : d.pt ≅ Z)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
(hv : ∀ (i : ι'), CategoryStruct.comp (b.inj i) v = g i := by aesop_cat)
(he₁ :
∀ (i : ι) (j : ι'),
CategoryStruct.comp (d.inj (i, j)) (CategoryStruct.comp e.hom p₁) = CategoryStruct.comp (q₁ i j) (a.inj i) := by
aesop_cat)
(he₂ :
∀ (i : ι) (j : ι'),
CategoryStruct.comp (d.inj (i, j)) (CategoryStruct.comp e.hom p₂) = CategoryStruct.comp (q₂ i j) (b.inj j) := by
aesop_cat)
:
Pullbacks distribute over universal coproducts in both arguments: This is the isomorphism
∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ).
theorem
CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{ι' : Type u_4}
{S : C}
{X : ι → C}
{a : Limits.Cofan X}
(hau : IsUniversalColimit a)
{Y : ι' → C}
{b : Limits.Cofan Y}
(hbu : IsUniversalColimit b)
(f : (i : ι) → X i ⟶ S)
(g : (i : ι') → Y i ⟶ S)
(u : a.pt ⟶ S)
(v : b.pt ⟶ S)
[∀ (i : ι), Limits.HasPullback (f i) v]
[Limits.HasPullback u v]
{P : ι × ι' → C}
{q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i}
{q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j}
(hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j))
(d : Limits.Cofan P)
(hd : Limits.IsColimit d)
(hu : ∀ (i : ι), CategoryStruct.comp (a.inj i) u = f i := by aesop_cat)
(hv : ∀ (i : ι'), CategoryStruct.comp (b.inj i) v = g i := by aesop_cat)
:
IsPullback (Limits.Cofan.IsColimit.desc hd fun (p : ι × ι') => CategoryStruct.comp (q₁ p.1 p.2) (a.inj p.1))
(Limits.Cofan.IsColimit.desc hd fun (p : ι × ι') => CategoryStruct.comp (q₂ p.1 p.2) (b.inj p.2)) u v