tmulEquivDep — Mathlib

English

The inverse of the dependent tensor product equivalence applied to a tensor equals the juxtaposition of the left and right components.

Русский

Обратный переход для зависимого тензорного произведения дает слева и справа разложение.

LaTeX

$$$\\bigl(\\mathrm{tmulEquivDep}\\;R\\;N\\bigr)^{\\!-1} (\\bigotimes i, f i) = \\bigl(\\bigotimes i, f(\\mathrm{Sum.inl}\, i)\\bigr) \\otimes \\bigl(\\bigotimes i, f(\\mathrm{Sum.inr}\, i)\\bigr)$$$

Lean4

/-- Equivalence between a `TensorProduct` of `PiTensorProduct`s and a single
`PiTensorProduct` indexed by a `Sum` type. If `N` is a constant family of
modules, use the non-dependent version `PiTensorProduct.tmulEquiv` instead. -/
def tmulEquivDep : (⨂[R] i₁, N (.inl i₁)) ⊗[R] (⨂[R] i₂, N (.inr i₂)) ≃ₗ[R] ⨂[R] i, N i :=
  LinearEquiv.ofLinear
    (TensorProduct.lift
      { toFun a := PiTensorProduct.lift (PiTensorProduct.lift (MultilinearMap.currySumEquiv (tprod R)) a)
        map_add' := by simp
        map_smul' := by simp })
    (PiTensorProduct.lift (MultilinearMap.domCoprodDep (tprod R) (tprod R)))
    (by
      ext
      dsimp
      simp only [lift.tprod, domCoprodDep_apply, lift.tmul, LinearMap.coe_mk, AddHom.coe_mk, currySum_apply]
      congr
      ext (_ | _) <;> simp)
    (TensorProduct.ext (by aesop))

Похожие утверждения