English
The left argument independence analogue: if y ∼ y' in the right argument, then colimitMulAux(F, x, y) = colimitMulAux(F, x, y').
Русский
Аналогично для правого аргумента: если y эквивалентно y' в правом аргументе, тогда colimitMulAux(F, x, y) = colimitMulAux(F, x, y').
LaTeX
$$$\text{If } y \sim y' \text{, then } \mathrm{colimitMulAux}^{\,\!}(F, x, y) = \mathrm{colimitMulAux}^{\,\!}(F, x, y').$$$
Lean4
/-- Multiplication in the colimit is well-defined in the right argument. -/
@[to_additive /-- Addition in the colimit is well-defined in the right argument. -/
]
theorem colimitMulAux_eq_of_rel_right {x y y' : Σ j, F.obj j}
(hyy' : Types.FilteredColimit.Rel (F ⋙ forget MonCat) y y') :
colimitMulAux.{v, u} F x y = colimitMulAux.{v, u} F x y' :=
by
obtain ⟨j₁, y⟩ := y; obtain ⟨j₂, x⟩ := x; obtain ⟨j₃, y'⟩ := y'
obtain ⟨l, f, g, hfg⟩ := hyy'
simp only [Functor.comp_obj, Functor.comp_map, forget_map] at hfg
obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
IsFiltered.tulip (IsFiltered.rightToMax j₂ j₁) (IsFiltered.leftToMax j₂ j₁) (IsFiltered.leftToMax j₂ j₃)
(IsFiltered.rightToMax j₂ j₃) f g
apply M.mk_eq
use s, α, γ
dsimp
simp_rw [MonoidHom.map_mul, ← ConcreteCategory.comp_apply, ← F.map_comp, h₁, h₂, h₃, F.map_comp,
ConcreteCategory.comp_apply, hfg]
