English
The composition biproduct.fromSubtype f p followed by biproduct.toSubtype f p is the identity on ⨁ Subtype.restrict p f.
Русский
Сложение biproduct.fromSubtype f p затем biproduct.toSubtype f p равно тождественному отображению на ⨁ Subtype.restrict p f.
LaTeX
$$$\\text{biproduct.fromSubtype } f p \\circ \\text{biproduct.toSubtype } f p = \\mathrm{Id}_{⨁ (Subtype.restrict p f)}$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_toSubtype [DecidablePred p] (j : J) :
biproduct.ι f j ≫ biproduct.toSubtype f p = if h : p j then biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0 := by
classical
ext i
rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, 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 j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_comp]
