English
For any index set J and function f, the composition from the j-th injection to the j-th projection is the identity on f(j).
Русский
Для любого индекса j композиция внедрения в j-ю компоненту и проекции из неё возвращает тождество на f(j).
LaTeX
$$$\forall J\, C\, (f: J \to C)\; [HasBiproduct f] \; (j: J)\; (biproduct.ι\, f\, j) \; \ggs \; (biproduct.π\, f\, j) = \mathrm{id}_{f(j)}$$$
Lean4
/-- Note that as this lemma has an `if` in the statement, we include a `DecidableEq` argument.
This means you may not be able to `simp` using this lemma unless you `open scoped Classical`. -/
@[reassoc]
theorem ι_π [DecidableEq J] (f : J → C) [HasBiproduct f] (j j' : J) :
biproduct.ι f j ≫ biproduct.π f j' = if h : j = j' then eqToHom (congr_arg f h) else 0 := by
convert (biproduct.bicone f).ι_π j j'
