isPullback_of_cofan_isVanKampen — Mathlib

English

Assume HasInitial C. Let c be a cocone which is a Van Kampen colimit for some diagram F : Discrete ι ⥤ C. For any i and j in ι, the square formed by the initial maps to X_i and X_j is a pullback, provided i and j are distinct.

Русский

Пусть C имеет начальный объект. Пусть c — когон, являющийся колимитом Ван-Кемпена для диаграммы F : Discrete ι ⥤ C. Тогда для любых i ≠ j ∈ ι квадрат, образованный начальными маппингами в X_i и X_j, является пуллбеком.

LaTeX

$$$\\forall i,j : ι,\\ i \\neq j\\;\\Rightarrow\\; \\mathrm{IsPullback}\\;\\bigl(P := (\\text{if } j=i \\text{ then } X_i \\text{ else } \\bot_C),\\; \\text{if } h:\\ j=i \\text{ then } \\mathrm{eqToHom}(\\text{if_pos } h) \\text{ else } \\mathrm{eqToHom}(\\text{if_neg } h) \\; \\overset{initial}{to}(X_i),\\; \\text{if } h:\\ j=i \\text{ then } \\mathrm{eqToHom}( (\\text{if_pos } h).trans (\\congr_arg X h.symm)) \\text{ else } \\mathrm{eqToHom}(\\text{if_neg } h) \\; \\overset{initial}{to}(X_j)\\bigr) $$

Lean4

theorem isPullback_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {X : ι → C} {c : Cofan X} (hc : IsVanKampenColimit c)
    (i j : ι) [DecidableEq ι] :
    IsPullback (P := (if j = i then X i else ⊥_ C))
      (if h : j = i then eqToHom (if_pos h) else eqToHom (if_neg h) ≫ initial.to (X i))
      (if h : j = i then eqToHom ((if_pos h).trans (congr_arg X h.symm)) else eqToHom (if_neg h) ≫ initial.to (X j))
      (Cofan.inj c i) (Cofan.inj c j) :=
  by
  refine
    (hc
          (Cofan.mk (X i) (f := fun k ↦ if k = i then X i else ⊥_ C)
            (fun k ↦ if h : k = i then (eqToHom <| if_pos h) else (eqToHom <| if_neg h) ≫ initial.to _))
          (Discrete.natTrans
            (fun k ↦
              if h : k.1 = i then (eqToHom <| (if_pos h).trans (congr_arg X h.symm))
              else (eqToHom <| if_neg h) ≫ initial.to _))
          (c.inj i) ?_ (NatTrans.equifibered_of_discrete _)).mp
      ⟨?_⟩ ⟨j⟩
  · ext ⟨k⟩
    simp only [Discrete.functor_obj, Functor.const_obj_obj, NatTrans.comp_app, Discrete.natTrans_app, Cofan.mk_pt,
      Cofan.mk_ι_app, Functor.const_map_app]
    split
    · subst ‹k = i›; rfl
    · simp
  · refine mkCofanColimit _ (fun t ↦ (eqToHom (if_pos rfl).symm) ≫ t.inj i) ?_ ?_
    · intro t j
      simp only [Cofan.mk_pt, cofan_mk_inj]
      split
      · subst ‹j = i›; simp
      · rw [Category.assoc, ← IsIso.eq_inv_comp]
        exact initialIsInitial.hom_ext _ _
    · intro t m hm
      simp [← hm i]

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