instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor

English

There is a colimit for the opposite of the discrete op functor composed with Z.

Русский

Существует колимит для противоположности дискретного оп-функторa, композиции с Z.

LaTeX

$$$\text{HasColimit}((\mathrm{Discrete.opposite}\, \alpha).inverse \circ (\mathrm{Discrete.functor} Z)^{\mathrm{op}})$$$

Lean4

instance : HasColimit ((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op) :=
  hasColimit_equivalence_comp (Discrete.opposite α).symm

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