OreLocalization.smul reducibility

Stream: mathlib4

[Kevin Buzzard]

Right now OreLocalization.smul is irreducible. So if A is an R-module and S is a submonoid of R, then A[S⁻¹] is an R[S⁻¹]-module. In mathlib we have defined mul on R[S⁻¹] as being equal to smul, so if a b : R[S⁻¹] then a • b = a * b and the proof is rfl.

If however A is an R-algebra then in #16650 I made A[S⁻¹] into an R[S⁻¹]-algebra, and now if a b : A[S⁻¹] then a • b = a * b and the proof isn't rfl (at least not according to typeclass inference) because smul is irreducible so Lean can't see that it's defeq to mul. Here is some code illustrating this:

import Mathlib.Algebra.Algebra.Defs
import Mathlib.RingTheory.OreLocalization.Basic

namespace OreLocalization

section CommMagma

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

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

private def mul''
  (a : A) (s : S) : A[S⁻¹] → A[S⁻¹] :=
  liftExpand (mul' a s) fun a₁ r₁ ⟨s₁, hs₁⟩ hr₁s₁ => by
  sorry -- proof omitted

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

-- OreLocalization.smul is irreducible but this still
-- works because mul on R[S⁻¹] is defined to be smul.
example (a b : R[S⁻¹]) : a • b = a * b := rfl

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

-- But here irreducibility causes problems:
example (as bt : R[S⁻¹]) : as * bt = as • bt := rfl -- fails

example (as bt : R[S⁻¹]) : as * bt = as • bt := by
  unfold HSMul.hSMul instHSMul SMul.smul instSMul
  -- rfl -- fails
  unfold OreLocalization.smul
  rfl -- now works

end CommMagma

end OreLocalization

To make the last proof rfl you can just remove the irreducible attribute on smul. This I do in #16746 and my understanding of recent comments by @Eric Wieser was that this is the right thing to do in this situation. However benchmarking only this change reveals that it makes the file Algebra.Module.LocalizedModule 8% slower. Is this a deal breaker?

[Eric Wieser]

In my opinion correctness wins over performance unless the performance is really disastrous. An 8% change in just one file doesn't seem too bad to me.

[Eric Wieser]

In a future change, you could try making liftExpand irreducible instead

[Eric Wieser]

Something I'd very much like to have here is a way to tell the elaborator to treat lift as a recursor and mk as a constructor, such that both are irreducible in isolation but lift f (mk x) reduces to f x

[Kevin Buzzard]

Here is another diamond which making smul not-irreducible doesn't fix:

rs : OreLocalization S R
⊢ liftExpand (fun r s ↦ Quotient.mk' (r, s)) ⋯ rs = rs

Proof is cases rs; rfl. Here OreLocalization S R is a quotient of R x S. The fact that this isn't rfl means that if I make A[1/S] into an R[1/S]-algebra and add this to typeclass inference then there are two nondefeq toFun instances of Algebra R[S⁻¹] R[S⁻¹] floating around. Is it likely that I can solve this by refactoring liftExpand?

[Eric Wieser]

That looks impossible to make rfl; but presumably this is an #xy problem and came from reducing something else that you wanted to be rfl?

[Kevin Buzzard]

Right, I want to make Algebra R[1/S] A[1/S] from Algebra R A but then I get two nondefeq Algebra R[1/S] R[1/S] instances

[Eric Wieser]

I think this is a problem with any attempt to make Algebra A B -> Algebra (F A) (F B) instances, for most Fs

[Eric Wieser]

But arguably you should never create those instances anyway, as they create propositional diamonds when B := F A