finsuppToCoinvariantsTensorFree_single

English

A variant form of the single-element image for finsuppToCoinvariantsTensorFree; the single i x maps to the coinvariants class of x ⊗ single i (1).

Русский

Вариант изображения одиночного элемента для finsuppToCoinvariantsTensorFree; единичный элемент i x отображается в класс коинвариантов x ⊗ single i (1).

LaTeX

$$$finsuppToCoinvariantsTensorFree\\;A\\;α\\;single\\;i\\;x = Coinvariants.mk\\_\\; (x \\otimesₜ\\; single i (single 1 1))$$$

Lean4

@[simp]
theorem finsuppToCoinvariantsTensorFree_single (i : α) (x : A) :
    DFunLike.coe (F := (α →₀ A.V) →ₗ[k] (A.ρ.tprod (Representation.free k G α)).Coinvariants)
        (finsuppToCoinvariantsTensorFree A α) (single i x) =
      Coinvariants.mk _ (x ⊗ₜ single i (single (1 : G) (1 : k))) :=
  by simp [finsuppToCoinvariantsTensorFree, Coinvariants.map, ModuleCat.MonoidalCategory.tensorObj, tensorObj_def]

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