colimitGroup — Mathlib

English

The filtered colimit G F of a functor F: J ⥤ GrpCat carries a natural group structure on its carrier, making the colimit object a group.

Русский

Фильтрованный колимит G F функторa F: J ⥤ GrpCat естественно порождает групповую структуру на носителе и тем колимитный объект становится группой.

LaTeX

$$Group (GrpCat.FilteredColimits.G F).carrier$$

Lean4

@[to_additive]
noncomputable instance colimitGroup : Group (G.{v, u} F) :=
  { colimitInv.{v, u} F, (G.{v, u} F).str with
    inv_mul_cancel := fun x => by
      refine Quot.inductionOn x ?_; clear x; intro x
      change (G.mk _ _)⁻¹ * G.mk _ _ = _
      obtain ⟨j, x⟩ := x
      simp [colimit_inv_mk_eq, colimit_mul_mk_eq F ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j), colimit_one_eq F j] }

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