preserves_lift_mapCone — Mathlib

English

If G preserves finite limits of cones, then the lift in G of a cone maps in a way compatible with G, i.e., G(lift_C) = lift_{G(C)}.

Русский

Если G сохраняет конечные пределы конусов, функционал G сохраняет подъем конуса: G(lift_C) = lift_{G(C)}.

LaTeX

$$$\\operatorname{preservesLimit}\\;F\\;G \\Rightarrow (\\mathrm{isLimitOfPreserves}\\;G\\;t).lift\\; (G.mapCone\\; _ ) = G.map (t.lift \\; _)$$$

Lean4

@[simp]
theorem preserves_lift_mapCone (c₁ c₂ : Cone F) (t : IsLimit c₁) :
    (isLimitOfPreserves G t).lift (G.mapCone c₂) = G.map (t.lift c₂) :=
  ((isLimitOfPreserves G t).uniq (G.mapCone c₂) _ (by simp [← G.map_comp])).symm

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