Skip to content

Commit

Permalink
feat: add scalar tower instances for RingQuot and BilinForm (#6066)
Browse files Browse the repository at this point in the history
I tidied up some universe and type variables in the RingQuot file while I was here (in the first commit).
  • Loading branch information
eric-wieser authored and kim-em committed Aug 14, 2023
1 parent e62a4e3 commit c04c70e
Show file tree
Hide file tree
Showing 2 changed files with 44 additions and 20 deletions.
49 changes: 29 additions & 20 deletions Mathlib/Algebra/RingQuot.lean
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,14 @@ Since everything runs in parallel for quotients of `R`-algebras, we do that case
-/


universe u₁ u₂ u₃ u₄
universe uR uS uT uA

variable {R : Type u₁} [Semiring R]
variable {R : Type uR} [Semiring R]

variable {S : Type u₂} [CommSemiring S]
variable {S : Type uS} [CommSemiring S]
variable {T : Type uT}

variable {A : Type u₃} [Semiring A] [Algebra S A]
variable {A : Type uA} [Semiring A] [Algebra S A]

namespace RingCon

Expand Down Expand Up @@ -66,15 +67,15 @@ theorem Rel.add_right {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) : R
exact Rel.add_left h
#align ring_quot.rel.add_right RingQuot.Rel.add_right

theorem Rel.neg {R : Type u₁} [Ring R] {r : R → R → Prop} ⦃a b : R⦄ (h : Rel r a b) :
theorem Rel.neg {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b : R⦄ (h : Rel r a b) :
Rel r (-a) (-b) := by simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, Rel.mul_right h]
#align ring_quot.rel.neg RingQuot.Rel.neg

theorem Rel.sub_left {R : Type u₁} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r a b) :
theorem Rel.sub_left {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r a b) :
Rel r (a - c) (b - c) := by simp only [sub_eq_add_neg, h.add_left]
#align ring_quot.rel.sub_left RingQuot.Rel.sub_left

theorem Rel.sub_right {R : Type u₁} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) :
theorem Rel.sub_right {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r b c) :
Rel r (a - b) (a - c) := by simp only [sub_eq_add_neg, h.neg.add_right]
#align ring_quot.rel.sub_right RingQuot.Rel.sub_right

Expand Down Expand Up @@ -169,10 +170,10 @@ private irreducible_def add : RingQuot r → RingQuot r → RingQuot r
private irreducible_def mul : RingQuot r → RingQuot r → RingQuot r
| ⟨a⟩, ⟨b⟩ => ⟨Quot.map₂ (· * ·) Rel.mul_right Rel.mul_left a b⟩

private irreducible_def neg {R : Type u₁} [Ring R] (r : R → R → Prop) : RingQuot r → RingQuot r
private irreducible_def neg {R : Type uR} [Ring R] (r : R → R → Prop) : RingQuot r → RingQuot r
| ⟨a⟩ => ⟨Quot.map (fun a ↦ -a) Rel.neg a⟩

private irreducible_def sub {R : Type u₁} [Ring R] (r : R → R → Prop) :
private irreducible_def sub {R : Type uR} [Ring R] (r : R → R → Prop) :
RingQuot r → RingQuot r → RingQuot r
| ⟨a⟩, ⟨b⟩ => ⟨Quot.map₂ Sub.sub Rel.sub_right Rel.sub_left a b⟩

Expand Down Expand Up @@ -213,10 +214,10 @@ instance : Mul (RingQuot r) :=
instance : Pow (RingQuot r) ℕ :=
fun x n ↦ npow r n x⟩

instance {R : Type u₁} [Ring R] (r : R → R → Prop) : Neg (RingQuot r) :=
instance {R : Type uR} [Ring R] (r : R → R → Prop) : Neg (RingQuot r) :=
⟨neg r⟩

instance {R : Type u₁} [Ring R] (r : R → R → Prop) : Sub (RingQuot r) :=
instance {R : Type uR} [Ring R] (r : R → R → Prop) : Sub (RingQuot r) :=
⟨sub r⟩

instance [Algebra S R] : SMul S (RingQuot r) :=
Expand Down Expand Up @@ -247,14 +248,14 @@ theorem pow_quot {a} {n : ℕ} : (⟨Quot.mk _ a⟩ ^ n : RingQuot r) = ⟨Quot.
rw [npow_def]
#align ring_quot.pow_quot RingQuot.pow_quot

theorem neg_quot {R : Type u₁} [Ring R] (r : R → R → Prop) {a} :
theorem neg_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a} :
(-⟨Quot.mk _ a⟩ : RingQuot r) = ⟨Quot.mk _ (-a)⟩ := by
show neg r _ = _
rw [neg_def]
rfl
#align ring_quot.neg_quot RingQuot.neg_quot

theorem sub_quot {R : Type u₁} [Ring R] (r : R → R → Prop) {a b} :
theorem sub_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a b} :
(⟨Quot.mk _ a⟩ - ⟨Quot.mk _ b⟩ : RingQuot r) = ⟨Quot.mk _ (a - b)⟩ := by
show sub r _ _ = _
rw [sub_def]
Expand All @@ -268,6 +269,14 @@ theorem smul_quot [Algebra S R] {n : S} {a : R} :
rfl
#align ring_quot.smul_quot RingQuot.smul_quot

instance [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [IsScalarTower S T R] :
IsScalarTower S T (RingQuot r) :=
fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_assoc]⟩

instance [CommSemiring T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] :
SMulCommClass S T (RingQuot r) :=
fun s t ⟨a⟩ => Quot.inductionOn a <| fun a' => by simp only [RingQuot.smul_quot, smul_comm]⟩

instance instAddCommMonoid (r : R → R → Prop) : AddCommMonoid (RingQuot r) where
add := (· + ·)
zero := 0
Expand Down Expand Up @@ -337,7 +346,7 @@ instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r) where
__ := instAddCommMonoid r
__ := instMonoidWithZero r

instance instRing {R : Type u₁} [Ring R] (r : R → R → Prop) : Ring (RingQuot r) :=
instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot r) :=
{ RingQuot.instSemiring r with
neg := Neg.neg
add_left_neg := by
Expand All @@ -358,14 +367,14 @@ instance instRing {R : Type u₁} [Ring R] (r : R → R → Prop) : Ring (RingQu
rintro n ⟨⟨⟩⟩
simp [smul_quot, neg_quot, add_mul] }

instance instCommSemiring {R : Type u₁} [CommSemiring R] (r : R → R → Prop) :
instance instCommSemiring {R : Type uR} [CommSemiring R] (r : R → R → Prop) :
CommSemiring (RingQuot r) :=
{ RingQuot.instSemiring r with
mul_comm := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp [mul_quot, mul_comm] }

instance {R : Type u₁} [CommRing R] (r : R → R → Prop) : CommRing (RingQuot r) :=
instance {R : Type uR} [CommRing R] (r : R → R → Prop) : CommRing (RingQuot r) :=
{ RingQuot.instCommSemiring r, RingQuot.instRing r with }

instance (r : R → R → Prop) : Inhabited (RingQuot r) :=
Expand Down Expand Up @@ -406,14 +415,14 @@ theorem mkRingHom_surjective (r : R → R → Prop) : Function.Surjective (mkRin
#align ring_quot.mk_ring_hom_surjective RingQuot.mkRingHom_surjective

@[ext 1100]
theorem ringQuot_ext {T : Type u₄} [Semiring T] {r : R → R → Prop} (f g : RingQuot r →+* T)
theorem ringQuot_ext [Semiring T] {r : R → R → Prop} (f g : RingQuot r →+* T)
(w : f.comp (mkRingHom r) = g.comp (mkRingHom r)) : f = g := by
ext x
rcases mkRingHom_surjective r x with ⟨x, rfl⟩
exact (RingHom.congr_fun w x : _)
#align ring_quot.ring_quot_ext RingQuot.ringQuot_ext

variable {T : Type u₄} [Semiring T]
variable [Semiring T]

irreducible_def preLift {r : R → R → Prop} { f : R →+* T } (h : ∀ ⦃x y⦄, r x y → f x = f y) :
RingQuot r →+* T :=
Expand Down Expand Up @@ -482,7 +491,7 @@ agrees with the quotient by the appropriate ideal.
-/


variable {B : Type u₁} [CommRing B]
variable {B : Type uR} [CommRing B]

/-- The universal ring homomorphism from `RingQuot r` to `B ⧸ Ideal.ofRel r`. -/
def ringQuotToIdealQuotient (r : B → B → Prop) : RingQuot r →+* B ⧸ Ideal.ofRel r :=
Expand Down Expand Up @@ -564,7 +573,7 @@ theorem star'_quot (hr : ∀ a b, r a b → r (star a) (star b)) {a} :
#align ring_quot.star'_quot RingQuot.star'_quot

/-- Transfer a star_ring instance through a quotient, if the quotient is invariant to `star` -/
def starRing {R : Type u₁} [Semiring R] [StarRing R] (r : R → R → Prop)
def starRing {R : Type uR} [Semiring R] [StarRing R] (r : R → R → Prop)
(hr : ∀ a b, r a b → r (star a) (star b)) : StarRing (RingQuot r) where
star := star' r hr
star_involutive := by
Expand Down
15 changes: 15 additions & 0 deletions Mathlib/LinearAlgebra/BilinearForm.lean
Original file line number Diff line number Diff line change
Expand Up @@ -223,6 +223,21 @@ theorem smul_apply {α} [Monoid α] [DistribMulAction α R] [SMulCommClass α R
rfl
#align bilin_form.smul_apply BilinForm.smul_apply

instance {α β} [Monoid α] [Monoid β] [DistribMulAction α R] [DistribMulAction β R]
[SMulCommClass α R R] [SMulCommClass β R R] [SMulCommClass α β R] :
SMulCommClass α β (BilinForm R M) :=
fun a b B => ext $ fun x y => smul_comm a b (B x y)⟩

instance {α β} [Monoid α] [Monoid β] [SMul α β] [DistribMulAction α R] [DistribMulAction β R]
[SMulCommClass α R R] [SMulCommClass β R R] [IsScalarTower α β R] :
IsScalarTower α β (BilinForm R M) :=
fun a b B => ext $ fun x y => smul_assoc a b (B x y)⟩

instance {α} [Monoid α] [DistribMulAction α R] [DistribMulAction αᵐᵒᵖ R]
[SMulCommClass α R R] [IsCentralScalar α R] :
IsCentralScalar α (BilinForm R M) :=
fun a B => ext $ fun x y => op_smul_eq_smul a (B x y)⟩

instance : AddCommMonoid (BilinForm R M) :=
Function.Injective.addCommMonoid _ coe_injective coe_zero coe_add fun _ _ => coe_smul _ _

Expand Down

0 comments on commit c04c70e

Please sign in to comment.