comp_reflectsLimit — Mathlib

English

If G reflects limits and H reflects limits, then F ⋙ G reflects limits.

Русский

Если G отражает пределы и H отражает пределы, то F ⋙ G отражает пределы.

LaTeX

$$$\\text{ReflectsLimit}(G,H) \\Rightarrow \\text{ReflectsLimit}(F \\circ G,H).$$$

Lean4

instance (priority := 100) comp_reflectsLimit {B : Type u₄} [Category.{v₄} B] {H : E ⥤ B} [ReflectsLimit G H] :
    ReflectsLimit (F ⋙ G) H where
  reflects {c}
    hc := by
    refine ⟨isLimitExtendConeEquiv F _ (isLimitOfReflects H ?_)⟩
    let hc' := (isLimitExtendConeEquiv (G := G ⋙ H) F _).symm hc
    exact IsLimit.ofIsoLimit hc' (Cones.ext (Iso.refl _) (by simp))

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