ι_comp_sigmaComparison — Mathlib

English

For coproductions indexed by a sigma type, the inclusion maps satisfy Sigma.ι _ b ≫ sigmaComparison G f = G.map (Sigma.ι f b).

Русский

Для coproducts, индексируемых сигма-типом, выполняется тождество Sigma.ι b ≫ sigmaComparison G f = G.map (Sigma.ι f b).

LaTeX

$$$\\Sigma.ι_{f,b} \\;\\circ\\; \\sigma\\text{-}\\,\\text{Comparison} = G(\\Sigma.ι f b).$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_comp_sigmaComparison [HasCoproduct f] [HasCoproduct fun b => G.obj (f b)] (b : β) :
    Sigma.ι _ b ≫ sigmaComparison G f = G.map (Sigma.ι f b) :=
  colimit.ι_desc _ (Discrete.mk b)

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