isoSum — Mathlib

English

Any functor out of a sum is the sum of its precomposition with the inclusions: for F : A ⊕ B ⥤ C, there is an iso F ≅ (inl ⋙ F).sum' (inr ⋙ F).

Русский

Любой функтор из суммы есть сумма его предобразов по включениям: для F : A ⊕ B ⥤ C существует изоморфизм F ≅ (inl ⋙ F) ⊔ (inr ⋙ F).

LaTeX

$$$ F \\cong (\\mathrm{inl}\\_A B \\gg F) \\;\\text{sum'}\\; (\\mathrm{inr}\\_A B \\gg F) $$$

Lean4

/-- Any functor out of a sum is the sum of its precomposition with the inclusions. -/
def isoSum : F ≅ (Sum.inl_ A B ⋙ F).sum' (Sum.inr_ A B ⋙ F) :=
  sumIsoExt (inlCompSum' _ _).symm (inrCompSum' _ _).symm

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