English
Given x = (j1, x1) and y = (j2, y1) and a common refinement k with morphisms f: j1 → k and g: j2 → k, one has
Русский
Найдя общий верхний предел k иMorphisms f: j1 → k, g: j2 → k, выполняется
LaTeX
$$$M.mk F x \; * \; M.mk F y = M.mk F \langle k, F.map f\, x_1 \;\cdot\; F.map g\, y_1 \rangle$$$
Lean4
/-- Multiplication in the colimit is independent of the chosen "maximum" in the filtered category.
In particular, this lemma allows us to "unfold" the definition of the multiplication of `x` and `y`,
using a custom object `k` and morphisms `f : x.1 ⟶ k` and `g : y.1 ⟶ k`.
-/
@[to_additive /-- Addition in the colimit is independent of the chosen "maximum" in the filtered
category. In particular, this lemma allows us to "unfold" the definition of the addition of
`x` and `y`, using a custom object `k` and morphisms `f : x.1 ⟶ k` and `g : y.1 ⟶ k`. -/
]
theorem colimit_mul_mk_eq (x y : Σ j, F.obj j) (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k) :
M.mk.{v, u} F x * M.mk F y = M.mk F ⟨k, F.map f x.2 * F.map g y.2⟩ :=
by
obtain ⟨j₁, x⟩ := x; obtain ⟨j₂, y⟩ := y
obtain ⟨s, α, β, h₁, h₂⟩ := IsFiltered.bowtie (IsFiltered.leftToMax j₁ j₂) f (IsFiltered.rightToMax j₁ j₂) g
refine M.mk_eq F _ _ ?_
use s, α, β
dsimp
simp_rw [MonoidHom.map_mul, ← ConcreteCategory.comp_apply, ← F.map_comp, h₁, h₂]
