English
The hom component of the isomorphism between biproducts given by whiskerEquiv is computed by a universal construction from the projections and the given isomorphisms w j.
Русский
Гом-компонента изоморфизма между биопродуктами, полученного через whiskerEquiv, задаётся универсальным образом через проекции и данные изоморфизмы w j.
LaTeX
$$$\\text{whiskerEquiv}.hom = \\text{biproduct.lift }\\lambda k. \\text{biproduct.π } f (e^{-1}(k)) \\circ (w_{k})^{-1} \\circ \\text{eqToHom}(``).$$$
Lean4
theorem whiskerEquiv_hom_eq_lift {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f]
[HasBiproduct g] :
(biproduct.whiskerEquiv e w).hom =
biproduct.lift fun k => biproduct.π f (e.symm k) ≫ (w _).inv ≫ eqToHom (by simp) :=
by
simp only [whiskerEquiv_hom]
ext k j
by_cases h : k = e j
· subst h
simp
· simp only [ι_desc_assoc, Category.assoc, lift_π]
rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
· simp
· rintro rfl
simp at h
· exact Ne.symm h
