English
On a homogeneous element x ∈ ∧^i_R M, liftι maps x to the direct-sum embedding in the i-th component: liftι(R,M)x = DirectSum.of (fun k => ∧^k_R M) k x.
Русский
На однородном элементе x ∈ ∧^i_R M liftι переводит x в соответствующую i-ю компоненту прямой суммы.
LaTeX
$$$\text{liftι}(R,M)x = \text{DirectSum}.of(\lambda k. \bigwedge^k_R M)\, i\, x$$$
Lean4
theorem liftι_eq (i : ℕ) (x : ⋀[R]^i M) : GradedAlgebra.liftι R M x = DirectSum.of (fun i => ⋀[R]^i M) i x :=
by
obtain ⟨x, hx⟩ := x
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
induction hx using Submodule.pow_induction_on_left' with
| algebraMap => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| add _ _ _ _ _ ihx ihy => simp_rw [map_add, ihx, ihy, ← AddMonoidHom.map_add]; rfl
| mem_mul _ hm _ _ _ ih =>
obtain ⟨_, rfl⟩ := hm
simp_rw [map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
