preservesBiproduct_of_epi_biproductComparison'

English

If a map of a biproduct is an isomorphism, the matrix of components yields a split mono/epi factorizations.

Русский

Если отображение биопродукта является изоморфизмом, то его матрица компонент дает разложение на разложение моно/эпиморфизм.

LaTeX

$$$f: X_1 \oplus X_2 \to Y_1 \oplus Y_2, \; f \text{ is iso} \Rightarrow \text{matrix of } f \text{ splits}$$$

Lean4

/-- If the (coproduct-like) biproduct comparison for `F` and `f` is an epimorphism, then `F`
preserves the biproduct of `F` and `f`. For the converse, see `mapBiproduct`. -/
theorem preservesBiproduct_of_epi_biproductComparison' {f : J → C} [HasBiproduct f] [HasBiproduct (F.obj ∘ f)]
    [Epi (biproductComparison' F f)] : PreservesBiproduct f F :=
  by
  haveI : Epi (splitEpiBiproductComparison F f).section_ := by simpa
  haveI : IsIso (biproductComparison F f) := IsIso.of_epi_section' (splitEpiBiproductComparison F f)
  apply preservesBiproduct_of_mono_biproductComparison

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