coinvariantsTensorFreeToFinsupp_mk_tmul_single

English

There is a linear map from α →₀ A to Coinvariants(A ⊗ free k G α), given by mapping a finsupp to the corresponding simple tensor image.

Русский

Существует линейное отображение из α →₀ A в коинварианты (A ⊗ free k G α), отображающее простейшее тензорное вложение для базисной функции.

LaTeX

$$$finsuppToCoinvariantsTensorFree : (α \\rightarrow₀ A) \\rightarrowₗ[k] Coinvariants (A ⊗ free k G α).ρ$$$

Lean4

@[simp]
theorem coinvariantsTensorFreeToFinsupp_mk_tmul_single (x : A) (i : α) (g : G) (r : k) :
    DFunLike.coe (F := (A.ρ.tprod (Representation.free k G α)).Coinvariants →ₗ[k] α →₀ A.V)
        (coinvariantsTensorFreeToFinsupp A α) (Coinvariants.mk _ (x ⊗ₜ single i (single g r))) =
      single i (r • A.ρ g⁻¹ x) :=
  by
  simp [tensorObj_def, ModuleCat.MonoidalCategory.tensorObj, coinvariantsTensorFreeToFinsupp, Coinvariants.map,
    finsuppTensorRight, TensorProduct.finsuppRight]

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