diagonalSuccIsoFree_inv_hom_single_single

English

Inverse on single element for diagonal-free iso maps single f g to a lifted form based on partial products.

Русский

Обратное на одиночном элементе диагонального свободного изоморфизма переводит single f g в поднесённую форму через частичные произведения.

LaTeX

$$$$ (\\text{diagonalSuccIsoFree } k\, G\, n).inv.hom (\\mathrm{single} f (g)) = \\mathrm{lift} \\_ k\\ G\\ (\\lambda a => \\mathrm{single} (a · \\mathrm{partialProd} f) 1) g. $$$$

Lean4

@[simp]
theorem diagonalSuccIsoFree_inv_hom_single_single (g : G) (f : Fin n → G) (a : k) :
    (diagonalSuccIsoFree k G n).inv.hom (single f (single g a)) = single (g • Fin.partialProd f) a :=
  by
  have := diagonalSuccIsoTensorTrivial_inv_hom_single_single g f a 1
  simp_all [diagonalSuccIsoFree, leftRegularTensorTrivialIsoFree_inv_hom_single_single (k := k)]

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