map'_comp_map — Mathlib

English

For f : α → C, g : β → C, h : γ → C with HasCoproducts, and p : α → β, q : α → f a ⟶ g(p a), q' : β → g b ⟶ h(p b), Sigma.map' p q ≫ Sigma.map' p q' = Sigma.map' p (λ a, q a ≫ q'(p a)).

Русский

Для f,g,h над α,β,γ с копроизведениями, верно равенство композиции Sigma.map' p q с Sigma.map' p q'.

LaTeX

$$$\\Sigma\\text{map}' p q \\;\\circ\\; \\Sigma\\text{map}' p q' = \\Sigma\\text{map}' p (a \\mapsto q a \\circ q'(p a))$$$

Lean4

theorem map'_comp_map {f : α → C} {g h : β → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (p : α → β)
    (q : ∀ (a : α), f a ⟶ g (p a)) (q' : ∀ (b : β), g b ⟶ h b) :
    Sigma.map' p q ≫ Sigma.map q' = Sigma.map' p (fun a => q a ≫ q' (p a)) := by ext; simp

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