of_domain_equivalence — Mathlib

English

Transport HasExactColimitsOfShape along a domain equivalence of shapes J ≃ J'.

Русский

Переноc HasExactColimitsOfShape вдоль эквивалентности формы J ≃ J'.

LaTeX

$$$\text{HasExactColimitsOfShape}(J',C)$ from $\text{HasExactColimitsOfShape}(J,C)$ via a domain equivalence $J\simeq J'$$$

Lean4

/-- Transport a `HasExactLimitsOfShape` along an equivalence of the shape.

Note: When `C` has finite colimits, this lemma holds with the equivalence replaced by a initial
functor, see `hasExactLimitsOfShape_of_initial` below.
-/
theorem of_domain_equivalence {J J' : Type*} [Category J] [Category J'] (e : J ≌ J') [HasLimitsOfShape J C]
    [HasExactLimitsOfShape J C] :
    haveI : HasLimitsOfShape J' C := hasLimitsOfShape_of_equivalence e
    HasExactLimitsOfShape J' C :=
  haveI : HasLimitsOfShape J' C := hasLimitsOfShape_of_equivalence e
  ⟨preservesFiniteColimits_of_natIso (Functor.Initial.limIso e.functor)⟩

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