lift_tmul — Mathlib

English

The lift map from graded tensor product to C takes tmul to the product of f a and g b under certain anti-commuting relations.

Русский

lift отображение обратно в C переводит tmul в произведение f(a)g(b) с учётом противо- commute условий.

LaTeX

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

Lean4

@[simp]
theorem lift_tmul (f : A →ₐ[R] C) (g : B →ₐ[R] C)
    (h_anti_commutes : ∀ ⦃i j⦄ (a : 𝒜 i) (b : ℬ j), f a * g b = (-1 : ℤˣ) ^ (j * i) • (g b * f a)) (a : A) (b : B) :
    lift 𝒜 ℬ f g h_anti_commutes (a ᵍ⊗ₜb) = f a * g b :=
  rfl

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