tmul_coe_mul_coe_tmul — Mathlib

English

A comprehensive graded product formula for tmul of arbitrary elements a₁,b₁,a₂,b₂, giving the graded sign and the product: GradedMul equals sign times (a₁a₂) ᵍ⊗ (b₁b₂).

Русский

Обобщённая формула умножения для tmul элементов с произвольными градациями: знак умножения и произведение элементов дают (a₁a₂) ᵍ⊗ (b₁b₂).

LaTeX

$$$(a_1 ᵍ⊗ b_1) * (a_2 ᵍ⊗ b_2) = (-1)^{j_1 i_2} \cdot ((a_1 a_2) ᵍ⊗ (b_1 b_2)).$$$

Lean4

/-- The characterization of this multiplication on partially homogeneous elements. -/
theorem tmul_coe_mul_coe_tmul {j₁ i₂ : ι} (a₁ : A) (b₁ : ℬ j₁) (a₂ : 𝒜 i₂) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (b₁ : B) * (a₂ : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = (-1 : ℤˣ) ^ (j₁ * i₂) • ((a₁ * a₂ : A) ᵍ⊗ₜ(b₁ * b₂ : B)) :=
  by
  dsimp only [mul_def, mulHom_apply, of_symm_of]
  dsimp [auxEquiv, tmul]
  rw [decompose_coe, decompose_coe]
  simp_rw [← lof_eq_of R]
  rw [tmul_of_gradedMul_of_tmul]
  simp_rw [lof_eq_of R]
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specialize `map_smul` to `LinearEquiv.map_smul`

  rw [@Units.smul_def _ _ (_) (_), ← Int.cast_smul_eq_zsmul R, LinearEquiv.map_smul, map_smul, Int.cast_smul_eq_zsmul R,
    ← @Units.smul_def _ _ (_) (_)]
  rw [congr_symm_tmul]
  dsimp
  simp_rw [decompose_symm_mul, decompose_symm_of, Equiv.symm_apply_apply]

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