coinvariantsTensorFreeLEquiv_apply

English

An alternate presentation of the same map sends a ⟦x ⊗ₜ (g,r)⟧ to the function i ↦ r · ρ(g⁻¹) x at i.

Русский

Альтернативная формулировка отображения отправляет элемент ⟦x ⊗ₜ (g,r)⟧ в функция на индексе i, равную r · ρ(g⁻¹) x.

LaTeX

$$$coinvariantsTensorFreeToFinsupp_mk_tmul_single\\ (x)\\ (i)\\ (g)\\ (r) = single i (r \\cdot A.ρ g^{-1} x)$$$

Lean4

@[simp]
theorem coinvariantsTensorFreeLEquiv_apply (x : (A ⊗ free k G α).ρ.Coinvariants) :
    DFunLike.coe (F := (A.ρ.tprod (Representation.free k G α)).Coinvariants →ₗ[k] α →₀ A)
        (A.coinvariantsTensorFreeToFinsupp α) x =
      coinvariantsTensorFreeToFinsupp A α x :=
  by rfl

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