English
The injections into the reindexed coproduct commute with the reindexing isomorphism.
Русский
Вставки в реиндексированный coproduct коммутируют с изоморфизмом реиндексации.
LaTeX
$$$\Sigma.\ι (f\circ \varepsilon)\; b \; \; ≫ (\Sigma.\reindex\varepsilon f).\hom = \Sigma.\ι f (\varepsilon b)$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_reindex_hom (b : β) : Sigma.ι (f ∘ ε) b ≫ (Sigma.reindex ε f).hom = Sigma.ι f (ε b) :=
by
dsimp [Sigma.reindex]
simp only [HasColimit.isoOfEquivalence_hom_π, Functor.id_obj, Discrete.functor_obj, Function.comp_apply,
Discrete.equivalence_functor, Discrete.equivalence_inverse, Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv,
Category.id_comp]
have h := colimit.w (Discrete.functor f) (Discrete.eqToHom' (ε.apply_symm_apply (ε b)))
simp only [Discrete.functor_obj] at h
erw [← h, eqToHom_map, eqToHom_map, eqToHom_trans_assoc]
all_goals { simp
}
