isLimitOfHasPullbackOfPreservesLimit

English

If C has pullbacks and G preserves pullbacks, then the mapped pullback cone is a pullback cone in the target category D.

Русский

Если в C существуют притяжения (pullbacks) и G сохраняет притяжения, то отображённый конус притяжения в D остаётся притяжением.

LaTeX

$$$IsLimitPullbackMapOfPreserves\\ G f g$$$

Lean4

/-- If `G` preserves pullbacks and `C` has them, then the pullback cone constructed of the mapped
morphisms of the pullback cone is a limit. -/
def isLimitOfHasPullbackOfPreservesLimit [HasPullback f g] :
    have : G.map (pullback.fst f g) ≫ G.map f = G.map (pullback.snd f g) ≫ G.map g := by
      simp only [← G.map_comp, pullback.condition]
    IsLimit (PullbackCone.mk (G.map (pullback.fst f g)) (G.map (pullback.snd f g)) this) :=
  isLimitPullbackConeMapOfIsLimit G _ (pullbackIsPullback f g)

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