isVanKampenColimit_extendCofan — Mathlib

English

Let C be a category with finite coproducts. For a natural number n and a map f : Fin(n+1) → C, form the cofan c1 on the tail of f (i ↦ f i.succ) and the binary cofan c2 with the object f(0) and vertex c1.pt. If c1 and c2 are Van Kampen colimits, and every pullback along c2.inr with any arrow into c2.pt exists, then the extended cofan extendCofan(c1,c2) is again a Van Kampen colimit. Equivalently, Van Kampen colimits are preserved under this particular gluing operation along the first leg.

Русский

Пусть C — категория с конечными копродуктами. Пусть n ∈ ℕ и f : Fin(n+1) → C. Пусть c1 — коган на хвосте f i.succ, а c2 — бинарный коган (f 0) c1.pt. Если c1 и c2 являются колимитами Ван-Кемпена, и для каждого Z и любого i ⟶ c2.pt существует тривиальный пассив-пуллапов, то склеенный коган extendCofan(c1,c2) снова является колимитом Ван-Кемпена. Эквивалентно, свойства универсальности сохраняются под этой операцией склейки.

LaTeX

$$$\\forall n\\, \\forall f : \\mathrm{Fin}(n+1) \\to \\mathcal{C},\\; \\exists c_1 : \\mathrm{Cofan} (\\lambda i:\\mathrm{Fin}\\,n \\mapsto f(i.succ)),\\; \\exists c_2 : \\mathrm{BinaryCofan} (f(0)) (c_1.pt),\\; t_1 : \\mathrm{IsVanKampenColimit}\, c_1,\\; t_2 : \\mathrm{IsVanKampenColimit}\, c_2,\\; [\\forall {Z} (i : Z \\to c_2.pt), \\mathrm{HasPullback}\\; c_2.inr i],\\; [\\mathrm{HasFiniteCoproducts}\\; C] \\,\\Rightarrow \\, \\mathrm{IsVanKampenColimit}(\\mathrm{extendCofan}(c_1,c_2)).$$

Lean4

theorem isVanKampenColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C) {c₁ : Cofan fun i : Fin n ↦ f i.succ}
    {c₂ : BinaryCofan (f 0) c₁.pt} (t₁ : IsVanKampenColimit c₁) (t₂ : IsVanKampenColimit c₂)
    [∀ {Z} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i] [HasFiniteCoproducts C] : IsVanKampenColimit (extendCofan c₁ c₂) :=
  by
  intro F c α i e hα
  refine ⟨?_, isUniversalColimit_extendCofan f t₁.isUniversal t₂.isUniversal c α i e hα⟩
  intro ⟨Hc⟩ ⟨j⟩
  have t₂' :=
    (@t₂ (pair (F.obj ⟨0⟩) (∐ fun (j : Fin n) ↦ F.obj ⟨j.succ⟩))
          (BinaryCofan.mk (P := c.pt) (c.ι.app _) (Sigma.desc fun b ↦ c.ι.app _))
          (mapPair (α.app _) (Sigma.desc fun b ↦ α.app _ ≫ c₁.inj _)) i ?_ (mapPair_equifibered _)).mp
      ⟨?_⟩
  rotate_left
  · ext ⟨⟨⟩⟩
    ·
      simpa only [pair_obj_left, Functor.const_obj_obj, pair_obj_right, Discrete.functor_obj, NatTrans.comp_app,
        mapPair_left, BinaryCofan.ι_app_left, BinaryCofan.mk_pt, BinaryCofan.mk_inl, Functor.const_map_app,
        extendCofan_pt, extendCofan_ι_app, Fin.cases_zero] using congr_app e ⟨0⟩
    · dsimp
      ext j
      simpa only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app, Category.assoc,
        extendCofan_pt, Functor.const_obj_obj, NatTrans.comp_app, extendCofan_ι_app, Fin.cases_succ,
        Functor.const_map_app] using congr_app e ⟨j.succ⟩
  · let F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
    have : F = Discrete.functor F' := by
      apply Functor.hext
      · exact fun i ↦ rfl
      · rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
        simp [F']
    clear_value F'
    subst this
    apply
      BinaryCofan.IsColimit.mk _
        (fun {T} f₁ f₂ ↦
          Hc.desc
            (Cofan.mk T (Fin.cases f₁ (fun i ↦ Sigma.ι (fun (j : Fin n) ↦ (Discrete.functor F').obj ⟨j.succ⟩) _ ≫ f₂))))
    · intro T f₁ f₂
      simp only [Discrete.functor_obj, pair_obj_left, BinaryCofan.mk_pt, Functor.const_obj_obj, BinaryCofan.mk_inl,
        IsColimit.fac, Cofan.mk_pt, Cofan.mk_ι_app, Fin.cases_zero]
    · intro T f₁ f₂
      simp only [Discrete.functor_obj, pair_obj_right, BinaryCofan.mk_pt, Functor.const_obj_obj, BinaryCofan.mk_inr]
      ext j
      simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app, IsColimit.fac, Fin.cases_succ]
    · intro T f₁ f₂ f₃ m₁ m₂
      simp at m₁ m₂ ⊢
      refine
        Hc.uniq
          (Cofan.mk T (Fin.cases f₁ (fun i ↦ Sigma.ι (fun (j : Fin n) ↦ (Discrete.functor F').obj ⟨j.succ⟩) _ ≫ f₂))) _
          ?_
      intro ⟨j⟩
      simp only [Discrete.functor_obj, Cofan.mk_pt, Functor.const_obj_obj, Cofan.mk_ι_app]
      induction j using Fin.inductionOn
      · simp only [Fin.cases_zero, m₁]
      · simp only [← m₂, colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app, Fin.cases_succ]
  induction j using Fin.inductionOn with
  | zero => exact t₂' ⟨WalkingPair.left⟩
  | succ j
    _ =>
    have t₁' :=
      (@t₁ (Discrete.functor (fun j ↦ F.obj ⟨j.succ⟩)) (Cofan.mk _ _) (Discrete.natTrans fun i ↦ α.app _)
            (Sigma.desc (fun j ↦ α.app _ ≫ c₁.inj _)) ?_ (NatTrans.equifibered_of_discrete _)).mp
        ⟨coproductIsCoproduct _⟩ ⟨j⟩
    rotate_left
    · ext ⟨j⟩
      dsimp
      rw [colimit.ι_desc]
      rfl
    simpa [Functor.const_obj_obj, Discrete.functor_obj, extendCofan_pt, extendCofan_ι_app, Fin.cases_succ,
      BinaryCofan.mk_pt, colimit.cocone_x, Cofan.mk_pt, Cofan.mk_ι_app, BinaryCofan.ι_app_right, BinaryCofan.mk_inr,
      colimit.ι_desc, Discrete.natTrans_app] using t₁'.paste_horiz (t₂' ⟨WalkingPair.right⟩)

Похожие утверждения