binding power of ≃ₐ[R]

Stream: mathlib4

[Kevin Buzzard]

I just noticed this when doing Frobenius elements:

import Mathlib.Algebra.Algebra.Equiv
import Mathlib.RingTheory.Ideal.Quotient

variable {A : Type*} [CommRing A] {B : Type*} [CommRing B] (Q : Ideal B) (P : Ideal A)
  [Algebra (A ⧸ P) (B ⧸ Q)]

#check (B ⧸ Q) ≃+* B ⧸ Q -- works
#check B ⧸ Q ≃+* B ⧸ Q -- works and syntactically the same as previous line
#check (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q -- works
#check B ⧸ Q ≃ₐ[A ⧸ P] B ⧸ Q -- fails (not parsed in the same way)

The reason is

notation:35 G " ⧸ " H:34 => HasQuotient.Quotient G H

infixl:25 " ≃+* " => RingEquiv

notation:50 A " ≃ₐ[" R "] " A' => AlgEquiv R A A'

Looking at precedence of things like ≃ and →ₑ[φ] makes me think that 25 is correct, but it also raises another question: should the notation definition for AlgEquiv look more like LinearMap?

notation:25 M " →ₗ[" R:25 "] " M₂:0 => LinearMap (RingHom.id R) M M₂

?

[Eric Wieser]

Perhaps we should define a :morphismPrec syntax in mathlib that means :25 or :50 or whatever, and use that everywhere?

[Eric Wieser]

(to match :arg, :max, etc)

[Eric Wieser]

I can't think of a case where the R:25 vs R really matters, unless someone makes a syntax with unmatched ]s, so only the other two precedences are relevant.

[Kevin Buzzard]

I don't know what the numbers mean in Lean 4, I used to understand lean 3 notation but I've never upgraded. What's the 0 at the end?