colimitSMulAux_eq_of_rel — Mathlib

English

If two representatives are related in the colimit type, then their colimitSMulAux values are equal after evaluating with the same scalar.

Русский

Если два представителя связаны в типе колимита, то их значения colimitSMulAux равны после применения одного и того же скаляра.

LaTeX

$$$$ \\text{If } h: x \\sim y \\Rightarrow \\text{colimitSMulAux}(F,r,x) = \\text{colimitSMulAux}(F,r,y) $$$$

Lean4

theorem colimitSMulAux_eq_of_rel (r : R) (x y : Σ j, F.obj j)
    (h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y) : colimitSMulAux F r x = colimitSMulAux F r y :=
  by
  apply M.mk_eq
  obtain ⟨k, f, g, hfg⟩ := h
  use k, f, g
  simp only [Functor.comp_obj, Functor.comp_map, forget_map] at hfg
  simp [hfg]

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