ring_hom notation and friends

Stream: general

[Jireh Loreaux]

I now have need to discuss non-unital subrings, and so I was going to first define non_unital_ring_hom in algebra.ring.basic as:

structure non_unital_ring_hom (α : Type*) (β : Type*) [non_unital_non_assoc_semiring α]
  [non_unital_non_assoc_semiring β] extends mul_hom α β, α →+ β

But there is the issue of notation. non_unital_ring_hom is an awfully long name to not have any associated notation, but the natural choice α →+* β is already taken by ring_hom. Of course, this comes up in two other situations, namely, mul_hom, where the natural notation α →* β is taken by monoid_hom, but this is not so bad since mul_hom is short. But then there is also non_unital_alg_hom, where the notation α →ₐ[R] β is usurped by alg_hom.

So, how would people feel about adding a ₁ to the notation for the versions with map_one, thereby unlocking the notation for the other homs? To be explicit, I am proposing:

1. α →*₁ β, α →+*₁ β, α →ₐ₁[R] β for monoid, ring and algebra homs.
2. α →* β, α →+* β, α →ₐ[R] β for mul_hom, non-unital ring hom (doesn't exist yet), and non-unital algebra hom?

[Yaël Dillies]

and docs#monoid_with_zero_hom?

[Yaël Dillies]

What about →+*\₁ for non_unital_ring_hom? (:rofl:)

[Jireh Loreaux]

Good point, I guess that should be monoid with zero hom should be α →*₀₁ β?

[Yaël Dillies]

Note that we now have algebraic order homs too: docs#order_monoid_hom, docs#order_monoid_with_zero_hom, docs#order_ring_hom, docs#order_ring_iso.

[Jireh Loreaux]

If we don't have the corresponding non-unital versions, I don't mind leaving other stuff as is for now.

[Jireh Loreaux]

Speaking of which, it doesn't look like we have semigroup_with_zero_hom, so maybe monoid_with_zero_hom doesn't need to change.

[Jireh Loreaux]

Another option would be to rename non_unital_ring to to rng, but (a) I've always hated that, and (b) there's no "i" to remove in "algebra".

[Yaël Dillies]

You're hitting algebrasts problems.

[Eric Rodriguez]

you could also use other arrows, like category theorists do. this seems suboptimal, though

[Eric Wieser]

Are you sure you actually need all these as bundled types?

[Yaël Dillies]

It would be a shame not to use the fancy new hom hierarchy, especially now that Jireh understood how it works.

[Jireh Loreaux]

@Eric Wieser Why would we not want it as a bundled type? I think the only reason it doesn't exist yet is that the algebraists have thus far only been concerned with unital rings (some algebraist please correct me if I'm mistaken). I am only adding non_unital_ring_hom anyway. (edit: I sent this and then realized you were probably talking to Yaël about the order versions.)

[Adam Topaz]

What's wrong with →'+* (and the analogous notation for the other arrows as well). One has to decide where to put the ':
→'+* vs. '→+* vs. →+*'. I think →+'* should be avoided.

[Yaël Dillies]

I would prefer the third because searching for →+* will also hit those.

[Eric Wieser]

I mean any of these; I'd argue we shouldn't aim to have every one of the exponentially many ways to pull legs off the morphism caterpillar (as I think I heard Reid describe it), but should have ideally a use case in mind of something that would consume each new type before we add

[Eric Wieser]

In the past, I've used "I need it for a universal property", and Yaël's used "I need foo_hom so that I can build the category of Foo". Anything stronger than "hey, we don't have this combination of legs yet" is probably a fine reason

[Jireh Loreaux]

Alright, so here is where it came up for me: I'm looking at C₀(α, R) where α is a topological space and R is a topological ring (non-unital or unital, it doesn't matter, because the function ring is non-unital). Then the point is to show that C₀(α, R) is isomorphic to the subring (actually, its a two-sided ideal, but we don't have those yet either) of C(alexandroff α, R) consisting of the functions f such that f ∞ = 0. Then, use this isomorphism to show that there is an isomorphism between unitization R C₀(α, R) and C(alexandroff α, R).

[Johan Commelin]

Eric Wieser said:

one of the exponentially many ways to pull legs off the morphism caterpillar (as I think I heard Reid describe it),

FYI: https://en.wikipedia.org/wiki/Centipede_mathematics

[Jireh Loreaux]

I agree we shouldn't just go defining arbitrary morphism classes until we need them; at the very least, it seems like there should be better ways to spend our time.

[Jireh Loreaux]

/poll New notation for ring_hom R S
R →¹+* S
R →+*¹ S
R →₁+* S
R →+*₁ S
Don't change my ring hom notation!

[Johan Commelin]

:stuck_out_tongue_wink: General rule: If you rip a leg of a well-functioning morphism caterpillar you have to put that leg back into the piece of notation for the crippled caterpillar. /s

[Jireh Loreaux]

Well, message clearly received, I won't change anybody's ring hom notation :sweat_smile: ! Any suggestions for good notation for non_unital_ring_hom then? Maybe R →ₙ+* S with the ₙ being for "non-unital"?

[Johan Commelin]

That seems like a good suggestion to me.

[Eric Wieser]

Alternatively, R →+*₀ S which is the existing R →*₀ S with addition.

[Scott Morrison]

I sort of like →+*' on the basis that the prime is telling you the multiplicative structure is a bit wonky.

[Eric Wieser]

I guess we could then have →*' for mul_hom too

[Jireh Loreaux]

I'm hesitant about the prime notation. Reason: When Adam originally suggested it above, I didn't even realize it was a prime, I thought it was a one, like I had originally suggested. It wasn't until Scott explicitly said "prime" that everything clicked.

As for →+*₀, this doesn't really have the stated relationship because →*₀ is a monoid with zero hom, not a semigroup with zero hom, and what we are talking about here is a non-unital ring hom.

[Johan Commelin]

Ooh, that's a good point. So →+*₀ is indeed sub-optimal. I think your →ₙ+* is maybe the winner.

[Eric Rodriguez]

I was just looking in the Unicode arrows and found ⥅. Could we do ⥅*? Or too confusing?

[Yaël Dillies]

We managed to stick to → for morphisms so far, so we would have to justify the difference here.

[Jireh Loreaux]

#13430 introduces non-unital ring homs with the notation R →ₙ+* S. In order to parallel this, in #13470 I introduce A →ₙₐ[R] B for non_unital_alg_hom R A B. Is this good or do we want something else?

[Jireh Loreaux]

/poll Notation for non_unital_alg_hom
A →ₙₐ[R] B

[Eric Wieser]

Probably the options for that poll should be notation for both ring_hom and alg_hom together; obviously they should be consistent, but I don't think we reached a consensus for the ring notation yet.

[Eric Wieser]

(in fact, I'd argue we should pick a notation for mul_hom, aka "non unital monoid_hom", at the same time)

[Jireh Loreaux]

Alright, create a new poll the way you see fit, I don't think I can delete the old one.

[Jireh Loreaux]

/poll non-unital hom notations (algebra, ring, semigroup)
A →ₙₐ[R] B and R →ₙ+* S and M →ₙ* N
A →ₐ'[R] B and R →+' S and M →' N

[Jireh Loreaux]

Per @Eric Wieser's suggestion above, here is a poll for uniform notation for non_unital_alg_hom R A B, non_unital_ring_hom R S (see #13430), and mul_hom M N. In the above ₙ means "non-unital". I'm pinging the following people because they participated in the previous poll about ring_hom notation and so thought they might want input: (@Oliver Nash @Frédéric Dupuis @Patrick Massot @Johan Commelin @Reid Barton @Sebastien Gouezel @Alex J. Best @Thomas Browning @Moritz Doll @Scott Morrison @Anne Baanen )

[Jireh Loreaux]

Given the above, #13470 for non_unital_alg_hom and #13526 for mul_hom. These should not go into the same batch. I'm sure there will be a merge conflict between them that needs resolving.

[Eric Wieser]

I assume we will want A →ₙ+ B too for add_hom?

[Jireh Loreaux]

I guess here the ₙ means "no zero"?

[Eric Wieser]

"non-identital"?

[Jireh Loreaux]

I could see having A →ₙ+ B for consistency, but I'm not too attached to assigning notation for it at the moment. The multiplicative versions are nice for me currently because I'm doing a lot of work to get the non-unital ring API up and running (and I'm dealing a lot with semigroups and mul_hom there as a result). I don't expect there will be a parallel use case with add_semigroups and add_hom; although eventually there might be a different use case.