feat(LinearAlgebra/TensorAlgebra/Basis): the free and tensor algebras…

… are free modules (#6680)

The main result here is `Basis.tensorAlgebra (b : Basis κ R M) : Basis (FreeMonoid κ) R (TensorAlgebra R M)` from which everything else follows without much work.

Mathlib.lean

@@ -2271,6 +2271,7 @@ import Mathlib.LinearAlgebra.Span
 import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.LinearAlgebra.SymplecticGroup
 import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+import Mathlib.LinearAlgebra.TensorAlgebra.Basis
 import Mathlib.LinearAlgebra.TensorAlgebra.Grading
 import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
 import Mathlib.LinearAlgebra.TensorPower

Mathlib/LinearAlgebra/FreeAlgebra.lean

@@ -7,6 +7,7 @@ import Mathlib.LinearAlgebra.Basis
 import Mathlib.Algebra.FreeAlgebra
 import Mathlib.LinearAlgebra.Dimension
 import Mathlib.LinearAlgebra.FinsuppVectorSpace
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 #align_import linear_algebra.free_algebra from "leanprover-community/mathlib"@"039a089d2a4b93c761b234f3e5f5aeb752bac60f"
 
@@ -22,21 +23,28 @@ universe u v
 
 namespace FreeAlgebra
 
+variable (R : Type u) (X : Type v)
+
+section
+variable [CommSemiring R]
+
 /-- The `FreeMonoid X` basis on the `FreeAlgebra R X`,
 mapping `[x₁, x₂, ..., xₙ]` to the "monomial" `1 • x₁ * x₂ * ⋯ * xₙ` -/
 -- @[simps]
-noncomputable def basisFreeMonoid (R : Type u) (X : Type v) [CommRing R] :
-    Basis (FreeMonoid X) R (FreeAlgebra R X) :=
+noncomputable def basisFreeMonoid : Basis (FreeMonoid X) R (FreeAlgebra R X) :=
   Finsupp.basisSingleOne.map (equivMonoidAlgebraFreeMonoid (R := R) (X := X)).symm.toLinearEquiv
 #align free_algebra.basis_free_monoid FreeAlgebra.basisFreeMonoid
 
--- TODO: generalize to `X : Type v`
-theorem rank_eq {K : Type u} {X : Type max u v} [Field K] :
-    Module.rank K (FreeAlgebra K X) = Cardinal.mk (List X) :=
-  -- Porting note: the type class inference was no longer automatic.
-  -- was: (Cardinal.lift_inj.mp (basisFreeMonoid K X).mk_eq_rank).symm
-  Cardinal.lift_inj.mp (@Basis.mk_eq_rank _ _ _ _ _ _ (inferInstance : Module K (FreeAlgebra K X))
-  (basisFreeMonoid K X)).symm
+instance : Module.Free R (FreeAlgebra R X) :=
+  have : Module.Free R (MonoidAlgebra R (FreeMonoid X)) := Module.Free.finsupp _ _ _
+  Module.Free.of_equiv (equivMonoidAlgebraFreeMonoid (R := R) (X := X)).symm.toLinearEquiv
+
+end
+
+theorem rank_eq [CommRing R] [Nontrivial R] :
+    Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u} (Cardinal.mk (List X)) := by
+  rw [←(Basis.mk_eq_rank'.{_,_,_,u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
+    Cardinal.lift_umax'.{v,u}, FreeMonoid]
 #align free_algebra.rank_eq FreeAlgebra.rank_eq
 
 end FreeAlgebra

Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+import Mathlib.LinearAlgebra.FreeModule.Basic
+import Mathlib.LinearAlgebra.FreeModule.Rank
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
+import Mathlib.LinearAlgebra.FreeAlgebra
+
+/-!
+# A basis for `TensorAlgebra R M`
+
+## Main definitions
+
+* `TensorAlgebra.equivMonoidAlgebra b : TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ`:
+  the isomorphism given by a basis `b : Basis κ R M`.
+* `Basis.tensorAlgebra b : Basis (FreeMonoid κ) R (TensorAlgebra R M)`:
+  the basis on the tensor algebra given by a basis `b : Basis κ R M`.
+
+## Main results
+
+* `TensorAlgebra.instFreeModule`: the tensor algebra over `M` is free when `M` is
+* `TensorAlgebra.rank_eq`
+
+-/
+namespace TensorAlgebra
+
+open scoped BigOperators
+
+universe uκ uR uM
+variable {κ : Type uκ} {R : Type uR} {M : Type uM}
+
+section CommSemiring
+variable [CommSemiring R] [AddCommMonoid M] [Module R M]
+
+/-- A basis provides an algebra isomorphism with the free algebra, replacing each basis vector
+with its index. -/
+noncomputable def equivFreeAlgebra (b : Basis κ R M) :
+    TensorAlgebra R M ≃ₐ[R] FreeAlgebra R κ :=
+  AlgEquiv.ofAlgHom
+    (TensorAlgebra.lift _ (Finsupp.total _ _ _ (FreeAlgebra.ι _) ∘ₗ b.repr.toLinearMap))
+    (FreeAlgebra.lift _ (ι R ∘ b))
+    (by ext; simp)
+    (hom_ext <| b.ext <| fun i => by simp)
+
+@[simp]
+lemma equivFreeAlgebra_ι_apply (b : Basis κ R M) (i : κ) :
+    equivFreeAlgebra b (ι R (b i)) = FreeAlgebra.ι R i :=
+  (TensorAlgebra.lift_ι_apply _ _).trans <| by simp
+
+@[simp]
+lemma equivFreeAlgebra_symm_ι (b : Basis κ R M) (i : κ) :
+    (equivFreeAlgebra b).symm (FreeAlgebra.ι R i) = ι R (b i) :=
+  (equivFreeAlgebra b).toEquiv.symm_apply_eq.mpr <| equivFreeAlgebra_ι_apply b i |>.symm
+
+/-- A basis on `M` can be lifted to a basis on `TensorAlgebra R M` -/
+@[simps! repr_apply]
+noncomputable def _root_.Basis.tensorAlgebra (b : Basis κ R M) :
+    Basis (FreeMonoid κ) R (TensorAlgebra R M) :=
+  (FreeAlgebra.basisFreeMonoid R κ).map <| (equivFreeAlgebra b).symm.toLinearEquiv
+
+/-- `TensorAlgebra R M` is free when `M` is. -/
+instance instModuleFree [Module.Free R M] : Module.Free R (TensorAlgebra R M) :=
+  let ⟨⟨_κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
+  .of_basis b.tensorAlgebra
+
+end CommSemiring
+
+section CommRing
+variable [CommRing R] [AddCommGroup M] [Module R M]
+
+local infixr:80 " ^ℕ " => @HPow.hPow Cardinal ℕ Cardinal _
+
+attribute [pp_with_univ] Cardinal.lift
+
+open Cardinal in
+lemma rank_eq [Nontrivial R] [Module.Free R M] :
+    Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR} (sum fun n ↦ Module.rank R M ^ℕ n) := by
+  let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
+  rw [(equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, mk_list_eq_sum_pow,
+    Basis.mk_eq_rank'' b]
+
+end CommRing
+
+end TensorAlgebra