hasBinaryBiproduct_of_preserves — Mathlib

English

The morphism biprodComparison' F X Y is split mono (again, via a right inverse).

Русский

Морфизм biprodComparison' F X Y является разложимым моно (с правым обратным).

LaTeX

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

Lean4

instance hasBinaryBiproduct_of_preserves : HasBinaryBiproduct (F.obj X) (F.obj Y) :=
  HasBinaryBiproduct.mk
    { bicone := F.mapBinaryBicone (BinaryBiproduct.bicone X Y)
      isBilimit := isBinaryBilimitOfPreserves F (BinaryBiproduct.isBilimit _ _) }

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