coneOfConeUncurry — Mathlib

English

A construction that, given a diagram of cones and a cone over the uncurry of a two-variable functor, yields a cone over the original diagram of cones.

Русский

Построение, которое из диаграммы конусов и конуса над uncurryobj F даёт конус над исходной диаграммой конусов.

LaTeX

$$$\\text{coneOfConeUncurry}(D,Q,c) : \\text{Cone } D.\\mathrm{conePoints}$$$

Lean4

/-- Given a diagram `D` of limit cones over the `F.obj j`, and a cone over `uncurry.obj F`,
we can construct a cone over the diagram consisting of the cone points from `D`.
-/
@[simps]
def coneOfConeUncurry {D : DiagramOfCones F} (Q : ∀ j, IsLimit (D.obj j)) (c : Cone (uncurry.obj F)) : Cone D.conePoints
    where
  pt := c.pt
  π :=
    { app := fun j =>
        (Q j).lift
          { pt := c.pt
            π :=
              { app := fun k => c.π.app (j, k)
                naturality := fun k k' f => by
                  simpa using @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j, k') (𝟙 j, f) } }
      naturality := fun j j' f =>
        (Q j').hom_ext (fun k => by simpa using @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j', k) (f, 𝟙 k)) }

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