mulHom_apply — Mathlib

English

The multiplication morphism mulHom on 𝒜 ᵍ⊗[R] ℬ is given by applying auxEquiv inverse to the graded multiplication of the images of x and y under auxEquiv.

Русский

Морфизм умножения mulHom на 𝒜 ᵍ⊗[R] ℬ задаётся через применение обратного auxEquiv к градаированной умножению образов x и y под действием auxEquiv.

LaTeX

$$$\mathrm{mulHom}_{𝒜,ℬ}(x,y) = (\mathrm{auxEquiv}_R(𝒜,ℬ))^{-1}\big( \mathrm{gradedMul}_R(𝒜·)(ℬ·)(\mathrm{auxEquiv}_R(𝒜,ℬ)(x),\mathrm{auxEquiv}_R(𝒜,ℬ)(y))\big)$$$

Lean4

theorem mulHom_apply (x y : 𝒜 ᵍ⊗[R] ℬ) :
    mulHom 𝒜 ℬ x y = (auxEquiv R 𝒜 ℬ).symm (gradedMul R (𝒜 ·) (ℬ ·) (auxEquiv R 𝒜 ℬ x) (auxEquiv R 𝒜 ℬ y)) :=
  rfl

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