hasExactLimitsOfShape — Mathlib

English

An adjunction with suitable properties transfers exact limits of shape J from D to C.

Русский

Сопряжённость с нужными свойствами переносит точные пределы формы J из D в C.

LaTeX

$$$\text{HasExactLimitsOfShape}(J,C)$ from $\text{HasExactLimitsOfShape}(J,D)$ via adjunction$$

Lean4

/-- Let `adj : F ⊣ G` be an adjunction, with `F : C ⥤ D` coreflective.
Assume that `C` has finite colimits and `G` commutes to them.
If `D` has exact limits of shape `J`, then `C` also has exact limits of shape `J`. -/
theorem hasExactLimitsOfShape (adj : F ⊣ G) [F.Full] [F.Faithful] (J : Type u') [Category.{v'} J] [HasLimitsOfShape J C]
    [HasLimitsOfShape J D] [HasExactLimitsOfShape J D] [HasFiniteColimits C] [PreservesFiniteColimits G] :
    HasExactLimitsOfShape J C where
  preservesFiniteColimits :=
    ⟨fun K _ _ ↦
      ⟨fun {H} ↦ by
        have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits
        have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits
        let e : (whiskeringRight J _ _).obj F ⋙ lim ⋙ G ≅ lim :=
          isoWhiskerLeft _ (preservesLimitNatIso G) ≪≫
            (Functor.associator _ _ _).symm ≪≫
              isoWhiskerRight (whiskeringRightObjCompIso F G) _ ≪≫
                isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) _ ≪≫
                  isoWhiskerRight whiskeringRightObjIdIso _ ≪≫ lim.leftUnitor
        exact preservesColimit_of_natIso _ e⟩⟩

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