rightAdjoint_preservesLimits — Mathlib

English

Transport of colimits across an equivalence in size-labelled form.

Русский

Перенос колимитов через эквивалентность в форме размера.

LaTeX

$$$$ HasColimitsOfSize^{v,u}(C) \\gets HasColimitsOfSize^{v,u}(D) \\text{ for equivalence } E: C\\to D. $$$$

Lean4

/-- A right adjoint preserves limits. -/
@[stacks 0038]
theorem rightAdjoint_preservesLimits : PreservesLimitsOfSize.{v, u} G where
  preservesLimitsOfShape :=
    {
      preservesLimit :=
        {
          preserves := fun hc =>
            ⟨IsLimit.isoUniqueConeMorphism.inv fun _ =>
                @Equiv.unique _ _ (IsLimit.isoUniqueConeMorphism.hom hc _)
                  ((adj.functorialityAdjunction' _).homEquiv _ _).symm⟩ } }

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