leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single

English

For a trivial A, the composition H1π A with the hom of H1IsoOfIsTrivial equals the cocycles iso hom map.

Русский

Для тривиального A композиция H1π A с гомоморфизмом H1IsoOfIsTrivial равна гомоморфизму из кокосов.

LaTeX

$$$H1\\pi\\,A \\circ (H1IsoOfIsTrivial A)^{\\mathrm{hom}} = (cocycles₁IsoOfIsTrivial A)^{\\mathrm{hom}}$$$

Lean4

@[simp]
theorem leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single (i : α) (g : G) (r s : k) :
    DFunLike.coe (F := ↑(ModuleCat.of k (G →₀ k) ⊗ ModuleCat.of k (α →₀ k)) →ₗ[k] α →₀ G →₀ k)
        (leftRegularTensorTrivialIsoFree k G α).hom.hom.hom (single g r ⊗ₜ[k] single i s) =
      single i (single g (r * s)) :=
  by simp [leftRegularTensorTrivialIsoFree, tensorObj_def, ModuleCat.MonoidalCategory.tensorObj]

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