English
The lift of the canonical embedding into the graded structure agrees with DirectSum.of on the graded components, i.e., the lifting map evaluated on x' equals the componentwise embedding.
Русский
Подъём канонического вложения в градуированную структуру совпадает с прямой суммой; отображение на компоненте даёт тот же результат.
LaTeX
$$lift_Q ⟨GradedAlgebra.ι Q, ι_sq_scalar Q⟩ x' = DirectSum.of(…) i' x'$$
Lean4
theorem lift_ι_eq (i' : ZMod 2) (x' : evenOdd Q i') :
lift Q ⟨GradedAlgebra.ι Q, GradedAlgebra.ι_sq_scalar Q⟩ x' = DirectSum.of (fun i => evenOdd Q i) i' x' :=
by
obtain ⟨x', hx'⟩ := x'
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
induction hx' using Submodule.iSup_induction' with
| mem i x hx =>
obtain ⟨i, rfl⟩ := i
dsimp only [Subtype.coe_mk] at hx
induction hx using Submodule.pow_induction_on_left' with
| algebraMap r => rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| add x y i hx hy ihx ihy =>
rw [map_add, ihx, ihy, ← AddMonoidHom.map_add]
rfl
| mem_mul m hm i x hx ih =>
obtain ⟨_, rfl⟩ := hm
rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
refine DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext ?_ ?_) <;>
dsimp only [GradedMonoid.mk, Subtype.coe_mk]
· rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
rfl
| zero =>
rw [map_zero]
apply Eq.symm
apply DFinsupp.single_eq_zero.mpr; rfl
| add x y hx hy ihx ihy => rw [map_add, ihx, ihy, ← AddMonoidHom.map_add]; rfl
