English
TensorAlgebra is graded by the powers of the submodule range(ι_R).
Русский
TensorAlgebra считается градуированной по степеням подмодуля образа ι_R.
LaTeX
$$$ \text{ gradedAlgebra : GradedAlgebra} \bigl( (\operatorname{range} (\iota R))^{\cdot} \bigr) $$$
Lean4
/-- The tensor algebra is graded by the powers of the submodule `(TensorAlgebra.ι R).range`. -/
instance gradedAlgebra : GradedAlgebra ((LinearMap.range (ι R : M →ₗ[R] TensorAlgebra R M) ^ ·) : ℕ → Submodule R _) :=
GradedAlgebra.ofAlgHom _ (lift R <| GradedAlgebra.ι R M)
(by
ext m
dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply, AlgHom.id_apply]
rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk])
fun 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 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 R M, DirectSum.of_mul_of]
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
