English
Let gradeBy define a grading of the monoid algebra by ι. For any i and any x in gradeBy(R, f, i), the auxiliary decomposition map sends x to the i-th direct summand; i.e., decomposeAux(f)(↑x) corresponds to the canonical inclusion into the i-th component.
Русский
Пусть градация gradeBy определяет градацию моноидовой алгебры по индексу ι. Для любого i и элемента x ∈ gradeBy(R, f, i) отображение decomposeAux(f) отправляет x в i-й прямой сумме; тождество показывает каноническое включение в i-ю компоненту.
LaTeX
$$$\decomposeAux f \uparrow x = DirectSum.of\bigl(\lambda i. \mathrm{gradeBy}(R,f,i)\bigr)\, i\, x$$$
Lean4
theorem decomposeAux_coe {i : ι} (x : gradeBy R f i) : decomposeAux f ↑x = DirectSum.of (fun i => gradeBy R f i) i x :=
by
classical
obtain ⟨x, hx⟩ := x
revert hx
refine Finsupp.induction x ?_ ?_
· intro hx
symm
exact AddMonoidHom.map_zero _
· intro m b y hmy hb ih hmby
have : Disjoint (Finsupp.single m b).support y.support := by
simpa only [Finsupp.support_single_ne_zero _ hb, Finset.disjoint_singleton_left]
rw [mem_gradeBy_iff, Finsupp.support_add_eq this, Finset.coe_union, Set.union_subset_iff] at hmby
obtain ⟨h1, h2⟩ := hmby
have : f m = i := by rwa [Finsupp.support_single_ne_zero _ hb, Finset.coe_singleton, Set.singleton_subset_iff] at h1
subst this
simp only [map_add, decomposeAux_single f m]
let ih' := ih h2
dsimp at ih'
rw [ih', ← AddMonoidHom.map_add]
apply DirectSum.of_eq_of_gradedMonoid_eq
congr 2
