isoObjConePointsOfIsLimit — Mathlib

English

If a PreservesLimit₂ instance exists, there is a natural isomorphism between the limit of the uncurry construction and the image of the pair of limits under G.

Русский

Если существует PreservesLimit₂, то есть естественный изоморфизм между пределом uncurry и изображением пары пределов через G.

LaTeX

$$$\\text{PreservesLimit₂.isoObjConePointsOfIsLimit}$$$

Lean4

/-- Given a `PreservesLimit₂` instance, extract the isomorphism between
a limit of `uncurry.obj (whiskeringLeft₂ C|>.obj K₁|>.obj K₂|>.obj G)` and
`(G.obj c₁).obj c₂` where c₁ (resp. c₂) is a limit of `K₁` (resp `K₂`). -/
noncomputable def isoObjConePointsOfIsLimit {c₁ : Cone K₁} (hc₁ : IsLimit c₁) {c₂ : Cone K₂} (hc₂ : IsLimit c₂)
    {c₃ : Cone <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)} (hc₃ : IsLimit c₃) :
    (G.obj c₁.pt).obj c₂.pt ≅ c₃.pt :=
  IsLimit.conePointUniqueUpToIso (isLimitOfPreserves₂ G hc₁ hc₂) hc₃

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