mk_eq — Mathlib

English

The forgetful functor from CommGrpCat to Type preserves epimorphisms; i.e., epimorphisms in CommGrpCat map to surjective functions on the underlying sets.

Русский

Функтор забывания из CommGrpCat в Type сохраняет эпиморфизмы; то есть эпиморфизмы в CommGrpCat переходят в сюръективные отображения на множестве.

LaTeX

$$$$ \mathrm{PreservesEpimorphisms}(\mathrm{forget CommGrpCat}) $$$$

Lean4

@[to_additive]
theorem mk_eq (x y : Σ j, F.obj j) (h : ∃ (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2) :
    G.mk.{v, u} F x = G.mk F y :=
  Quot.eqvGen_sound (Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel (F ⋙ forget GrpCat) x y h)

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