map'_comp_map' — Mathlib

English

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

Русский

Пусть имеются семейства f,g,h над C, индексы α,β; для отображения p: α→β, морфизмов q и q' удовлетворяющих условию, верно равенство композиции Sigma.map' p q и Sigma.map' p' q'.

LaTeX

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

Lean4

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

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