English
The map biproduct.toSubtype f p equals the described biproduct.desc with a sum over j: if p j then the corresponding injection, else 0.
Русский
Отображение biproduct.toSubtype f p равно описанному biproduct.desc с суммой по j: если p j выполнено, то соответствующая инъекция, иначе 0.
LaTeX
$$$\\text{biproduct.toSubtype } f p = \\text{biproduct.desc }(\\lambda j.\\; \\text{if } p j \\text{ then } \\text{biproduct.ι } (f j) \\langle j, \\cdot \\rangle \\text{ else } 0).$$$
Lean4
@[reassoc (attr := simp)]
theorem fromSubtype_π [DecidablePred p] (j : J) :
biproduct.fromSubtype f p ≫ biproduct.π f j = if h : p j then biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0 := by
classical
ext i; dsimp
rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π]
by_cases h : p j
· rw [dif_pos h, biproduct.ι_π]
split_ifs with h₁ h₂ h₂
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
· rw [dif_neg h, dif_neg (show (i : J) ≠ j from fun h₂ => h (h₂ ▸ i.2)), comp_zero]
