colimitInvAux_eq_of_rel — Mathlib

English

If two representatives x,y are related by a relation in the filtered colimit, their inverses agree after applying the colimit inv-aux map.

Русский

Если два представителя x,y связаны отношением в фильтрованном колимите, их инверсы совпадают после применения колимитной вспомогательной карты инверсии.

LaTeX

$$colimitInvAux.{v, u} F x = colimitInvAux F y$$

Lean4

@[to_additive]
theorem colimitInvAux_eq_of_rel (x y : Σ j, F.obj j) (h : Types.FilteredColimit.Rel (F ⋙ forget GrpCat) x y) :
    colimitInvAux.{v, u} F x = colimitInvAux F y := by
  apply G.mk_eq
  obtain ⟨k, f, g, hfg⟩ := h
  use k, f, g
  rw [MonoidHom.map_inv, MonoidHom.map_inv, inv_inj]
  exact hfg

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