English
One can reindex a biproduct along an equivalence ε between index sets β and γ, obtaining an isomorphism between ⨁ f ∘ ε and ⨁ f. This isomorphism is given by desc and lift maps built from the appropriate injections and projections.
Русский
Можно переставлять индексы би-производного по эквивалентности между индексными множествами, получая изоморфизм между ⨁ f ∘ ε и ⨁ f, задаваемый соответствующими отображениями desc и lift.
LaTeX
$$$\operatorname{biproduct}(f\circ ε) \cong \operatorname{biproduct} f$$$
Lean4
/-- Reindex a categorical biproduct via an equivalence of the index types. -/
@[simps]
def reindex {β γ : Type} [Finite β] (ε : β ≃ γ) (f : γ → C) [HasBiproduct f] [HasBiproduct (f ∘ ε)] : ⨁ f ∘ ε ≅ ⨁ f
where
hom := biproduct.desc fun b => biproduct.ι f (ε b)
inv := biproduct.lift fun b => biproduct.π f (ε b)
hom_inv_id := by
ext b b'
by_cases h : b' = b
· subst h; simp
· have : ε b' ≠ ε b := by simp [h]
simp [biproduct.ι_π_ne _ h, biproduct.ι_π_ne _ this]
inv_hom_id := by
classical
cases nonempty_fintype β
ext g g'
by_cases h : g' = g <;>
simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite, Equiv.apply_eq_iff_eq_symm_apply, h]
