English
The DomCoprod operator is the sum of summands after applying the quotient-morphism.
Русский
Оператор DomCoprod есть сумма summand после применения лурной мапы.
LaTeX
$$$$domCoprod a b = \sum_{σ} domCoprod.summand a b σ.$$$$
Lean4
/-- A more bundled version of `AlternatingMap.domCoprod` that maps
`((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂)` to `(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂`. -/
def domCoprod' : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] (Mᵢ [⋀^ιb]→ₗ[R'] N₂) →ₗ[R'] (Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂)) :=
TensorProduct.lift <| by
refine LinearMap.mk₂ R' domCoprod (fun m₁ m₂ n => ?_) (fun c m n => ?_) (fun m n₁ n₂ => ?_) fun c m n => ?_ <;>
· ext
simp only [domCoprod_apply, add_apply, smul_apply, ← Finset.sum_add_distrib, Finset.smul_sum,
MultilinearMap.sum_apply, domCoprod.summand]
congr
ext σ
refine Quotient.inductionOn' σ fun σ => ?_
simp only [Quotient.liftOn'_mk'', coe_add, coe_smul, MultilinearMap.smul_apply,
← MultilinearMap.domCoprod'_apply]
simp only [TensorProduct.add_tmul, ← TensorProduct.smul_tmul', TensorProduct.tmul_add, TensorProduct.tmul_smul,
LinearMap.map_add, LinearMap.map_smul]
first
| rw [← smul_add]
| rw [smul_comm]
rfl
