diagonalSuccIsoFree_inv_hom_single

English

Inverse on a simple tensor of a pair of singles maps to a single with product of the first components.

Русский

Обратное на тензор простых элементов single возвращает единичный элемент со произведением первой компоненты.

LaTeX

$$$$ (\\text{diagonalSuccIsoFree } k\, G\, n).inv.hom (\\mathrm{single} f (\\mathrm{single} g a)) = \\mathrm{single} (g • \\mathrm{partialProd} f) a. $$$$

Lean4

theorem diagonalSuccIsoFree_inv_hom_single (g : G →₀ k) (f : Fin n → G) :
    (diagonalSuccIsoFree k G n).inv.hom (single f g) = lift _ k G (fun a => single (a • Fin.partialProd f) 1) g :=
  g.induction (by simp) fun _ _ _ _ _ _ =>
    by
    rw [single_add, map_add, diagonalSuccIsoFree_inv_hom_single_single]
    simp_all [sum_add_index']

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