English
Two maps from M × M₂ to M₃ are equal iff they agree after precomposing with inl and inr, i.e., extensionality on product maps.
Русский
Два отображения из M × M₂ в M₃ равны тогда и только тогда, когда они равны после пресекачивания через inl и inr, т.е. экстенсиональность на отображениях произведения.
LaTeX
$$$ f = g \\iff f \\circ (inl\\ R\\ M\\ M_2) = g \\circ (inl\\ R\\ M\\ M_2) \\land f \\circ (inr\\ R\\ M\\ M_2) = g \\circ (inr\\ R\\ M\\ M_2) $$$
Lean4
/-- Taking the product of two maps with the same codomain is equivalent to taking the product of
their domains.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/
@[simps]
def coprodEquiv [Module S M₃] [SMulCommClass R S M₃] : ((M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ≃ₗ[S] M × M₂ →ₗ[R] M₃
where
toFun f := f.1.coprod f.2
invFun f := (f.comp (inl _ _ _), f.comp (inr _ _ _))
left_inv f := by simp only [coprod_inl, coprod_inr]
right_inv f := by simp only [← comp_coprod, comp_id, coprod_inl_inr]
map_add' a
b := by
ext
simp only [Prod.snd_add, add_apply, coprod_apply, Prod.fst_add, add_add_add_comm]
map_smul' r
a := by
dsimp
ext
simp only [smul_add, smul_apply, coprod_apply]
