English
If two biproducts are indexed by equivalent types and multiplied by corresponding isomorphisms, then they are isomorphic. The whisker equivalence provides an explicit isomorphism between ⨁ f and ⨁ g.
Русский
Если два биопродукта индексируются эквивалентными типами и допускают сочетание с соответствующими изоморфизмами, то они изоморфны. Связка whiskerEquiv задаёт явное изоморождение между ⨁ f и ⨁ g.
LaTeX
$$$\\text{If } e: J \\simeq K \\text{ and } w_j: g(e(j)) \\cong f(j) \\text{ with biproducts } ⨁ f, ⨁ g, \\text{then } ⨁ f \\cong ⨁ g.$$$
Lean4
/-- Two biproducts which differ by an equivalence in the indexing type,
and up to isomorphism in the factors, are isomorphic.
Unfortunately there are two natural ways to define each direction of this isomorphism
(because it is true for both products and coproducts separately).
We give the alternative definitions as lemmas below. -/
@[simps]
def whiskerEquiv {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] :
⨁ f ≅ ⨁ g where
hom := biproduct.desc fun j => (w j).inv ≫ biproduct.ι g (e j)
inv := biproduct.desc fun k => eqToHom (by simp) ≫ (w (e.symm k)).hom ≫ biproduct.ι f _
