Skip to content

Commit

Permalink
feat(Algebra/TensorAlgebra): support towers of algebras (#6073)
Browse files Browse the repository at this point in the history
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`.
  • Loading branch information
eric-wieser authored and kim-em committed Aug 2, 2023
1 parent 2fdc335 commit fab8f45
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 7 deletions.
27 changes: 21 additions & 6 deletions Mathlib/Algebra/RingQuot.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down Expand Up @@ -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⟩

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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]
Expand All @@ -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
Expand All @@ -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) :=
Expand Down
28 changes: 27 additions & 1 deletion Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down

0 comments on commit fab8f45

Please sign in to comment.