tmul_coe_mul_zero_coe_tmul — Mathlib

English

In the presence of an algebra map on B, the graded tensor product multiplication distributes through the algebra map: (a1 ᵍ⊗ b1) * (algebraMap r ᵍ⊗ b2) = (a1 a'1) ᵍ⊗ (b1 b2) with a' chosen appropriately.

Русский

При наличии алгебраического отображения на B умножение в градуированном тензорном произведении распределяется через отображение: (a1 ᵍ⊗ b1) * (algebraMap r ᵍ⊗ b2) = (a1 a2) ᵍ⊗ (b1 b2).

LaTeX

$$$(a_1 ᵍ⊗ b_1) * (\mathrm{algebraMap}_R B(r) ᵍ⊗ b_2) = (a_1 a_r) ᵍ⊗ (b_1 b_2)$$$

Lean4

/-- A special case for when `a₂` has grade 0. -/
theorem tmul_coe_mul_zero_coe_tmul {j₁ : ι} (a₁ : A) (b₁ : ℬ j₁) (a₂ : 𝒜 0) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (b₁ : B) * (a₂ : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = ((a₁ * a₂ : A) ᵍ⊗ₜ(b₁ * b₂ : B)) := by
  rw [tmul_coe_mul_coe_tmul, mul_zero, uzpow_zero, one_smul]

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