mk_eq — Mathlib

English

If two representatives x,y ∈ Σ j, F.obj j map to the same element under the colimit relation, then their MonCat.M.mk representatives are equal.

Русский

Если два представителя колимитной эквидности эквивалентны между собой, то их представления в M.mk равны.

LaTeX

$$$\forall x,y, \; \big(\exists k, f: x.1 \to k, g: y.1 \to k, F.map f\, x.2 = F.map g\, y.2\big) \Rightarrow M.mk F x = M.mk F y.$$$

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) :
    M.mk.{v, u} F x = M.mk F y :=
  Quot.eqvGen_sound (Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel (F ⋙ forget MonCat) x y h)

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