English
The inverse of the whiskerEquiv is given by a biproduct.lift of the projections composed with the isomorphisms w j.
Русский
Обратное к whiskerEquiv задаётся как lift-отображение биопродукта через проекции и изоморфизмы w j.
LaTeX
$$$(\\text{biproduct.whiskerEquiv } e w).{\\rm inv} = \\text{biproduct.lift } (\\lambda j. \\text{biproduct.π } g (e(j)) \\circ (w_j)^{\\,hom}).$$$
Lean4
theorem whiskerEquiv_inv_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).inv = biproduct.lift fun j => biproduct.π g (e j) ≫ (w j).hom :=
by
simp only [whiskerEquiv_inv]
ext j k
by_cases h : k = e j
· subst h
simp only [ι_desc_assoc, ← eqToHom_iso_hom_naturality_assoc w (e.symm_apply_apply j).symm, Equiv.symm_apply_apply,
eqToHom_comp_ι, Category.assoc, bicone_ι_π_self, Category.comp_id, lift_π, bicone_ι_π_self_assoc]
· simp only [ι_desc_assoc, Category.assoc, lift_π]
rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
· simp
· exact h
· rintro rfl
simp at h
