finitaryExtensive_functor — Mathlib

English

If an arrow g is an isomorphism, then every cospan with f, g is preserved by the functor F; i.e., limits along walking cospans are preserved.

Русский

Если стрелка g является изоморфизмом, то любая коспановая диаграмма с f, g сохраняется функтором F; то есть пределы вдоль шагающего коспана сохраняются.

LaTeX

$$$IsIso(g)\Rightarrow PreservesLimit(\mathrm{cospan}(f,g),F)$$$

Lean4

instance finitaryExtensive_functor [HasPullbacks C] [FinitaryExtensive C] : FinitaryExtensive (D ⥤ C) :=
  haveI : HasFiniteCoproducts (D ⥤ C) := ⟨fun _ => Limits.functorCategoryHasColimitsOfShape⟩
  ⟨fun c hc => isVanKampenColimit_of_evaluation _ c fun _ => FinitaryExtensive.vanKampen _ <| isColimitOfPreserves _ hc⟩

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