tmul_coe_mul_algebraMap_tmul — Mathlib

English

The lift map appropriately respects graded tensor multiplication against algebra maps, ensuring coherence with the algebra structure.

Русский

Лифт-отображение согласуется с градуированным тензорным умножением и алгебраическим отображением, поддерживая структуру алгебры.

LaTeX

$$$\text{lift}_{𝒜,ℬ}(f,g,h_{anti}) (a ᵍ⊗ b)= f(a) g(b)$$$

Lean4

theorem tmul_coe_mul_algebraMap_tmul {j₁ : ι} (a₁ : A) (b₁ : ℬ j₁) (r : R) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (b₁ : B) * algebraMap R A r ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = (a₁ * algebraMap R A r : A) ᵍ⊗ₜ(b₁ * b₂ : B) :=
  tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ b₁ (GAlgebra.toFun (A := (𝒜 ·)) r) b₂

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