coconeOfCoconeUncurryIsColimit — Mathlib

English

`coconeOfCoconeUncurry Q c` is a colimit cocone when `c` is a colimit cocone.

Русский

Кокон coconeOfCoconeUncurry Q c является колимитным коконом, если c является колимитным коконом.

LaTeX

$$$\text{coconeOfCoconeUncurry } Q c\ text{ is a colimit cocone whenever } c \text{ is a colimit cocone.}$$$

Lean4

/-- `coconeOfCoconeUncurry Q c` is a colimit cocone when `c` is a colimit cocone.
-/
def coconeOfCoconeUncurryIsColimit {D : DiagramOfCocones F} (Q : ∀ j, IsColimit (D.obj j)) {c : Cocone (uncurry.obj F)}
    (P : IsColimit c) : IsColimit (coconeOfCoconeUncurry Q c)
    where
  desc
    s :=
    P.desc
      { pt := s.pt
        ι :=
          { app := fun p => (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1
            naturality := fun p p' f => by
              dsimp; simp only [Category.assoc]
              rcases p with ⟨j, k⟩
              rcases p' with ⟨j', k'⟩
              rcases f with ⟨fj, fk⟩
              dsimp
              slice_lhs 2 3 => rw [(D.obj j').ι.naturality]
              simp only [Functor.const_obj_map, Category.assoc]
              have w := (D.map fj).w k
              dsimp at w
              slice_lhs 1 2 => rw [← w]
              have n := s.ι.naturality fj
              dsimp at n
              simp only [Category.comp_id] at n
              rw [← n]
              simp } }
  fac s
    j := by
    apply (Q j).hom_ext
    intro k
    simp
  uniq s m
    w :=
    by
    refine
      P.uniq
        { pt := s.pt
          ι := _ } m ?_
    rintro ⟨j, k⟩
    dsimp
    rw [← w j]
    simp

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