reflectsLimit_of_comp — Mathlib

English

Let F: C → D be an initial functor and G: D → E, H: E → B be functors. If H reflects limits of shape F ∘ G, then H reflects limits of shape G.

Русский

Пусть F: C → D — начальный функтор, G: D → E, H: E → B — функторы. Если H отражает пределы по форме F ∘ G, то H отражает пределы по форме G.

LaTeX

$$$F \text{ initial} \wedge \\operatorname{ReflectsLimit}(F \\circ G, H) \\Rightarrow \\operatorname{ReflectsLimit}(G, H)$$$

Lean4

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

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