notation for algebra_map

Stream: maths

[Johan Commelin]

Random thought. Should we have

notation `↑ₐ` := algebra_map _ _

• Pro: in informal maths, this is usually an invisible map. ↑ₐ is a lot more invisible than algebra_map _ _
• Con: It's pretty invisible to new users. Yet another mysterioglyph that needs to be learned and deciphered.

[Eric Wieser]

I made a thread about this maybe 6 months ago

[Oliver Nash]

I'm not sure about notation for this. When we're creating something resembling conventional mathematical notation then I see the case but I don't recall ever seeing notation for algebra_map in conventional mathematics (except maybe •).

[Eric Wieser]

In conventional mathematics we don't write A →ₐ[R] B or ↑n * r either though, right?

[Kevin Buzzard]

No, we write things like "A -> B is an R-algebra homomorphism" which is far worse

[Eric Wieser]

So both ↑ and ₐ are already "lean noise"

[Kevin Buzzard]

or "efficient compression"

[Oliver Nash]

Eric Wieser said:

In conventional mathematics we don't write A →ₐ[R] B or ↑n * r either though, right?

I could be blind to the craziness of familiar notation (both formal and informal) but at least for me the distance between our A →ₐ[R] B and the conventional A → B (where context disambiguates) is smaller than between ↑ₐ and what we'd write informally (e.g, • or f or nothing).

[Kevin Buzzard]

I think I'd write nothing at all for algebra_map -- if B is an A-algebra then elements of A "are" elements of B.

[Oliver Nash]

Right.

[Oliver Nash]

I'm not against ↑ₐ though, I enjoy using fewer characters. I just don't want Mathlib to become as opaque to new users as APL.

[Johan Commelin]

ι gεt θat :wink: APL φτɯ

[Johan Commelin]

There was the old proposal to get rid of algebra_map and just use a • b everywhere. Maybe that's the best option after all.

[Kevin Buzzard]

I'm confused. Surely \bub can only be used when doing algebra_map a * b? What if I want to do (algebra_map a)^2?

[Kevin Buzzard]

docs#algebra_map

[Johan Commelin]

(a • 1)^2 :see_no_evil:

[Kevin Buzzard]

Great

[Johan Commelin]

It's still shorter :see_no_evil:

[Oliver Nash]

I'm still holding out hope that someone will change the definition of algebra so that it extends module and does not include the map.

[Kevin Buzzard]

But we still need to refer to the map sometimes

[Oliver Nash]

Yes but it will be definitionally shorter which should help.

[Oliver Nash]

Or more precisely we won't write algebra_map for the times when we don't care that the scalar action is also a multiplicative homomorphism.

[Oliver Nash]

Anyway I've ruined this thread. There are good reasons to consider ↑ₐ. I'm not against it, just on the fence.

[Anne Baanen]

What if we made a class extending has_coe(_t?) stating the coercion is a ring hom? This could replace the uses of algebra where we want algebra_map to be defeq to something concrete, and it gives nice and easy ↑ notation for the easy case. We'd still want some notation for the bundled map, but that should occur less (I hope!) than the unbundled, applied coercion.

[Johan Commelin]

The downside is that it would duplicate a bunch of ring hom API.

[Anne Baanen]

On the other hand, we'll deduplicate e.g. docs#int.cast_mul, docs#subring.coe_mul, etc.

[Eric Wieser]

We'd still need a typeclass to say that smul and the coercion are consistent though

[Anne Baanen]

Either that, or we make a has_ring_coe.to_algebra instance.

[Eric Wieser]

That would generate data which is bad

[Johan Commelin]

Anne Baanen said:

What if we made a class extending has_coe(_t?) stating the coercion is a ring hom?

Could this just be an extra part of the existing [algebra A B]?

[Johan Commelin]

Then we would automatically have compatibility with smul, etc...

[Eric Wieser]

Yes, that's what algebra.smul_def is today

[Johan Commelin]

It would mean that every search for a coe between A and B would fire [semiring A] [semiring B] [algebra A B]. Is that a problem?

[Eric Wieser]

(Here's the old thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20.60algebra_map.60.20.2F.20.60algebra.2Eof_id.60/near/216356787)

[Eric Wieser]

If we go down this route, I would envisage something like:

class has_ring_hom_coe extends ring_hom A B.

instance [has_ring_hom_coe A B] : has_coe_t A B := sorry

-- just like we have today, but `ring_hom` is replaced with `has_ring_hom_coe`
class algebra extends has_ring_hom_coe R A :=
-- the same fields we have today

[Eric Wieser]

To summarize, I guess this is the "yes, let's have notation and it should just be coe" answer to your question

[Eric Wieser]

A crazier option would be to change the type of coe from A → B to coe_wrapper A B (a single-field structure) and then we can register a ring_hom_class (coe_wrapper A B), monoid_hom_class, etc under suitable situations

[Johan Commelin]

What is the benefit of having both has_ring_hom_coe and algebra?

[Riccardo Brasca]

I would like to add that sometimes we really want to talk about the map. For example in flt-regular we are using a lot the fact that sometimes it is automatically injective.

[Anne Baanen]

Not sure that I like it, but how about the spelling ring_hom.coe A B for what used to be algebra_map A B?

[Eric Wieser]

Johan Commelin said:

What is the benefit of having both has_ring_hom_coe and algebra?

docs#matrix.scalar satisfies the first but not the second when R is not commutative

[Anne Baanen]

Johan Commelin said:

What is the benefit of having both has_ring_hom_coe and algebra?

I want my canonical maps to have concrete defeqs, while Oliver doesn't want to have the algebra_map field in algebra. If I can use has_ring_hom_coe instead, then an algebra_map-less algebra is fine for me.

[Eric Wieser]

Note that I'm in the middle of a large algebra refactor regarding right actions (#10716), so I'd appreciate it if people could hold off on starting a large parallel one!

[Damiano Testa]

My personal view is that up-arrows feel much less "mathematical" than decorated left-to-right arrows or bullets for multiplication.

I actually find the proposal of writing a • b quite good: I am used to writing the product of elements of A and of an A-algebra B in the same way as multiplication in either A or B alone, but there is always something in the back of my mind saying that the notation should really acknowledge that they are not the same...

[Anne Baanen]

Right, mathematically it would make sense to delete algebra_map altogether and just write a • 1 for the inclusion of the scalars into the algebra. The thing is that you very often encounter a pair of rings with a canonical map between them: a subring and a larger ring, {ℕ, ℤ, ℚ} and a {semiring, ring, field of char 0}, a ring and its fraction field, a ring of integers and a number field, ... It doesn't quite make mathematical sense to use "algebra" to describe this situation, but the algebra class does work well. So my proposal to make a coe_ring_hom class is to separate the second kind of usage from the first, so that (later) we can get rid of algebra_map and just write a • b.