sigmaComparison_map_desc — Mathlib

English

Given HasCoproduct f and HasCoproduct (G.obj (f b)) for all b, the sigmaComparison map composed with G.map (Sigma.desc g) equals Sigma.desc (j ↦ G.map (g j)).

Русский

При наличии coproducts f и coproducts G.obj(f b) для всех b, выполняется выражение sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc (j ↦ G.map (g j)).

LaTeX

$$$\\sigma\\text{-}Comparison G f \\;\\circ\\; G.map(\\Sigma.\\desc g) = \\Sigma.\\desc (j \\mapsto G(g_j)).$$$

Lean4

@[reassoc (attr := simp)]
theorem sigmaComparison_map_desc [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (P : C) (g : ∀ j, f j ⟶ P) :
    sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j => G.map (g j) :=
  by
  ext j
  simp only [ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]

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