ring structure on algebra localization

Stream: mathlib4

[Kevin Buzzard]

Let $R$ be a commutative ring and let $A$ be an $R$-module. If $S$ is a submonoid of $R$ then $A[S^{-1}]$ is a module over $R[S^{-1}]$, and multiplication on $R[S^{-1}]$ is defined via this module structure if $A=R$. We have all this in mathlib, in files like RingTheory.OreLocalization.Basic and RingTheory.OreLocalization.Ring.

Now say $A$ is in fact a commutative $R$-algebra. Then $A[S^{-1}]$ is, I think, naturally an $R[S^{-1}]$-algebra but first things first, I want to make $A[S^{-1}]$ into a ring or even a monoid. To do this I have to define a multiplication on $A[S^{-1}]$. But my attempt, trying to mimic the code here, causes a diamond.

import Mathlib.RingTheory.OreLocalization.Ring

namespace OreLocalization

variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] {S : Submonoid R}

-- already a thing
#check (OreLocalization.smul : R[S⁻¹] → A[S⁻¹] → A[S⁻¹])

-- the def of `smul` comes from lifting this:
/-
private def smul' (r₁ : R) (s₁ : S) (r₂ : A) (s₂ : S) : A[S⁻¹] :=
  oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)
-/

-- attempt to copy the `smul'`, `smul''`, `smul` pattern in RingTheory.OreLocalization.Basic
private def mul' (a₁ : A) (s₁ : S) (a₂ : A) (s₂ : S) : A[S⁻¹] :=
  a₁ * a₂ /ₒ (s₂ * s₁) -- no `oreDenom` available for `A` as `S` is a submonoid of `R` not `A`,
  -- but everything is commutative so just use `oreNum a s = a` and `oreDenom a s = s` and hope

private def mul'' (a : A) (s : S) : A[S⁻¹] → A[S⁻¹] :=
  liftExpand (mul' a s) fun a₁ a₂ s' hs => by
  -- didn't check proof
  sorry

protected def mul : A[S⁻¹] → A[S⁻¹] → A[S⁻¹] :=
  liftExpand mul'' fun a₁ a₂ s hs => by
  -- didn't check proof
  sorry

-- looks like I made a diamond anyway in the case A=R
example (as bt : R[S⁻¹]) : as.mul bt = as * bt := rfl -- fails

Any advice @Andrew Yang or anyone else?

[Kevin Buzzard]

Oh, they're equal, the proof just isn't rfl:

example (as bt : R[S⁻¹]) : as.mul bt = as * bt := by
  unfold OreLocalization.mul HMul.hMul instHMul Mul.mul instMul OreLocalization.smul
  congr

But I think I need it to be rfl in order to make this viable.

To un-#xy: Bourbaki says "we need to check a property of this big commutative diagram of R-algebras but WLOG P is maximal because just localize the entire diagram at R - P and this doesn't change anything relevant".

[Eric Wieser]

Why does congr work there?

[Kevin Buzzard]

Answer: because rfl works.

example (as bt : R[S⁻¹]) : as.mul bt = as * bt := by
  -- rfl -- fails
  unfold OreLocalization.mul HMul.hMul instHMul Mul.mul instMul OreLocalization.smul
  rfl -- works

So now I'm even more confused but at least we're making progress :-)

[Kevin Buzzard]

:lightbulb: I guess it's because OreLocalization.smul is tagged irreducible.

/-- The scalar multiplication on the Ore localization of monoids. -/
@[to_additive (attr := irreducible)
  "the vector addition on the Ore localization of additive monoids."]
protected def smul : R[S⁻¹] → X[S⁻¹] → X[S⁻¹] :=

[Kevin Buzzard]

mathlib compiles with (attr := irreducible) removed.

[Eric Wieser]

Yep, smul should never be irreducible because this causes diamonds. We had this long ago with Polynomial.

[Christian Merten]

Do I understand you correctly that you don't want to use docs#Localization (or docs#IsLocalization)?

[Christian Merten]

(or rather some abstract (Aₚ : Type) [CommRing Aₚ] [Algebra R Aₚ] [IsLocalization M Aₚ])

[Kevin Buzzard]

I need a concrete localization. I have a theorem which applies to maximal ideals and I have a ring R and a prime ideal and I want to say "apply the theorem to R_P where P is now maximal".

The reason I'm doing this Ore stuff was that I was reacting to the following error:

import Mathlib

variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] {S : Submonoid R}


abbrev SR := R[S⁻¹]
abbrev SA := A[S⁻¹]

instance : Algebra (R[S⁻¹]) (A[S⁻¹]) where
/-
error:
failed to synthesize
  Semiring (OreLocalization S A)
-/

Just to be clear -- I only care about the commutative case for the application.

[Eric Wieser]

Do you get in trouble here with diamonds if A = R[S\inv]?

[Eric Wieser]

Or is that instantiation nonsense?

[Kevin Buzzard]

That instantiation definitely isn't nonsense, it's definitely worth checking that there are no problems in this case.

[Eric Wieser]

If it's not nonsense, then I'm pretty sure this gives the same diamond as it would for polynomials

[Christian Merten]

I think the usual spelling would be

import Mathlib

variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] {S : Submonoid R}

#synth CommRing (Localization (S.map (algebraMap R A)))

but I am surprised that

#synth Algebra (Localization S) (Localization (S.map (algebraMap R A)))

does not work.

[Christian Merten]

Also not with Algebra.algebraMapSubmonoid A S instead of S.map (algebraMap R A). This works, but might cause issues:

noncomputable instance : Algebra (Localization S) (Localization (Algebra.algebraMapSubmonoid A S)) :=
  RingHom.toAlgebra <| IsLocalization.map (T := Algebra.algebraMapSubmonoid A S) _ (algebraMap R A) <|
    Submonoid.le_comap_map S

[Kevin Buzzard]

I really don't want to get involved with S.map. I have a diagram of 6 commutative rings and if I localise them at 6 different places I think I'll be in for a lot of pain. This way I'm localising them all at the same place. I don't know for sure if my way is better but I think it's worth experimenting with. But now I seem to have a diamond and I don't know why. Two semiring instances which are defeq on + and * are not defeq. Could they differ defeqly at 0 or 1? How does one go from a goal of "these two explicit semiring instances are equal" to "they were constructed from the same fields"?

import Mathlib.RingTheory.OreLocalization.Ring
import Mathlib -- just in case, when developing

/-!

# Algebra instances of Ore Localizations

If `R` is a commutative ring with submonoid `S`, and if `A` is a commutative `R`-algebra,
then my guess is that `A[S⁻¹]` is an `R[S⁻¹]`-algebra. Let's see if I'm right and if so,
in what generality.

-/

namespace OreLocalization

section CommMagma

variable {R A : Type*} [CommMonoid R] [CommMagma A] [MulAction R A] [IsScalarTower R A A]
  {S : Submonoid R}

@[to_additive]
private def mul' (a₁ : A) (s₁ : S) (a₂ : A) (s₂ : S) : A[S⁻¹] :=
  a₁ * a₂ /ₒ (s₂ * s₁)

@[to_additive]
private def mul''
  (a : A) (s : S) : A[S⁻¹] → A[S⁻¹] :=
  liftExpand (mul' a s) fun a₁ r₁ ⟨s₁, hs₁⟩ hr₁s₁ => by
  unfold OreLocalization.mul'
  simp only at hr₁s₁ ⊢
  rw [oreDiv_eq_iff]
  use ⟨s₁, hs₁⟩, r₁ * s₁
  simp only [Submonoid.mk_smul, Submonoid.coe_mul]
  constructor
  · rw [← smul_mul_assoc]
    rw [← smul_mul_assoc]
    rw [mul_comm]
    rw [smul_mul_assoc, smul_mul_assoc]
    rw [mul_comm]
    -- it's like a bloody Rubik's cube
    rw [smul_mul_assoc]
    rw [← mul_smul]
  · obtain ⟨s₂, hs₂⟩ := s
    simpa only [Submonoid.mk_smul, Submonoid.coe_mul] using mul_left_comm s₁ (r₁ * s₁) s₂

@[to_additive]
protected def mul : A[S⁻¹] → A[S⁻¹] → A[S⁻¹] :=
  liftExpand mul'' fun a₁ r₁ s hs => by
  obtain ⟨s₁, hs₁⟩ := s
  simp only at hs
  unfold OreLocalization.mul''
  simp
  unfold OreLocalization.mul'
  dsimp
  ext sa
  induction sa
  rename_i a s_temp
  obtain ⟨s, hs⟩ := s_temp
  rw [liftExpand_of]
  rw [liftExpand_of]
  rw [oreDiv_eq_iff]
  simp only [Submonoid.mk_smul, Submonoid.coe_mul]
  use ⟨s₁, hs₁⟩, r₁ * s₁
  simp only [Submonoid.mk_smul, Submonoid.coe_mul]
  constructor
  · rw [smul_mul_assoc]
    rw [← mul_smul]
    rw [mul_comm]
  · repeat rw [mul_assoc]
    repeat rw [mul_left_comm s₁]
    rw [mul_left_comm s]

instance : Mul (A[S⁻¹]) where
  mul := OreLocalization.mul

protected def mul_def (a : A) (s : { x // x ∈ S }) (b : A) (t : { x // x ∈ S }) :
  a /ₒ s * (b /ₒ t) = a * b /ₒ (t * s) := rfl

-- no diamond
example (as bt : R[S⁻¹]) : as * bt = as • bt := rfl

end CommMagma

section One

variable {R A : Type*} [CommMonoid R] [MulAction R A] [One A] {S : Submonoid R}

instance : One (A[S⁻¹]) where
  one := 1 /ₒ 1

protected theorem one_def' : (1 : A[S⁻¹]) = 1 /ₒ 1 := rfl

end One

section CommMonoid

variable {R A : Type*} [CommMonoid R] [CommMonoid A] [MulAction R A] [IsScalarTower R A A]
  {S : Submonoid R}

instance commMonoid : CommMonoid (A[S⁻¹]) where
  mul_assoc a b c := by
    induction' a with a
    induction' b with b
    induction' c with c
    change (a * b * c) /ₒ _ = (a * (b * c)) /ₒ _
    simp [mul_assoc]
  one_mul a := by
    induction' a with a
    change (1 * a) /ₒ _ = a /ₒ _
    simp
  mul_one a := by
    induction' a with a s
    simp [OreLocalization.mul_def, OreLocalization.one_def']
  mul_comm a b := by
    induction' a with a
    induction' b with b
    simp only [OreLocalization.mul_def, mul_comm]

end CommMonoid

section CommSemiring

variable {R A : Type*} [CommMonoid R] [CommSemiring A] [DistribMulAction R A] [IsScalarTower R A A]
  {S : Submonoid R}

theorem left_distrib' (a b c : A[S⁻¹]) :
    a * (b + c) = a * b + a * c := by
  induction' a with a r
  induction' b with b s
  induction' c with c t
  rcases oreDivAddChar' b c s t with ⟨r₁, s₁, h₁, q⟩; rw [q]; clear q
  simp only [OreLocalization.mul_def]
  rcases oreDivAddChar' (a * b) (a * c) (s * r) (t * r) with ⟨r₂, s₂, h₂, q⟩; rw [q]; clear q
  rw [oreDiv_eq_iff]
  obtain ⟨r, hr⟩ := r
  obtain ⟨s, hs⟩ := s
  obtain ⟨t, ht⟩ := t
  obtain ⟨s₁, hs₁⟩ := s₁
  obtain ⟨s₂, hs₂⟩ := s₂
  simp only [Submonoid.mk_smul, Submonoid.coe_mul] at h₁ h₂ ⊢
  sorry
  --use ⟨?_, ?_⟩, ?_
  --constructor
  --· simp
  --  sorry
  --· sorry

instance instCommSemiring' : CommSemiring A[S⁻¹] where
  __ := commMonoid
  left_distrib := left_distrib'
  right_distrib a b c := by
    rw [mul_comm, mul_comm a, mul_comm b, left_distrib']
  zero_mul a := by
    induction' a with a s
    rw [OreLocalization.zero_def, OreLocalization.mul_def]
    simp
  mul_zero a := by
    induction' a with a s
    rw [OreLocalization.zero_def, OreLocalization.mul_def]
    simp

end CommSemiring

section the_problem

variable {R A : Type*} [CommSemiring R] {S : Submonoid R}

example : (instCommSemiring : CommSemiring R[S⁻¹]) = (instCommSemiring' : CommSemiring R[S⁻¹]) := by --rfl #exit -- fails

  ext
  · -- additions coincide
    rfl
  · -- multiplications coincide
    rfl

end the_problem

[Kevin Buzzard]

Eric Wieser said:

If it's not nonsense, then I'm pretty sure this gives the same diamond as it would for polynomials

@Eric Wieser can you clarify what the problem is? Is it different to the problem I expose above?

[Kevin Buzzard]

Finally, should I PR the removal of irreducible from smul separately as a one-line PR?

[Matthew Ballard]

with_unfolding_all rfl solves your problem so probably more irreducible

[Matthew Ballard]

Is there a better design of these SMul instances where

1. We block reduction to the quotient still
2. We can still compare pullbacks of SMul actions

[Yaël Dillies]

Kevin Buzzard said:

Eric Wieser said:

If it's not nonsense, then I'm pretty sure this gives the same diamond as it would for polynomials

Eric Wieser can you clarify what the problem is? Is it different to the problem I expose above?

It's the classic problem of deciding whether ι → α acts on ι → ι → α by

• the action of ι → α on ι → α coming from the action of α on α
• or the action of α on ι → α coming from the action of α on α

[Yaël Dillies]

The first gives you (f • g) i j = (f • g i) j = f j • g i j while the second gives you (f • g) i j = (f i • g i) j = f i • g i j.

[Eric Wieser]

That particular example happens to have featured (with a diagram) in a thesis Kevin read, but I don't know enough about localizations to know if in this case things happen to end up propeq

[Kevin Buzzard]

I'm still trying to understand what polynomials, functions etc have to do with all this.

I want to go from Algebra R A to Algebra R[1/S] A[1/S] and apparently the issue is when A=R[1/S]. Trying to follow the logic here, we certainly have Algebra R (R[1/S]) but I don't know if we have any instance of Algebra A (A[1/S])in mathlib if S : Submonoid R and Algebra R A. However I guess it would not be unreasonable to make one and indeed that would make a diamond (which is almost certainly propeq, at least in the commutative case).

On the other hand I definitely want these instances in a situation when A can't be R[1/S]. So is the idea that I should make them defs and then just fire them up when I need them? I've recently run into another such situation -- I want D tensor[R] A to be an A-algebra but I think that we only have A tensor[R] D being an A-algebra, and if D tensor A is too, then A tensor A now has two (non-propeq) A-algebra structures. I propose getting around this by just making my instance a def, and promoting it to an instance locally. Does this sound OK?

[Johan Commelin]

It sounds ok. But I'm not sure I can see through all the ramifications

[Eric Wieser]

Making things (reducible) defs instead of instances is currently the best option we have, I think

[Eric Wieser]

Kevin Buzzard said:

I've recently run into another such situation -- I want D tensor[R] A to be an A-algebra but I think that we only have A tensor[R] D being an A-algebra, and if D tensor A is too, then A tensor A now has two (non-propeq) A-algebra structures. I propose getting around this by just making my instance a def, and promoting it to an instance locally. Does this sound OK?

Do you definitely need both structures? I know a lot of informal math prefers writing the ring on the right of tensor products instead of mathlib writing it on the left, but I'd be interested to see an example where that's not just a style choice.

[Kevin Buzzard]

I was chatting about this with de Jong during my visit to New York and he said that in any system (such as ours) with maps on the left, there's a good argument for having actions on the right, so you can write $f(mr)=f(m)r$. But I think that this would put us out of sync with most of the mathematical literature.

"Do you definitely need both structures" is kind of a tiresome question, because of course mathematicians need all obviously true things like $A\otimes B$ being both an $A$-module and a $B$-module, and somehow I feel like mathlib is putting the onus on me to try and figure out how to work around this just because the special case $A=B$ makes a diamond possible, even though it's not possible in my application. However, this is where we are, so I guess I'll have to think about it. Basically my situation is that I have a fixed base commutative ring $R$, a commutative $R$-algebra $A$ and a non-commutative $R$-algebra $D$, and extensive literature writing $D\otimes_R A$ and wanting a $D$-action on the left but also wanting it to be an $A$-module. I think that if our system doesn't let me do this then my conclusion is that this says something bad about our system. But I'll go away and think about how to work around this -- at least I understand what the problem is. But right now what I want to do is to just add the left $A$-algebra action, make it a local instance confident in the fact that $D\not=A$ (because for example $D$ really isn't commutative and $A$ is) and just get the argument out of the way (which is "...and hence it's a topological ring") and then forget the module structure (indeed the next line of the construction is "...and hence its units are a topological group" and now I never think about the $A$-module structure again).

[Eric Wieser]

I think for the tensor product, the instance does already exist as a def

[Eric Wieser]

I guess another way to handle this would be an (empty) class TensorProduct.GiveMeRightActions D R A which you can instantiate mid-proof to get all the relevant instances

[Eric Wieser]

That is, a way to opt into collections of problematic instances without having to turn them all on individually

[Kevin Buzzard]

For the tensor product the instance-as-a-def only exists under the assumption that D is commutative :-(

[Kevin Buzzard]

I think I'm happy switching things on on a case by case basis. At least, I feel like this should be able to get me through without causing problems.

[Johan Commelin]

The empty class idea is a nice one. But shouldn't we just get support for open scoped RightActions mid proof?

[Eric Wieser]

Johan Commelin said:

The empty class idea is a nice one. But shouldn't we just get support for open scoped RightActions mid proof?

That turns on notation, not new instances

[Eric Wieser]

But also, the trivial class approach lets you restrict the dangerous action to certain types

[Matthew Ballard]

This sounds like a job for a new attribute + tactic rather than the existing instance machine.

[Eric Wieser]

If that's a performance consideration, it would be good to measure before making that decision.

[Matthew Ballard]

Not really performance. Just a having a hammer so all things are nails consideration.

[Kevin Buzzard]

My proposal right now is to just plough on making instances locally and hoping that this won't cause a problem, and I suspect it won't. My work on topologies on modules just needs to kick in at some point to say "...and now this is a topological ring" and then I can forget the fact that it's a module completely (I think).

[Eric Wieser]

Yes, local instances are totally fine, but as you say this is annoying and it would be great to find a safe way to reduce the annoyance.

[Antoine Chambert-Loir]

Kevin Buzzard said:

I was chatting about this with de Jong during my visit to New York and he said that in any system (such as ours) with maps on the left, there's a good argument for having actions on the right, so you can write $f(mr)=f(m)r$. But I think that this would put us out of sync with most of the mathematical literature.

If $R$ is a (nonnecessary commutative) ring, and if you wish to have $n \times n$ matrices to act on $R^ n$ in the usual way, through the standard formulas, then you'd better view $R^n$ as a right-$R$-module. And even in the commutative case, the proof that they act linearly requires two applications of commutativity.