Algebra.cast

Stream: mathlib4

[Artie Khovanov]

The (scoped) coercion from a commutative semiring to an algebra over this semiring is registered as Algebra.cast, which is reducibly defeq to algebraMap, but not syntactically or simp-equal. In fact, absolutely nothing is proved about Algebra.cast except that it commutes with ring operations.

This makes it annoying to state lemmas about algebras because you have to either write algebraMap _ everywhere or rewrite away the casts. I therefore propose to either

1. add a simp lemma Algebra.cast_eq_algebraMap, or
2. remove Algebra.cast and change the scoped coercion to be algebraMap.

What are people's thoughts?

[Aaron Liu]

I prefer #2

[Aaron Liu]

we don't need more nothing-definitions

[Riccardo Brasca]

I also prefer the second option. Note that this should stay scoped, as in the very common case R is ℤ there is already a coercion ℤ → A.

[Artie Khovanov]

#32991

[Artie Khovanov]

Here is a problem with option 2: @[coe] can only be applied to function type declarations. Therefore it doesn't work for algebraMap, which is bundled. This breaks the delaborator, which is fine - but it also breaks norm_cast, which is an issue. I want to register coe for the expression @DFunLike.coe (R →+* A) R (fun x ↦ A) RingHom.instFunLike (algebraMap R A). Working up to reducible defeq by defining Algebra.cast is not good enough because Mathlib tactics care about syntactic equality (ie, status quo / option 1 is bad).

[Riccardo Brasca]

In my opinion we should live with the fact that algebraMap is not a coercion. We already do so in most of the library, and even if it is not the perfect solution it works in practice.

[Artie Khovanov]

In that case we should add a simp lemma to convert between Algebra.cast and algebraMap. The current situation is very bad: we have a nothing-definition with no API!

[Johan Commelin]

Maybe Riccardo is suggesting:

3. remove Algebra.cast

[Riccardo Brasca]

Yes, honestly I don't see why it's there. The idea is nice, but in practice it doesn't work. Is it used a lot?

[Eric Wieser]

It's there because it was part of a larger development that got reverted by the port

[Eric Wieser]

I believe the plan was to make it the simp-normal form instead of algebraMap (which has the benefit of making it work for towers of monoids and groups, like the units of the rings)

[Eric Wieser]

The plan was a little more compelling in Lean 3 where it could replace Nat.cast, Int.cast, and Rat.cast at the same time

[Artie Khovanov]

Oh OK
Yeah let's remove Algebra.cast

[Artie Khovanov]

#32991 - remove Algebra.cast

[Artie Khovanov]

Riccardo Brasca said:

Yes, honestly I don't see why it's there. The idea is nice, but in practice it doesn't work. Is it used a lot?

Places where the cast is actually used as a cast (as opposed to notation):
Algebra.adjoin_insert_natCast
div_eq_quo_add_rem_div_add_rem_div
(WIP)

[Eric Wieser]

See also #mathlib4 > Algebra.cast and algebraMap @ 💬

[Artie Khovanov]

ah, an old question
I would really suggest having a simp lemma for now and then we can decide whether to go ahead with ripping out the coercion in future

[Artie Khovanov]

@Eric Wieser what do you mean when you say the following:
image.png
If there is some way to make algebraMap work with norm_cast, then we should just do that.

[Eric Wieser]

(note you can quote messages from other threads rather than screenshotting)

[Artie Khovanov]

So.. what does that message mean? Is there some way to make algebraMap work with norm_cast?

[Aaron Liu]

I thought @[coe] was just a pretty printer thing

[Aaron Liu]

why is it messing up norm_cast

[Artie Khovanov]

norm_cast looks for coercion instances. It is not possible to register a bundled function as a coercion.

[Jireh Loreaux]

No, norm_cast looks for @[coe] attributes, not coercion instances, those attributes don't just affect pretty-printing.

[Jireh Loreaux]

In particular, since Lean inserts the function underlying a coercion (via coercion instances) during elaboration, the fact that they were / are a coercion would be lost in the resulting Expr, so we need the attribute to tell Lean "hey, when you see Subtype.val, that's a coercion."

[Artie Khovanov]

Ah, thanks for the correction! The situation is the same though right? It sounds like there's no way to make this work, then?

[Eric Wieser]

I think there's a request here for a version norm_cast that accepts an explicit list of names rather than just everything tagged with coe

[Eric Wieser]

norm_cast could be a shorthand for norm_fun [Coe.coe] or similar

[Artie Khovanov]

Or alternatively a request to allow coercion functions to be bundled, via a CoeFun instance.

[Artie Khovanov]

Or both tbh :joy:

[Eric Wieser]

I think we have exactly one function we want to do that with (algebraMap), but if we decided to

Eric Wieser said:

make [Algebra.cast] the simp-normal form instead of algebraMap (which has the benefit of making it work for towers of monoids and groups, like the units of the rings)

then we would have zero of them

[Artie Khovanov]

The issue with making it the SNF is we lose all the bundled function API
I'd rather have a bare coercion that simps to algebraMap

[Artie Khovanov]

Also we could make the Nat.toInt etc coercions bundled!

[Eric Wieser]

docs#Nat.toInt isn't a thing

[Artie Khovanov]

Sorry I mean Nat.cast

[Aaron Liu]

Artie Khovanov said:

Sorry I mean Nat.cast

There are times when it makes sense to not bundle those, and there are times it makes sense to use docs#Nat.castRingHom etc.

[Aaron Liu]

Artie Khovanov said:

It is not possible to register a bundled function as a coercion.

Why do you say this? I think it's definitely possible

[Aaron Liu]

you just write a CoeFun instance and you make the coercion part the bundled function

[Artie Khovanov]

Aaron Liu said:

Artie Khovanov said:

Sorry I mean Nat.cast

There are times when it makes sense to not bundle those, and there are times it makes sense to use docs#Nat.castRingHom etc.

Well in that case we should add API to Algebra.cast to relate it to algebraMap!

[Artie Khovanov]

Like we should do something

[Aaron Liu]

well the difference is that I don't think it makes sense to not bundle algebraMap

[Artie Khovanov]

right

[Aaron Liu]

like with the absolutely minimal assumptions you put that makes the definition work is still gives you enough to make it bundled

[Aaron Liu]

whereas there's times that Nat.cast is useful but the target isn't a ring

[Eric Wieser]

Aaron Liu said:

like with the absolutely minimal assumptions you put that makes the definition work is still gives you enough to make it bundled

Only because the current generality is wrong; consider non-associative rings or non-commutative base rings or monoids.

[Eric Wieser]

e.g.

class AlgebraCast (R A) where
  algebraCast : R → A

-- imagine that `Algebra` extended `AlgebraCast`
instance [Algebra R A] : AlgebraCast R A where algebraCast := algebraMap R A

-- This can't be bundled as a ringhom
instance [Algebra R A] : AlgebraCast Rˣ Aˣ where
  algebraCast r := ⟨algebraCast r, algebraCast r⁻¹, sorry, sorry⟩