Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(Algebra/TensorAlgebra): support towers of algebras #6073

Closed
wants to merge 17 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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 _
ocfnash marked this conversation as resolved.
Show resolved Hide resolved

-- 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
Loading