English
The coprodEquiv is a linear equivalence between pairs of maps and a single map from the product domain to the codomain, with a canonical inverse given by composing with inl and inr.
Русский
CoprodEquiv — линейная эквивалентность между парами отображений и одним отображением из произведения в кодом, с каноническим обратным отображением через inl и inr.
LaTeX
$$$$ \text{coprodEquiv} : ((M_1 \to_L[R] M) \times (M_2 \to_L[R] M)) \simeq_L M_1 \times M_2 \to_L[R] M $$$$
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.
TODO: Upgrade this to a `ContinuousLinearEquiv`. This should be true for any topological
vector space over a normed field thanks to `ContinuousLinearMap.precomp` and
`ContinuousLinearMap.postcomp`. -/
@[simps]
def coprodEquiv [ContinuousAdd M₁] [ContinuousAdd M₂] [Semiring S] [Module S M] [ContinuousConstSMul S M]
[SMulCommClass R S M] : ((M₁ →L[R] M) × (M₂ →L[R] M)) ≃ₗ[S] M₁ × M₂ →L[R] M
where
toFun f := f.1.coprod f.2
invFun f := (f.comp (.inl ..), f.comp (.inr ..))
left_inv f := by simp
right_inv f := by simp [← comp_coprod f (.inl R M₁ M₂)]
map_add' a b := coprod_add ..
map_smul' r
a := by
dsimp
ext <;> simp [smul_apply]
