Documentation

Mathlib.CategoryTheory.Limits.VanKampen

Universal colimits and van Kampen colimits #

Main definitions #

References #

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
Instances For
    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} ( : Equifibered α) ( : 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} ( : 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} ( : Equifibered α) (H : Functor K J) :

    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

      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

        A universal colimit is a colimit.

        Equations
        Instances For

          A van Kampen colimit is a colimit.

          Equations
          Instances For
            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] :
            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] :
            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 fCategoryStruct.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 fCategoryStruct.comp αY c.inr = CategoryStruct.comp (cofans X' Y').inr fIsPullback (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.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] :
            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] :
            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.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] :

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

            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