isUniversalColimit_extendCofan — Mathlib

English

If c₁ and c₂ are universal colimits, and appropriate pullback exist, then extendCofan c₁ c₂ is a universal colimit.

Русский

Если c₁ и c₂ — универсальные колимиты, и существует соответствующий пуллбаэк, то extendCofan c₁ c₂ является универсальным колимитом.

LaTeX

$$$IsUniversalColimit(c₁) \\land IsUniversalColimit(c₂) \\land \\forall i, HasPullback(c₂.inr, i) \\Rightarrow IsUniversalColimit(ExtendCofan(c₁,c₂))$$$

Lean4

theorem isUniversalColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C) {c₁ : Cofan fun i : Fin n ↦ f i.succ}
    {c₂ : BinaryCofan (f 0) c₁.pt} (t₁ : IsUniversalColimit c₁) (t₂ : IsUniversalColimit c₂)
    [∀ {Z} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i] : IsUniversalColimit (extendCofan c₁ c₂) :=
  by
  intro F c α i e hα H
  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']
  have t₁' :=
    @t₁ (Discrete.functor (fun j ↦ F.obj ⟨j.succ⟩))
      (Cofan.mk (pullback c₂.inr i) fun j ↦ pullback.lift (α.app _ ≫ c₁.inj _) (c.ι.app _) ?_)
      (Discrete.natTrans fun i ↦ α.app _) (pullback.fst _ _) ?_ (NatTrans.equifibered_of_discrete _) ?_
  rotate_left
  ·
    simpa only [Functor.const_obj_obj, pair_obj_right, Discrete.functor_obj, 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⟩
  · ext j
    dsimp
    simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Cofan.inj]
  · intro j
    simp only [pair_obj_right, Functor.const_obj_obj, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app,
      Discrete.natTrans_app]
    refine IsPullback.of_right ?_ ?_ (IsPullback.of_hasPullback (BinaryCofan.inr c₂) i).flip
    · simp only [Functor.const_obj_obj, pair_obj_right, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
      exact H _
    · simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Cofan.inj]
  obtain ⟨H₁⟩ := t₁'
  have t₂' :=
    @t₂ (pair (F.obj ⟨0⟩) (pullback c₂.inr i)) (BinaryCofan.mk (c.ι.app ⟨0⟩) (pullback.snd _ _))
      (mapPair (α.app _) (pullback.fst _ _)) i ?_ (mapPair_equifibered _) ?_
  rotate_left
  · ext ⟨⟨⟩⟩
    · simpa [mapPair] using congr_app e ⟨0⟩
    · simpa using pullback.condition
  · rintro ⟨⟨⟩⟩
    · simp only [pair_obj_right, Functor.const_obj_obj, pair_obj_left, BinaryCofan.mk_pt, BinaryCofan.ι_app_left,
        BinaryCofan.mk_inl, mapPair_left]
      exact H ⟨0⟩
    · simp only [pair_obj_right, Functor.const_obj_obj, BinaryCofan.mk_pt, BinaryCofan.ι_app_right, BinaryCofan.mk_inr,
        mapPair_right]
      exact (IsPullback.of_hasPullback (BinaryCofan.inr c₂) i).flip
  obtain ⟨H₂⟩ := t₂'
  clear_value F'
  subst this
  refine
    ⟨IsColimit.ofIsoColimit (extendCofanIsColimit (fun i ↦ (Discrete.functor F').obj ⟨i⟩) H₁ H₂) <|
        Cocones.ext (Iso.refl _) ?_⟩
  dsimp
  rintro ⟨j⟩
  simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Category.comp_id]
  induction j using Fin.inductionOn
  · simp only [Fin.cases_zero]
  · simp only [Fin.cases_succ]

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