English
For any g and f, liftAlternating composed with AltMaps equals AltMaps composed with liftAlternating; i.e., the construction is functorial and respects composition of alternating maps.
Русский
Для любых g и f композиция liftAlternating с AltMaps равна композиции AltMaps с liftAlternating; конструкция функториальна.
LaTeX
$$$liftAlternating\circ (g \circ\_AlternatingMap f) = g \circ liftAlternating f$$$
Lean4
@[simp]
theorem liftAlternating_ιMulti :
liftAlternating (R := R) (M := M) (N := ExteriorAlgebra R M) (ιMulti R) =
(LinearMap.id : ExteriorAlgebra R M →ₗ[R] ExteriorAlgebra R M) :=
by
ext v
dsimp
induction v using CliffordAlgebra.left_induction with
| algebraMap => rw [liftAlternating_algebraMap, ιMulti_zero_apply, Algebra.algebraMap_eq_smul_one]
| add _ _ hx hy => rw [map_add, hx, hy]
| ι_mul _ _ hx =>
simp_rw [liftAlternating_ι_mul, ιMulti_succ_curryLeft, liftAlternating_comp, LinearMap.comp_apply,
LinearMap.mulLeft_apply, hx]
