hasWidePushouts_shrink — Mathlib

English

If a category has wide pushouts at a higher universe level, it also has wide pushouts at a lower universe level; universes can be shrunk along an equivalence of shapes.

Русский

Если у категории существуют широкие объединения на более высокой вселенной, то они существуют и на более низкой вселенной; вселенные можно сжимать через эквиваленцию форм.

LaTeX

$$$[HasWidePushouts^{\\max w w'} C] \\Rightarrow HasWidePushouts^{w} C$$$

Lean4

/-- If a category has wide pushouts on a higher universe level it also has wide pushouts
on a lower universe level. -/
theorem hasWidePushouts_shrink [HasWidePushouts.{max w w'} C] : HasWidePushouts.{w} C := fun _ =>
  hasColimitsOfShape_of_equivalence (WidePushoutShape.equivalenceOfEquiv _ Equiv.ulift.{w'})

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