preservesBiproducts_shrink — Mathlib

English

If a functor preserves biproducts at a large universe level, then it preserves biproducts at a smaller universe level.

Русский

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

LaTeX

$$$\text{PreservesBiproducts} F \Rightarrow \text{PreservesBiproducts}_{w_1} F$$$

Lean4

/-- Preserving biproducts at a bigger universe level implies preserving biproducts at a
smaller universe level. -/
theorem preservesBiproducts_shrink (F : C ⥤ D) [PreservesZeroMorphisms F] [PreservesBiproducts.{max w₁ w₂} F] :
    PreservesBiproducts.{w₁} F :=
  ⟨fun {_} =>
    ⟨fun {_} =>
      ⟨fun {b} ib =>
        ⟨((F.mapBicone b).whiskerIsBilimitIff _).toFun
            (isBilimitOfPreserves F ((b.whiskerIsBilimitIff Equiv.ulift.{w₂}).invFun ib))⟩⟩⟩⟩

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