of_codomain_equivalence — Mathlib

English

Transport HasLimitsOfShape and HasExactLimitsOfShape along an equivalence C ≌ D.

Русский

Перенос HasLimitsOfShape и HasExactLimitsOfShape через эквивалентность C ≌ D.

LaTeX

$$$\text{HasExactLimitsOfShape}(J,D)$ given $e: C \simeq D$ and $\text{HasLimitsOfShape}(J,C)$, $\text{HasExactLimitsOfShape}(J,C)$$$

Lean4

theorem of_codomain_equivalence (J : Type*) [Category J] {D : Type*} [Category D] (e : C ≌ D) [HasLimitsOfShape J C]
    [HasExactLimitsOfShape J C] :
    haveI : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse
    HasExactLimitsOfShape J D :=
  by
  haveI : HasLimitsOfShape J D := Adjunction.hasLimitsOfShape_of_equivalence e.inverse
  refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
  refine preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)
  apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
  exact isoWhiskerLeft (_ ⋙ lim) e.unitIso.symm ≪≫ (preservesLimitNatIso e.inverse).symm

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