fromSubtype_toSubtype — Mathlib

English

For a subtype-parameterized biproduct, the injections commute with the subtype projection.

Русский

Для биопродукта с параметризацией по подтипу, инъекции коммутируют с проекцией подтипа.

LaTeX

$$$\\text{ι toSubtype } f p = \\text{ι} (Subtype.restrict p f)$$$

Lean4

@[reassoc (attr := simp)]
theorem fromSubtype_toSubtype : biproduct.fromSubtype f p ≫ biproduct.toSubtype f p = 𝟙 (⨁ Subtype.restrict p f) :=
  by
  refine biproduct.hom_ext _ _ fun j => ?_
  rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]

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