whiskerRight — Mathlib

English

If α is equifibered and H: C ⥤ D preserves certain cospan limits, then whiskerRight α H is equifibered.

Русский

Если α равнолистовое и H сохраняет определённые пределы по бикосцеплению, тогда whiskerRight α H также равнолистово.

LaTeX

$$Equifibered α → (PreservesLimit cospan ...) → Equifibered (whiskerRight α H)$$

Lean4

theorem whiskerRight {F G : J ⥤ C} {α : F ⟶ G} (hα : Equifibered α) (H : C ⥤ D)
    [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) H] : Equifibered (whiskerRight α H) :=
  fun _ _ f => (hα f).map H

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