cancelBaseChange — Mathlib

English

The inverse associator sends a ⊗ (b ⊗ c) to (a ⊗ b) ⊗ c for a ∈ A, b ∈ C, c ∈ D.

Русский

Обратная к ассоциатору отображает a ⊗ (b ⊗ c) в (a ⊗ b) ⊗ c для a ∈ A, b ∈ C, c ∈ D.

LaTeX

$$$ (\\operatorname{assoc}_{R,S,A,C,D})^{-1}(a \\otimes (b \\otimes c)) = (a \\otimes b) \\otimes c $$$

Lean4

/-- The natural isomorphism `A ⊗[S] (S ⊗[R] B) ≃ₐ[T] A ⊗[R] B`. -/
def cancelBaseChange : A ⊗[S] (S ⊗[R] B) ≃ₐ[T] A ⊗[R] B :=
  AlgEquiv.symm <|
    AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.cancelBaseChange R S T A B).symm
        (by simp [Algebra.TensorProduct.one_def]) <|
      LinearMap.map_mul_of_map_mul_tmul (fun _ _ _ _ ↦ by simp)

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