reflectsLimitsOfSize_of_univLE — Mathlib

English

A functor that reflects larger limits also reflects smaller limits; more precisely, ReflectsLimitsOfShape and related size notions transfer to smaller universes.

Русский

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

LaTeX

$$$[\\text{UnivLE}] \\; [\\mathrm{ReflectsLimitsOfShape}\\,J\\,F] \\Rightarrow [\\mathrm{ReflectsLimitsOfShape}\\,J\\,F]_{0,0}$$$

Lean4

/-- A functor reflecting larger limits also reflects smaller limits. -/
theorem reflectsLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
    [ReflectsLimitsOfSize.{w', w₂'} F] : ReflectsLimitsOfSize.{w, w₂} F where
  reflectsLimitsOfShape
    {J} := reflectsLimitsOfShape_of_equiv ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F

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