colimit_mul_mk_eq — Mathlib

English

In the filtered colimit of GrpCat, the product of two canonical representatives equals the canonical representative at a suitable index with the product of mapped components.

Русский

В колимите GrpCat произведение двух канонических представителей равно каноническому представителю в подходящем индексе, с произведением отображённых компонентов.

LaTeX

$$$G.mk F x * G.mk F y = G.mk F ⟨k, F.map f x.2 * F.map g y.2⟩$$$

Lean4

@[to_additive]
theorem colimit_mul_mk_eq (x y : Σ j, F.obj j) (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k) :
    G.mk.{v, u} F x * G.mk F y = G.mk F ⟨k, F.map f x.2 * F.map g y.2⟩ :=
  MonCat.FilteredColimits.colimit_mul_mk_eq _ _ _ _ _ _

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