English
An adjunction F ⊣ G, with G full and faithful, preserves exact colimits of shape J from C to D under suitable hypotheses.
Русский
При наличии сопряжённости F ⊣ G, где G полно и удовлетворяет условиям, точные колимиты формы J переносятся из C в D.
LaTeX
$$$\text{HasExactColimitsOfShape}(J,D)$ under $F \dashv G$ with $G$ full/faithful and hypotheses$$
Lean4
/-- Let `adj : F ⊣ G` be an adjunction, with `G : D ⥤ C` reflective.
Assume that `D` has finite limits and `F` commutes to them.
If `C` has exact colimits of shape `J`, then `D` also has exact colimits of shape `J`. -/
theorem hasExactColimitsOfShape (adj : F ⊣ G) [G.Full] [G.Faithful] (J : Type u') [Category.{v'} J]
[HasColimitsOfShape J C] [HasColimitsOfShape J D] [HasExactColimitsOfShape J C] [HasFiniteLimits D]
[PreservesFiniteLimits F] : HasExactColimitsOfShape J D where
preservesFiniteLimits :=
⟨fun K _ _ ↦
⟨fun {H} ↦ by
have : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjoint_preservesLimits
have : PreservesColimitsOfSize.{v', u'} F := adj.leftAdjoint_preservesColimits
let e : (whiskeringRight J D C).obj G ⋙ colim ⋙ F ≅ colim :=
isoWhiskerLeft _ (preservesColimitNatIso F) ≪≫
(Functor.associator _ _ _).symm ≪≫
isoWhiskerRight (whiskeringRightObjCompIso G F) _ ≪≫
isoWhiskerRight ((whiskeringRight J D D).mapIso (asIso adj.counit)) _ ≪≫
isoWhiskerRight whiskeringRightObjIdIso _ ≪≫ colim.leftUnitor
exact preservesLimit_of_natIso _ e⟩⟩
