From fab8f45047e2d19339981ae81f2d21d2d20105bc Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 07:03:11 +0000 Subject: [PATCH] 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`. --- Mathlib/Algebra/RingQuot.lean | 27 ++++++++++++++---- .../LinearAlgebra/TensorAlgebra/Basic.lean | 28 ++++++++++++++++++- 2 files changed, 48 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean index 79bd63c7b5348..4faabdc1908a1 100644 --- a/Mathlib/Algebra/RingQuot.lean +++ b/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) := diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean index d182454434916..afdaa2c0c75df 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean +++ b/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`.