Algebra.Algebra.Basic

Stream: mathlib4

[Yury G. Kudryashov]

I started porting Algebra.Algebra.Basic before all required PRs made it to mathlib3port. I'll use my restart-port script to fix it tomorrow.

[Notification Bot]

4 messages were moved from this topic to #mathlib4 > restart port by Yury G. Kudryashov.

[Yury G. Kudryashov]

I've started looking at the file and I have some questions about porting the "algebra_map as a coercion" code.

[Yury G. Kudryashov]

0. Is CoeTC the right typeclass?

1. If I add an instance [algebra R A] : CoeTC R A := ⟨algebra_map R A⟩, then

   • Lean 4 will unfold coercions, and we'll deal with algebra_map R A x everywhere;
   • there won't be any definition that can be tagged with @[coe], so we'll have these algebra_maps in the goals view etc;
   • there will be two competing Coe Nat R instances for every semiring R; same with Int and a ring; same with NNReal and Real;
   • moreover, one of the two competing instances will be a bundled ring homomorphism.

2. If we make the coercion function an outParam argument, then

   • it will look ugly;
   • there will be no symbol for simp/norm_cast lemmas to match on.

What should I do? Do I miss more issues? solutions?

[Eric Wieser]

I think having algebra_map in the goal is ok for now; using coes for algebra_map behaves poorly in Lean 3 anyway, as we reverted the refactor that made it work well due to porting concerns

[Kevin Buzzard]

I have been long interested in the concept of a "canonical" map and one working definition I have is "it would be a coercion in lean". But the algebra map is definitely canonical :-)

[Yury G. Kudryashov]

I forgot about one more option:

3. Define Algebra.cast and use it as a coercion. This way the behavior is very close to that of mathlib 3; the only exception is that this coercion is not reducibly defeq to, e.g., Nat.cast.

[Eric Wieser]

So to be clear, we can define a Coe instance for algebra_map abd everything is fine, but we can't tag algebra_map with @[coe] for pretty-printing becuase it's bundled and not a raw function?

[Yury G. Kudryashov]

If we define Coe to be algebra_map, then the behavior will differ from Lean 3 (coe_add etc will be simp lemmas because of map_add etc; nothing will be norm_cast).

[Yury G. Kudryashov]

BTW, let me repeat Q0: which typeclass should I use? docs4#CoeHTCT ? docs4#CoeDep ? Something else?

[Yury G. Kudryashov]

OTOH, if we define coercion to be Algebra.cast, then we'll have norm_cast but the up arrow will have (at least) 2 meanings for Nat -> R.

[Yury G. Kudryashov]

I'm going to try the Algebra.cast solution. IMHO, it is the closest to what we have in Lean 3.

[Yury G. Kudryashov]

I rebased !4#2234 on !4#2244 and now coercion NNReal → Real uses NNReal.toReal before I define an Algebra instance and it uses Algebra.cast after I define it.

[Yury G. Kudryashov]

What should I do about it?

[Eric Wieser]

Probably AlgebraCast should be a standalone class

[Eric Wieser]

Then you can build that up front, and add the structure later

[Yury G. Kudryashov]

This will work for NNReals but I'm afraid that some lemmas about Nat or Int formulated after Algebra.cast can accidentally use Algebra.cast. What about making Algebra.cast a scoped instance?

[Yury G. Kudryashov]

The problem with AlgebraCast is that this is a solution half-way towards "let's create our own MathlibCoe class and use it for all Coes". IMHO, we should either avoid generic Coes like Algebra.cast or move to MathlibCoe (with a better name) everywhere.

[Chris Hughes]

Isn't one of the advantages of the Lean4 approach that a coe can also be a bundled morphism? Probably at least we need RingHomCoe, GroupHomCoe etc ?

[Yury G. Kudryashov]

I don't want to change too much during port.

[Yury G. Kudryashov]

We can try different options later.

[Eric Wieser]

@Chris Hughes: the @[coe] attribute can't be used on bundled morphisms

[Chris Hughes]

Oh. I didn't realise that. In the long run we need to know that coercions are morphisms right?

[Chris Hughes]

And in a way that lets us do things like hom_ext.

[Eric Wieser]

In the long run we need to know that coercions are morphisms right?

Yes, but often the type of morphism depends on the ambient structure. x => (x, x) would be a reasonable coercion, that's additive if X is, multiplicative if X is, etc. @Anne Baanen already made this refactor in Lean3, but it was reverted as it was deemed to interfere with the port.