isLimitMapConeEquiv — Mathlib

English

For a diagram c in C and a functor G: C → D, there is a natural equivalence between the limit property of the mapped cone and the limit property of the original cone after applying G.

Русский

Для диаграммы c в C и функторa G: C → D существует естественное эквивалентность между лимитностью отображённого конуса и лимитностью исходного конуса после применения G.

LaTeX

$$$IsLimit(mapCone\\ G\\ c) \\simeq IsLimit(c.map\\ G)$$$

Lean4

/-- The map (as a cone) of a pullback cone is limit iff
the map (as a pullback cone) is limit. -/
def isLimitMapConeEquiv : IsLimit (mapCone G c) ≃ IsLimit (c.map G) :=
  (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).symm.trans <|
    IsLimit.equivIsoLimit <| by
      refine PullbackCone.ext (Iso.refl _) ?_ ?_
      · dsimp only [fst]
        simp
      · dsimp only [snd]
        simp

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