mapBiprod_inv_map_desc — Mathlib

English

Under preservation assumptions, biprodComparison F X Y is a split epi, i.e., has a section.

Русский

При условии сохранения би-производного, biprodComparison F X Y является разложимым эпиморфизмом (имеет секцию).

LaTeX

$$$\\text{IsSplitEpi}(\\text{biprodComparison}(F,X,Y))$$$

Lean4

theorem mapBiprod_inv_map_desc (f : X ⟶ W) (g : Y ⟶ W) :
    (F.mapBiprod X Y).inv ≫ F.map (biprod.desc f g) = biprod.desc (F.map f) (F.map g) := by
  ext <;> simp [mapBiprod, ← F.map_comp]

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