hasWidePullbacks_shrink — Mathlib

English

If wide pullbacks exist at a high universe, they exist at a lower universe; pushforward via equivalence of shapes shrinks universes.

Русский

Если существуют широкие вытянутые пределы на большой вселенной, то они существуют и на меньшей вселенной.

LaTeX

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

Lean4

/-- If a category has wide pullbacks on a higher universe level it also has wide pullbacks
on a lower universe level. -/
theorem hasWidePullbacks_shrink [HasWidePullbacks.{max w w'} C] : HasWidePullbacks.{w} C := fun _ =>
  hasLimitsOfShape_of_equivalence (WidePullbackShape.equivalenceOfEquiv _ Equiv.ulift.{w'})

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