English
If there is an equivalence e: C ≌ D and C has HasColimitsOfShape J and HasExactColimitsOfShape J, then D has HasExactColimitsOfShape J.
Русский
Если существует эквивалентность e: C ≌ D и в C существуют колимиты и точные колимиты формы J, то и в D существуют точные колимиты формы J.
LaTeX
$$$\text{HasExactColimitsOfShape}(J,D)$ under an equivalence $e: C \simeq D$ supplied with $\text{HasColimitsOfShape}(J,C)$ and $\text{HasExactColimitsOfShape}(J,C)$$$
Lean4
theorem of_codomain_equivalence (J : Type*) [Category J] {D : Type*} [Category D] (e : C ≌ D) [HasColimitsOfShape J C]
[HasExactColimitsOfShape J C] :
haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
HasExactColimitsOfShape J D :=
by
haveI : HasColimitsOfShape J D := Adjunction.hasColimitsOfShape_of_equivalence e.inverse
refine ⟨⟨fun _ _ _ => ⟨@fun K => ?_⟩⟩⟩
refine preservesLimit_of_natIso K (?_ : e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim)
apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso
exact isoWhiskerLeft (_ ⋙ colim) e.unitIso.symm ≪≫ (preservesColimitNatIso e.inverse).symm
