monoid_hom.map

Stream: maths

[Kevin Buzzard]

This is either a technical point or me fussing about nothing. I was just developing group theory from scratch for my undergraduate course (so no monoids) and afterwards I realised I'd put map (f : group_hom G H) : subgroup G -> subgroup H in the group_hom namespace rather than the subgroup namespace. Is there a category-theoretic reason that in mathlib it's in the subgroup namespace (i.e. something to do with functor.map), or is it just a convention / "random choice", or is it to do with the fact that group_hom = monoid_hom but subgroup != submonoid?

[Eric Wieser]

Certainly the fact that group_hom = monoid_hom (and ring_hom = semiring_hom) is relevant, but we cope with that already with docs#monoid_hom.range vs docs#monoid_hom.mrange and docs#ring_hom.range vs docs#ring_hom.srange

[Yury G. Kudryashov]

Also, submonoid.map agrees with list.map, finset.map, filter.map

[Kevin Buzzard]

But none of those could be in the morphism namespace because they're all function.map . Here we have a different kind of map

[Yury G. Kudryashov]

ring_hom can map at least subrings, subsemirings, and polynomials

[Eric Wieser]

Note we have docs#ring_hom.map_matrix, so we could have ring_hom.map_subring to match

[Eric Wieser]

Or we fix the functorial machinery so that we can actually use it for this type of thing

[Yury G. Kudryashov]

has_map (α β : Type*) (γ : out_param (Type*))?

[Yury G. Kudryashov]

(I'm not sure whether we want Type*s or Sort*s)

[Kevin Buzzard]

I'm not suggesting fixes or changes -- I was just trying to teach myself the algorithm for learning in which namespace to look for things like functions mapping subgroups to subgroups along group homomorphisms.

[Anne Baanen]

This discussion inspired a random idea: would it make sense to define subsemiring.range (f : α → β) := closure (set.range f)?

[Kevin Buzzard]

The image of a subsemiring under a ring hom is a subsemiring and the advantage of the "concrete" definition of range (the carrier is the set.range, and then you prove the axioms) is that it's sometimes handy to have x \in subsemiring.range f (when f is a ring hom) to be defeq to \exists a, x = f a. Or am I missing the point?

[Anne Baanen]

Right, so I guess I'm asking: is it worth it to lose that defeq in exchange for not having to prove that f is a ring hom ahead of time?

[Oliver Nash]

Anne Baanen said:

Right, so I guess I'm asking: is it worth it to lose that defeq in exchange for not having to prove that f is a ring hom ahead of time?

I think you could keep the desired defeq and still allow the user to defer the proof that their map is a ring hom, by defining range so that it consumes a function f together with a proof that set.range f = closure (set.range f).