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'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.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'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ⟶ G)
[CategoryTheory.IsIso α]
:
theorem
CategoryTheory.NatTrans.Equifibered.comp
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{H : CategoryTheory.Functor J C}
{α : F ⟶ G}
{β : G ⟶ H}
(hα : CategoryTheory.NatTrans.Equifibered α)
(hβ : CategoryTheory.NatTrans.Equifibered β)
:
theorem
CategoryTheory.NatTrans.Equifibered.whiskerRight
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ⟶ G}
(hα : CategoryTheory.NatTrans.Equifibered α)
(H : CategoryTheory.Functor C D)
[(i j : J) → (f : j ⟶ i) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (α.app i) (G.map f)) H]
:
theorem
CategoryTheory.NatTrans.Equifibered.whiskerLeft
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{K : Type u_3}
[CategoryTheory.Category.{u_4, u_3} K]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
{α : F ⟶ G}
(hα : CategoryTheory.NatTrans.Equifibered α)
(H : CategoryTheory.Functor K J)
:
theorem
CategoryTheory.mapPair_equifibered
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
{F' : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
(α : F ⟶ F')
:
theorem
CategoryTheory.NatTrans.equifibered_of_discrete
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{ι : Type u_3}
{F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C}
{G : CategoryTheory.Functor (CategoryTheory.Discrete ι) C}
(α : F ⟶ G)
:
def
CategoryTheory.IsUniversalColimit
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.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'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.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'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
(H : CategoryTheory.IsVanKampenColimit c)
:
noncomputable def
CategoryTheory.IsVanKampenColimit.isColimit
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
(h : CategoryTheory.IsVanKampenColimit c)
:
A van Kampen colimit is a colimit.
Equations
Instances For
theorem
CategoryTheory.IsUniversalColimit.of_iso
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
{c' : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.IsUniversalColimit c)
(e : c ≅ c')
:
theorem
CategoryTheory.IsVanKampenColimit.of_iso
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
{c' : CategoryTheory.Limits.Cocone F}
(H : CategoryTheory.IsVanKampenColimit c)
(e : c ≅ c')
:
theorem
CategoryTheory.IsVanKampenColimit.precompose_isIso
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ⟶ G)
[CategoryTheory.IsIso α]
{c : CategoryTheory.Limits.Cocone G}
(hc : CategoryTheory.IsVanKampenColimit c)
:
theorem
CategoryTheory.IsUniversalColimit.precompose_isIso
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ⟶ G)
[CategoryTheory.IsIso α]
{c : CategoryTheory.Limits.Cocone G}
(hc : CategoryTheory.IsUniversalColimit c)
:
theorem
CategoryTheory.IsVanKampenColimit.precompose_isIso_iff
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{G : CategoryTheory.Functor J C}
(α : F ⟶ G)
[CategoryTheory.IsIso α]
{c : CategoryTheory.Limits.Cocone G}
:
theorem
CategoryTheory.IsUniversalColimit.of_mapCocone
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
(G : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
[CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G]
[CategoryTheory.Limits.ReflectsColimitsOfShape J G]
(hc : CategoryTheory.IsUniversalColimit (G.mapCocone c))
:
theorem
CategoryTheory.IsVanKampenColimit.of_mapCocone
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
(G : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
[(i j : J) →
(X : C) →
(f : X ⟶ F.obj j) → (g : i ⟶ j) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (F.map g)) G]
[(i : J) → (X : C) → (f : X ⟶ c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.ι.app i)) G]
[CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan G]
[CategoryTheory.Limits.PreservesColimitsOfShape J G]
[CategoryTheory.Limits.ReflectsColimitsOfShape J G]
(H : CategoryTheory.IsVanKampenColimit (G.mapCocone c))
:
theorem
CategoryTheory.IsVanKampenColimit.mapCocone_iff
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
(G : CategoryTheory.Functor C D)
{F : CategoryTheory.Functor J C}
{c : CategoryTheory.Limits.Cocone F}
[CategoryTheory.IsEquivalence G]
:
CategoryTheory.IsVanKampenColimit (G.mapCocone c) ↔ CategoryTheory.IsVanKampenColimit c
theorem
CategoryTheory.IsUniversalColimit.whiskerEquivalence
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{K : Type u_3}
[CategoryTheory.Category.{u_4, u_3} K]
(e : J ≌ K)
{F : CategoryTheory.Functor K C}
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.IsUniversalColimit c)
:
theorem
CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{K : Type u_3}
[CategoryTheory.Category.{u_4, u_3} K]
(e : J ≌ K)
{F : CategoryTheory.Functor K C}
{c : CategoryTheory.Limits.Cocone F}
:
theorem
CategoryTheory.IsVanKampenColimit.whiskerEquivalence
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{K : Type u_3}
[CategoryTheory.Category.{u_4, u_3} K]
(e : J ≌ K)
{F : CategoryTheory.Functor K C}
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.IsVanKampenColimit c)
:
theorem
CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{K : Type u_3}
[CategoryTheory.Category.{u_4, u_3} K]
(e : J ≌ K)
{F : CategoryTheory.Functor K C}
{c : CategoryTheory.Limits.Cocone F}
:
theorem
CategoryTheory.isVanKampenColimit_of_evaluation
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasPullbacks D]
[CategoryTheory.Limits.HasColimitsOfShape J D]
(F : CategoryTheory.Functor J (CategoryTheory.Functor C D))
(c : CategoryTheory.Limits.Cocone F)
(hc : ∀ (x : C), CategoryTheory.IsVanKampenColimit (((CategoryTheory.evaluation C D).obj x).mapCocone c))
:
theorem
CategoryTheory.IsUniversalColimit.map_reflective
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
{Gl : CategoryTheory.Functor C D}
{Gr : CategoryTheory.Functor D C}
(adj : Gl ⊣ Gr)
[CategoryTheory.Full Gr]
[CategoryTheory.Faithful Gr]
{F : CategoryTheory.Functor J D}
{c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F Gr)}
(H : CategoryTheory.IsUniversalColimit c)
[∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)]
[(X : D) →
(f : X ⟶ Gl.obj c.pt) →
CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl]
:
CategoryTheory.IsUniversalColimit (Gl.mapCocone c)
theorem
CategoryTheory.IsVanKampenColimit.map_reflective
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasColimitsOfShape J C]
{Gl : CategoryTheory.Functor C D}
{Gr : CategoryTheory.Functor D C}
(adj : Gl ⊣ Gr)
[CategoryTheory.Full Gr]
[CategoryTheory.Faithful Gr]
{F : CategoryTheory.Functor J D}
{c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp F Gr)}
(H : CategoryTheory.IsVanKampenColimit c)
[∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)]
[(X : D) →
(f : X ⟶ Gl.obj c.pt) →
CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl]
[(X : C) →
(i : J) → (f : X ⟶ c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.ι.app i)) Gl]
:
CategoryTheory.IsVanKampenColimit (Gl.mapCocone c)
theorem
CategoryTheory.hasStrictInitial_of_isUniversal
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasInitial C]
(H : CategoryTheory.IsUniversalColimit
(CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.id (⊥_ C))
(CategoryTheory.CategoryStruct.id (⊥_ C))))
:
theorem
CategoryTheory.isVanKampenColimit_of_isEmpty
{J : Type v'}
[CategoryTheory.Category.{u', v'} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasStrictInitialObjects C]
[IsEmpty J]
{F : CategoryTheory.Functor J C}
(c : CategoryTheory.Limits.Cocone F)
(hc : CategoryTheory.Limits.IsColimit c)
:
theorem
CategoryTheory.BinaryCofan.isVanKampen_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(c : CategoryTheory.Limits.BinaryCofan X Y)
:
CategoryTheory.IsVanKampenColimit c ↔ ∀ {X' Y' : C} (c' : CategoryTheory.Limits.BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
CategoryTheory.CategoryStruct.comp αX (CategoryTheory.Limits.BinaryCofan.inl c) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inl c') f →
CategoryTheory.CategoryStruct.comp αY (CategoryTheory.Limits.BinaryCofan.inr c) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inr c') f →
(Nonempty (CategoryTheory.Limits.IsColimit c') ↔ CategoryTheory.IsPullback (CategoryTheory.Limits.BinaryCofan.inl c') αX f
(CategoryTheory.Limits.BinaryCofan.inl c) ∧ CategoryTheory.IsPullback (CategoryTheory.Limits.BinaryCofan.inr c') αY f
(CategoryTheory.Limits.BinaryCofan.inr c))
theorem
CategoryTheory.BinaryCofan.isVanKampen_mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(c : CategoryTheory.Limits.BinaryCofan X Y)
(cofans : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y)
(colimits : (X Y : C) → CategoryTheory.Limits.IsColimit (cofans X Y))
(cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PullbackCone f g)
(limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.IsLimit (cones f g))
(h₁ : ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
CategoryTheory.CategoryStruct.comp αX (CategoryTheory.Limits.BinaryCofan.inl c) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inl (cofans X' Y')) f →
CategoryTheory.CategoryStruct.comp αY (CategoryTheory.Limits.BinaryCofan.inr c) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inr (cofans X' Y')) f →
CategoryTheory.IsPullback (CategoryTheory.Limits.BinaryCofan.inl (cofans X' Y')) αX f
(CategoryTheory.Limits.BinaryCofan.inl c) ∧ CategoryTheory.IsPullback (CategoryTheory.Limits.BinaryCofan.inr (cofans X' Y')) αY f
(CategoryTheory.Limits.BinaryCofan.inr c))
(h₂ : {Z : C} →
(f : Z ⟶ c.pt) →
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.BinaryCofan.mk
(CategoryTheory.Limits.PullbackCone.fst (cones f (CategoryTheory.Limits.BinaryCofan.inl c)))
(CategoryTheory.Limits.PullbackCone.fst (cones f (CategoryTheory.Limits.BinaryCofan.inr c)))))
:
theorem
CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasInitial C]
{X : C}
{Y : C}
{c : CategoryTheory.Limits.BinaryCofan X Y}
(h : CategoryTheory.IsVanKampenColimit c)
:
theorem
CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasInitial C]
{c : CategoryTheory.Limits.BinaryCofan X Y}
(h : CategoryTheory.IsVanKampenColimit c)
:
CategoryTheory.IsPullback
(CategoryTheory.Limits.initial.to
((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }))
(CategoryTheory.Limits.initial.to
((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
(CategoryTheory.Limits.BinaryCofan.inl c) (CategoryTheory.Limits.BinaryCofan.inr c)
theorem
CategoryTheory.isUniversalColimit_extendCofan
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{n : ℕ}
(f : Fin (n + 1) → C)
{c₁ : CategoryTheory.Limits.Cofan fun (i : Fin n) => f (Fin.succ i)}
{c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt}
(t₁ : CategoryTheory.IsUniversalColimit c₁)
(t₂ : CategoryTheory.IsUniversalColimit c₂)
[∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.BinaryCofan.inr c₂) i]
:
theorem
CategoryTheory.isVanKampenColimit_extendCofan
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{n : ℕ}
(f : Fin (n + 1) → C)
{c₁ : CategoryTheory.Limits.Cofan fun (i : Fin n) => f (Fin.succ i)}
{c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt}
(t₁ : CategoryTheory.IsVanKampenColimit c₁)
(t₂ : CategoryTheory.IsVanKampenColimit c₂)
[∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.BinaryCofan.inr c₂) i]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
theorem
CategoryTheory.isPullback_of_cofan_isVanKampen
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasInitial C]
{ι : Type u_3}
{X : ι → C}
{c : CategoryTheory.Limits.Cofan X}
(hc : CategoryTheory.IsVanKampenColimit c)
(i : ι)
(j : ι)
[DecidableEq ι]
:
CategoryTheory.IsPullback
(if h : j = i then CategoryTheory.eqToHom (_ : (if j = i then X i else ⊥_ C) = X i)
else
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (if j = i then X i else ⊥_ C) = ⊥_ C))
(CategoryTheory.Limits.initial.to (X i)))
(if h : j = i then CategoryTheory.eqToHom (_ : (if j = i then X i else ⊥_ C) = X j)
else
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (if j = i then X i else ⊥_ C) = ⊥_ C))
(CategoryTheory.Limits.initial.to (X j)))
(CategoryTheory.Limits.Cofan.inj c i) (CategoryTheory.Limits.Cofan.inj c j)
theorem
CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasInitial C]
{ι : Type u_3}
{F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C}
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.IsVanKampenColimit c)
(i : CategoryTheory.Discrete ι)
(j : CategoryTheory.Discrete ι)
(hi : i ≠ j)
:
CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (F.obj i)) (CategoryTheory.Limits.initial.to (F.obj j))
(c.ι.app i) (c.ι.app j)
theorem
CategoryTheory.mono_of_cofan_isVanKampen
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasInitial C]
{ι : Type u_3}
{F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C}
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.IsVanKampenColimit c)
(i : CategoryTheory.Discrete ι)
:
CategoryTheory.Mono (c.ι.app i)