coconeOfCoconeUncurry — Mathlib

English

There is an IsPullback structure for the canonical pullback of FormalCoproducts along f and g with pb data.

Русский

Существует структура IsPullback для канонического обратного предела FormalCoproduct по f и g с данными pb.

LaTeX

$$$\\mathrm{IsPullback} (\\mathrm{pullbackCone}\\ f\\ g\\ pb).fst\\ (\\mathrm{pullbackCone}\\ f\\ g\\ pb).snd\\ f\\ g$$$

Lean4

/-- Given a diagram `D` of colimit cocones over the `F.obj j`, and a cocone over `uncurry.obj F`,
we can construct a cocone over the diagram consisting of the cocone points from `D`.
-/
@[simps]
def coconeOfCoconeUncurry {D : DiagramOfCocones F} (Q : ∀ j, IsColimit (D.obj j)) (c : Cocone (uncurry.obj F)) :
    Cocone D.coconePoints where
  pt := c.pt
  ι :=
    { app := fun j =>
        (Q j).desc
          { pt := c.pt
            ι :=
              { app := fun k => c.ι.app (j, k)
                naturality := fun k k' f => by
                  dsimp; simp only [Category.comp_id]
                  conv_lhs => arg 1; equals (F.map (𝟙 _)).app _ ≫ (F.obj j).map f => simp
                  conv_lhs => arg 1; rw [← uncurry_obj_map F (𝟙 j ×ₘ f)]
                  rw [c.w] } }
      naturality := fun j j' f =>
        (Q j).hom_ext
          (by
            dsimp
            intro k
            simp only [Limits.CoconeMorphism.w_assoc, Limits.Cocones.precompose_obj_ι, Limits.IsColimit.fac,
              NatTrans.comp_app, Category.comp_id, Category.assoc]
            have := @NatTrans.naturality _ _ _ _ _ _ c.ι (j, k) (j', k) (f, 𝟙 k)
            dsimp at this
            simp only [Category.comp_id, CategoryTheory.Functor.map_id] at this
            exact this) }

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