English
There exists a canonical linear equivalence that reindexes the components of a Pi-tensor product along a bijection of the index set.
Русский
Существует каноническое линейное равнообразие, перенумеровывающее компоненты PiTensorProduct вдоль биективности индексов.
LaTeX
$$$\\text{There exists a linear isomorphism } \\operatorname{reindex}_{e}: \\bigotimes_{i\\in \\iota} s_i \\;\\cong_{R}\\; \\bigotimes_{i\\in \\iota_2} s_{e^{-1}(i)}$ where $e: \\iota \\isomto \\iota_2$.$$
Lean4
/-- Re-index the components of the tensor power by `e`. -/
def reindex (e : ι ≃ ι₂) : (⨂[R] i : ι, s i) ≃ₗ[R] ⨂[R] i : ι₂, s (e.symm i) :=
let f := domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₂), s (e.symm i)) e
let g := domDomCongrLinearEquiv' R R s (⨂[R] (i : ι), s i) e
LinearEquiv.ofLinear (lift <| f.symm <| tprod R) (lift <| g <| tprod R) (by aesop) (by aesop)
