ι_colimitPointwiseProductToProductColimit_π

English

For pointwise products over a discrete index, the colimit-pointwise product-to-product colimit interacts with projections via a natural isomorphism.

Русский

Для покомпонентного произведения над дискретным индексом колимитно-точечное произведение взаимодействует с проекциями через естественный изоморфизм.

LaTeX

$$ι_colimitPointwiseProductToProductColimit_π (k) (s)$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitPointwiseProductToProductColimit_π (k : ∀ i, I i) (s : α) :
    colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π _ s =
      Pi.π _ s ≫ colimit.ι (F s) (k s) :=
  by simp [colimitPointwiseProductToProductColimit]

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