coprod_inr_leftDistrib_hom — Mathlib

English

In a monoidal category with binary coproducts and left distributivity, the right coprojection behaves compatibly with the left distributivity isomorphism ∂L X Y Z: the injection coprod.inr followed by ∂L.hom equals the right whiskering of coprod.inr.

Русский

В моноидальной категории с бинарными копроизведениями и левым распределением правая копроекция ведёт себя совместимо с изоморфизмом ∂L X Y Z: вложение coprod.inr затем ∂L.hom эквивалентно правому отнесению coprod.inr.

LaTeX

$$$\\operatorname{coprod.inr} \\circ (\\partial_L X Y Z)^{\\mathrm{hom}} = X \\triangleleft \\operatorname{coprod.inr}$$$

Lean4

@[reassoc (attr := simp)]
theorem coprod_inr_leftDistrib_hom [IsMonoidalLeftDistrib C] {X Y Z : C} :
    coprod.inr ≫ (∂L X Y Z).hom = X ◁ coprod.inr := by rw [leftDistrib_hom, coprod.inr_desc]

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