feat: port LinearAlgebra.TensorAlgebra.Grading (#4803)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>

Mathlib.lean

@@ -1951,6 +1951,7 @@ import Mathlib.LinearAlgebra.Span
 import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.LinearAlgebra.SymplecticGroup
 import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+import Mathlib.LinearAlgebra.TensorAlgebra.Grading
 import Mathlib.LinearAlgebra.TensorPower
 import Mathlib.LinearAlgebra.TensorProduct
 import Mathlib.LinearAlgebra.TensorProduct.Matrix

Mathlib/Algebra/Algebra/Operations.lean

@@ -438,7 +438,8 @@ protected theorem pow_induction_on_left' {C : ∀ (n : ℕ) (x), x ∈ M ^ n →
     (hr : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
     (hadd : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
     (hmul : ∀ m (hm : m ∈ M), ∀ (i x hx), C i x hx → C i.succ (m * x) (mul_mem_mul hm hx))
-    {x : A} {n : ℕ}
+    -- porting note: swapped argument order to match order of `C`
+    {n : ℕ} {x : A}
     (hx : x ∈ M ^ n) : C n x hx := by
   induction' n with n n_ih generalizing x
   · rw [pow_zero] at hx
@@ -457,7 +458,8 @@ protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n 
     (hmul :
       ∀ i x hx, C i x hx →
         ∀ m (hm : m ∈ M), C i.succ (x * m) ((pow_succ' M i).symm ▸ mul_mem_mul hx hm))
-    {x : A} {n : ℕ} (hx : x ∈ M ^ n) : C n x hx := by
+    -- porting note: swapped argument order to match order of `C`
+    {n : ℕ} {x : A} (hx : x ∈ M ^ n) : C n x hx := by
   induction' n with n n_ih generalizing x
   · rw [pow_zero] at hx
     obtain ⟨r, rfl⟩ := hx

Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module linear_algebra.tensor_algebra.grading
+! leanprover-community/mathlib commit 2a7ceb0e411e459553a303d48eecdbb8553bd7ed
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+import Mathlib.RingTheory.GradedAlgebra.Basic
+
+/-!
+# Results about the grading structure of the tensor algebra
+
+The main result is `TensorAlgebra.gradedAlgebra`, which says that the tensor algebra is a
+ℕ-graded algebra.
+-/
+
+
+namespace TensorAlgebra
+
+variable {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M]
+
+open scoped DirectSum
+
+variable (R M)
+
+/-- A version of `TensorAlgebra.ι` that maps directly into the graded structure. This is
+primarily an auxiliary construction used to provide `TensorAlgebra.gradedAlgebra`. -/
+nonrec def GradedAlgebra.ι : M →ₗ[R] ⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[_] _) ^ i) :=
+  DirectSum.lof R ℕ (fun i => ↥(LinearMap.range (ι R : M →ₗ[_] _) ^ i)) 1 ∘ₗ
+    (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m
+#align tensor_algebra.graded_algebra.ι TensorAlgebra.GradedAlgebra.ι
+
+theorem GradedAlgebra.ι_apply (m : M) :
+    GradedAlgebra.ι R M m =
+      DirectSum.of (fun (i : ℕ) => ↥(LinearMap.range (TensorAlgebra.ι R : M →ₗ[_] _) ^ i)) 1
+        ⟨TensorAlgebra.ι R m, by simpa only [pow_one] using LinearMap.mem_range_self _ m⟩ :=
+  rfl
+#align tensor_algebra.graded_algebra.ι_apply TensorAlgebra.GradedAlgebra.ι_apply
+
+variable {R M}
+
+/-- 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
+    cases' x with x hx
+    dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
+    -- porting note: use new `induction using` support that failed in Lean 3
+    induction hx using Submodule.pow_induction_on_left' with
+    | hr r =>
+      rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
+    | hadd x y i hx hy ihx ihy =>
+      rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
+    | hmul m hm i x hx ih =>
+      obtain ⟨_, rfl⟩ := hm
+      rw [AlgHom.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)
+#align tensor_algebra.graded_algebra TensorAlgebra.gradedAlgebra
+
+end TensorAlgebra