feat(Algebra/TensorAlgebra): support towers of algebras (#6073)

This is pre-work towards a base-change of clifford algebras.

The main result here is
```lean
@[nolint unusedArguments]
instance instAlgebra {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A]
    [Algebra R A] [Module R M] [Module A M]
    [IsScalarTower R A M] :
    Algebra R (TensorAlgebra A M)
```
Note that strictly the `IsScalarTower R A M` argument isn't needed, but I'd claim the instance doesn't make any sense without it.

In order to prevent diamonds in the `algebraMap` fields of the `Int` and `Nat` algebra instances, we have stop having `natCast`  as an `irreducible_def`, and we have to add a missing `intCast` customization for `RingQuot`. In order to prevent diamonds in the `smul` fields there and elsewhere (such as a complex tensor algebra being a real algebra), we have to stop having the `smul` definition as an `irreducible_def`. We already had to make a similar refactor to prevent diamonds for `Algebra R (Polynomial A)`.

If we backport any of this to mathlib3, we'd additionally have to change the `smul` definition to not use pattern matching. Thankfully, structure eta in Lean 4 makes that unnecessary.

These diamonds are tested with inline `examples`.

Author: eric-wieser

Mathlib/Algebra/RingQuot.lean

@@ -155,7 +155,8 @@ namespace RingQuot
 
 variable (r : R → R → Prop)
 
-private irreducible_def natCast (n : ℕ) : RingQuot r :=
+-- can't be irreducible, causes diamonds in ℕ-algebras
+private def natCast (n : ℕ) : RingQuot r :=
   ⟨Quot.mk _ n⟩
 
 private irreducible_def zero : RingQuot r :=
@@ -196,9 +197,13 @@ private irreducible_def npow (n : ℕ) : RingQuot r → RingQuot r
             exact this)
         a⟩
 
-private irreducible_def smul [Algebra S R] (n : S) : RingQuot r → RingQuot r
+-- note: this cannot be irreducible, as otherwise diamonds don't commute.
+private def smul [Algebra S R] (n : S) : RingQuot r → RingQuot r
   | ⟨a⟩ => ⟨Quot.map (fun a ↦ n • a) (Rel.smul n) a⟩
 
+instance : NatCast (RingQuot r) :=
+  ⟨natCast r⟩
+
 instance : Zero (RingQuot r) :=
   ⟨zero r⟩
 
@@ -265,7 +270,7 @@ theorem sub_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a b} :
 theorem smul_quot [Algebra S R] {n : S} {a : R} :
     (n • ⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (n • a)⟩ := by
   show smul r _ _ = _
-  rw [smul_def]
+  rw [smul]
   rfl
 #align ring_quot.smul_quot RingQuot.smul_quot
 
@@ -327,8 +332,8 @@ instance instMonoidWithZero (r : R → R → Prop) : MonoidWithZero (RingQuot r)
 
 instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r) where
   natCast := natCast r
-  natCast_zero := by simp [Nat.cast, natCast_def, ← zero_quot]
-  natCast_succ := by simp [Nat.cast, natCast_def, ← one_quot, add_quot]
+  natCast_zero := by simp [Nat.cast, natCast, ← zero_quot]
+  natCast_succ := by simp [Nat.cast, natCast, ← one_quot, add_quot]
   left_distrib := by
     rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
     simp only [mul_quot, add_quot, left_distrib]
@@ -346,6 +351,10 @@ instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r) where
   __ := instAddCommMonoid r
   __ := instMonoidWithZero r
 
+-- can't be irreducible, causes diamonds in ℤ-algebras
+private def intCast {R : Type uR} [Ring R] (r : R → R → Prop) (z : ℤ) : RingQuot r :=
+  ⟨Quot.mk _ z⟩
+
 instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot r) :=
   { RingQuot.instSemiring r with
     neg := Neg.neg
@@ -365,7 +374,13 @@ instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot
       simp [smul_quot, add_quot, add_mul, add_comm]
     zsmul_neg' := by
       rintro n ⟨⟨⟩⟩
-      simp [smul_quot, neg_quot, add_mul] }
+      simp [smul_quot, neg_quot, add_mul]
+    intCast := intCast r
+    intCast_ofNat := fun n => congrArg RingQuot.mk <| by
+      exact congrArg (Quot.mk _) (Int.cast_ofNat _)
+    intCast_negSucc := fun n => congrArg RingQuot.mk <| by
+      simp_rw [neg_def]
+      exact congrArg (Quot.mk _) (Int.cast_negSucc n) }
 
 instance instCommSemiring {R : Type uR} [CommSemiring R] (r : R → R → Prop) :
   CommSemiring (RingQuot r) :=

Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

@@ -67,13 +67,39 @@ def TensorAlgebra :=
 -- Porting note: Expanded `deriving Inhabited, Semiring, Algebra`
 instance : Inhabited (TensorAlgebra R M) := RingQuot.instInhabitedRingQuot _
 instance : Semiring (TensorAlgebra R M) := RingQuot.instSemiring _
-instance : Algebra R (TensorAlgebra R M) := RingQuot.instAlgebraRingQuotInstSemiring _
+
+-- `IsScalarTower` is not needed, but the instance isn't really canonical without it.
+@[nolint unusedArguments]
+instance instAlgebra {R A M} [CommSemiring R] [AddCommMonoid M] [CommSemiring A]
+    [Algebra R A] [Module R M] [Module A M]
+    [IsScalarTower R A M] :
+    Algebra R (TensorAlgebra A M) :=
+  RingQuot.instAlgebraRingQuotInstSemiring _
+
+-- verify there is no diamond
+example : (algebraNat : Algebra ℕ (TensorAlgebra R M)) = instAlgebra := rfl
+
+instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
+    [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
+    [IsScalarTower R A M] [IsScalarTower S A M] [SMulCommClass R S A] :
+    SMulCommClass R S (TensorAlgebra A M) :=
+  RingQuot.instSMulCommClassRingQuotInstSMulRingQuotInstSMulRingQuot _
+
+instance {R S A M} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] [CommSemiring A]
+    [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M]
+    [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S A] :
+    IsScalarTower R S (TensorAlgebra A M) :=
+  RingQuot.instIsScalarTowerRingQuotInstSMulRingQuotInstSMulRingQuot _
 
 namespace TensorAlgebra
 
 instance {S : Type _} [CommRing S] [Module S M] : Ring (TensorAlgebra S M) :=
   RingQuot.instRing (Rel S M)
 
+-- verify there is no diamond
+variable (S M : Type) [CommRing S] [AddCommGroup M] [Module S M] in
+example : (algebraInt _ : Algebra ℤ (TensorAlgebra S M)) = instAlgebra := rfl
+
 variable {M}
 
 /-- The canonical linear map `M →ₗ[R] TensorAlgebra R M`.