Units.prod, Units.fst, Units.snd

Stream: mathlib4

[Kevin Buzzard]

I can't believe we're missing these -- am I just not looking in the wrong place? (I guess they all work for monoids too)

import Mathlib

variable {R S : Type*} [Ring R] [Ring S]

-- do we not have this?
def Units.prod (u : Rˣ) (v : Sˣ) : (R × S)ˣ where
  val := (u, v)
  inv := ((u⁻¹ : Rˣ), (v⁻¹ : Sˣ))
  val_inv := by simp
  inv_val := by simp

-- do we not have these?
def Units.fst : (R × S)ˣ → Rˣ :=  Units.map (MonoidHom.fst R S)
def Units.snd : (R × S)ˣ → Sˣ :=  Units.map (MonoidHom.snd R S)

While I'm here, which of these should I be using in a "prod" lemma?

open NNReal
noncomputable def ringHaarChar : Rˣ →* ℝ≥0 := sorry -- a thing (under extra assumptions)

-- which should be ringHaarChar_prod? Or should I have both?
lemma ringHaarChar_prod (u : Rˣ) (v : Sˣ) :
    ringHaarChar (u.prod v) = ringHaarChar u * ringHaarChar v := by sorry

lemma ringHaarChar_prod' (uv : (R × S)ˣ) :
    ringHaarChar uv = ringHaarChar uv.fst * ringHaarChar uv.snd := by sorry

[Kevin Buzzard]

Aah, found it: docs#MulEquiv.prodUnits

[Kevin Buzzard]

So I'm supposed to write this?!

example (u : Rˣ) (v : Sˣ) :
    ringHaarChar (MulEquiv.prodUnits.symm (u, v)) = ringHaarChar u * ringHaarChar v := by sorry

example (uv : (R × S)ˣ) :
    ringHaarChar uv =
    ringHaarChar (MulEquiv.prodUnits uv).1 * ringHaarChar (MulEquiv.prodUnits uv).2 := by sorry

My versions look more beautiful! Do we want my suggestions?

[Wrenna Robson]

I do think this looks like useful API.

[Wrenna Robson]

Though I think you'd want them as MulHoms, no?

[Wrenna Robson]

@[simps!?]
def Units.prod : Mˣ × Nˣ →* (M × N)ˣ := sorry

def Units.fst : (M × N)ˣ →* Mˣ := Units.map (MonoidHom.fst M N)
def Units.snd : (M × N)ˣ →* Nˣ := Units.map (MonoidHom.snd M N)

[Wrenna Robson]

This kind of thing

[Wrenna Robson]

def Units.prod : Mˣ × Nˣ →* (M × N)ˣ :=
  MonoidHom.toHomUnits (MonoidHom.prodMap (Units.coeHom M) (Units.coeHom N))
def Units.fst : (M × N)ˣ →* Mˣ := Units.map (MonoidHom.fst M N)
def Units.snd : (M × N)ˣ →* Nˣ := Units.map (MonoidHom.snd M N)

[Wrenna Robson]

Think it's this if I've got the right library functions. Let me write out the simp lemmas (simps doesn't seem to make something nice, kinda chokes on Prod.map it seems, which feels a bit like a deficiency in Prod.map_apply but anyway).

[Eric Wieser]

I suspect what Kevin is observing is a common pattern across a lot of API; that we declare some heavily bundled equivalence, and don't bother trying to write definitions for all the separate pieces (especially if those pieces don't hold in any greater generality.

[Eric Wieser]

Arguably this is a deliberate decision; it reduces the amount of API we have to maintain, and the number of lemmas we have to write that just duplicate API about the equivalence

[Wrenna Robson]

namespace Units

variable [Monoid M] [Monoid N]

/-- A map from the product of the units of two monoids to the units of their product. -/
@[to_additive prod "A map from the product of the additive units of two
    additive monoids to the additive units of their product."]
def prod : Mˣ × Nˣ →* (M × N)ˣ :=
  MonoidHom.toHomUnits (MonoidHom.prodMap (Units.coeHom M) (Units.coeHom N))

@[to_additive (attr := simp) val_prod_apply]
theorem val_prod_apply (g : Mˣ × Nˣ) : (prod g).val = (g.1.val, g.2.val) := rfl

@[to_additive (attr := simp) val_inv_prod_apply]
theorem val_inv_prod_apply (g : Mˣ × Nˣ) : (prod g)⁻¹.val = (g.1⁻¹.val, g.2⁻¹.val) := rfl

/-- The first element of the units of the product of two monoids. -/
@[to_additive (attr := simps!) "The first element of the additive units of the
  product of two additive monoids."]
def fst : (M × N)ˣ →* Mˣ := Units.map (MonoidHom.fst M N)

/-- The second element of the units of the product of two monoids. -/
@[to_additive (attr := simps!) "The second element of the additive units of the
  product of two additive monoids."]
def snd : (M × N)ˣ →* Nˣ := Units.map (MonoidHom.snd M N)

@[to_additive (attr := simp) fst_prod]
theorem fst_prod (g : Mˣ × Nˣ) : (prod g).fst = g.1 := rfl

@[to_additive (attr := simp) snd_prod]
theorem snd_prod (g : Mˣ × Nˣ) : (prod g).snd = g.2 := rfl

@[to_additive (attr := simp) prod_fst_snd]
theorem prod_fst_snd (g : (M × N)ˣ) : prod (fst g, snd g) = g := rfl

end Units

[Wrenna Robson]

Something like this I think.

[Wrenna Robson]

Unless there's any obvious comments I'll make a PR.

[Yakov Pechersky]

Do you also want to have the reverse, the inl and inr, given that products and coproducts are the same here?

[Wrenna Robson]

Oh that's a good point

[Wrenna Robson]

And presumably they have some relation to fst and snd?

[Yakov Pechersky]

Yeah, fst (inl u N) is going to be u, snd (inl u N) is going to be 1, etc.

[Wrenna Robson]

Weirdly we seem to have (for MonoidHom, not units), fst_comp_inl rather than fst_inl as I might expect, i.e. it is the same theorem but not applied.

[Wrenna Robson]

Which seems a bit off-style but maybe not here? Which do you think is better?

[Yakov Pechersky]

Well, it's a lemma about composition of monoid homs which gives another monoid hom, either id or 1.

[Wrenna Robson]

True, true.

[Wrenna Robson]

Here I could do

theorem fst_comp_inl  : fst.comp (inl (N := N)) = MonoidHom.id Mˣ := rfl
```
or
```
theorem fst_inl (u : Mˣ) : fst (inl (M := M) (N := N) u) = u := rfl
```

[Yakov Pechersky]

(Related PR of mine, #22420), just haven't had time to actually sit down and tidy it, nor do the plain GroupWithZero homs.

[Wrenna Robson]

I feel like the latter feels better here.

[Yakov Pechersky]

You could have both.

[Wrenna Robson]

True, just sort of feel I want it for MonoidHom as well. But I guess reviewers can decide that.

[Wrenna Robson]

Is there an associated equiv? It feels like no?

[Yakov Pechersky]

Which would be the equiv here?

[Yakov Pechersky]

The equiv is already Units.prod.

[Yakov Pechersky]

iiuc

[Yakov Pechersky]

Sorry, what I meant was the existing docs#MulEquiv.prodUnits

[Wrenna Robson]

I meant apart from that.

[Yakov Pechersky]

so Units.prod := MulEquiv.prodUnits.symm.toMonoidHom

[Jz Pan]

But I think an equiv version is already enough?

[Jz Pan]

Seems that it does not have simp lemmas (together with a lot of things in that file).

[Wrenna Robson]

Yes, as Kevin noted originally, but what he was asking for was something more ergonomic to use API-wise.

[Wrenna Robson]

#25112

[Wrenna Robson]

@Kevin Buzzard especially would like your opinion on this give you were asking for it.

[Wrenna Robson]

@Jz Pan What Kevin was saying here was that he could do it but that API would make it more beautiful (I agree). #mathlib4 > Units.prod, Units.fst, Units.snd @ 💬

[Kevin Buzzard]

I am swayed by Eric's

Eric Wieser said:

Arguably this is a deliberate decision; it reduces the amount of API we have to maintain, and the number of lemmas we have to write that just duplicate API about the equivalence

message enough to make me wonder whether we should just stick to what we have.

[Wrenna Robson]

I personally think it's worth it - having just been editing one of the only places it's used, having these defined was extremely nice.

[Wrenna Robson]

Arguably I suppose whether you define the equivalence first and then create synonyms of its projections.

[Wrenna Robson]

But then we wouldn't have the inl and inr as noted above.

[Wrenna Robson]

The equivalence now becomes
def prodUnits : (M × N)ˣ ≃* Mˣ × Nˣ := (fst.prod snd).toMulEquiv prod rfl rfl

[Wrenna Robson]

Wheras the non-predefined version would look like this:

def prodUnits : (M × N)ˣ ≃* Mˣ × Nˣ :=
  ((Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N))).toMulEquiv
  (MonoidHom.toHomUnits (MonoidHom.prodMap (Units.coeHom M) (Units.coeHom N))) rfl rfl

[Eric Wieser]

Well, you can compress that to

def prodUnits : (M × N)ˣ ≃* Mˣ × Nˣ :=
  ((Units.map (.fst M N)).prod (Units.map (.snd M N))).toMulEquiv
  ((Units.coeHom M).prodMap (Units.coeHom N)).toHomUnits rfl rfl

[Wrenna Robson]

I mean I don't disagree and that's sort of nicer but it isn't very readable. Either way I think giving names to the projections is good.

[Eric Wieser]

I think that's a nicer definition that the current definition, but I don't think it's a good idea to define Units.snd as Units.map (.snd _ _)

[Eric Wieser]

Do we really want to define a (fst, snd, proj, ...) for every type that defines a map?

[Wrenna Robson]

Units one could argue is often a bit clunkier without extra API (or so I have found in the past).

[Eric Wieser]

Any more so than ULift or MulOpposite or QuotientGroup or ... ?

[Wrenna Robson]

No, fair.

[Wrenna Robson]

If one could automate it I'd say do that.

[Eric Wieser]

Even then, the user still has to decide whether to unfold Units.fst to work with theorems about map

[Wrenna Robson]

True, though I would say "ideally not" if you write the API well enough.

[Eric Wieser]

So do you copy the entire API around map too? fst.comp (map f) = map (f \comp fst), (map f).comp fst = map (fst \comp f), ...?

[Eric Wieser]

(maybe this is a straw man because docs#Units.map has no API to begin with...)

[Wrenna Robson]

Well it has a little... but yeah. IDK!

[Wrenna Robson]

def fst : (M × N)ˣ →* Mˣ := (MonoidHom.fst _ _).comp prodUnits.toMonoidHom

def snd : (M × N)ˣ →* Nˣ := (MonoidHom.snd _ _).comp prodUnits.toMonoidHom

[Wrenna Robson]

So if you did use the nice definition above, this is what defining them in terms of projections would mean.

[Wrenna Robson]

Don't have a nice definition of inl and inr, of course.

[Wrenna Robson]

Obviously you then also have
def prod : Mˣ × Nˣ →* (M × N)ˣ := prodUnits.symm.toMonoidHom

[Wrenna Robson]

Oh the other nice thing about having Units.fst and Units.snd is that you can use projection notation: u.fst etc.

[Wrenna Robson]

Hrrm.

[Wrenna Robson]

I have what looks like a diamond issue here.

[Wrenna Robson]

theorem coprod_inl_inr : MonoidHom.coprod (inl (M := M)) (inr (N := N)) =
    prodUnits.symm.toMonoidHom := sorry

[Wrenna Robson]

Error:

[Wrenna Robson]

type mismatch
  prodUnits.symm.toMonoidHom
has type
  @MonoidHom (?m.55835ˣ × ?m.55836ˣ) (?m.55835 × ?m.55836)ˣ Prod.instMulOneClass
    instMulOneClass : Type (max ?u.55833 ?u.55834)
but is expected to have type
  @MonoidHom (?m.53414 × ?m.53415) ?m.53416 Prod.instMulOneClass
    Monoid.toMulOneClass : Type (max (max ?u.53412 ?u.53413) ?u.53411)

[Wrenna Robson]

Oh it might be because I don't have CommMonoid...

[Wrenna Robson]

This may not even be true. Anyway!

[Wrenna Robson]

Basically in general this is: if you haveprodEquiv : T (M × N) ≃ T M × T N, maybe with some extra structure preservation, then do you want the projection T (M × N) -> T M to be called fst?

[Wrenna Robson]

(Where T, I guess, is some operator like Units, AddOpposite, etc.)

[Wrenna Robson]

(and add snd, prod, etc., to taste).

[Eric Wieser]

What if T is the composition of two operators?

[Wrenna Robson]

Then you don't, I guess.

[Wrenna Robson]

I think there's a tension here between usability and maintenace burden that I don't feel qualified to opine on.

[Wrenna Robson]

But I think the neater definition of the equiv (and moving its namespace) at the very least are good ideas.

[Yakov Pechersky]

Eric, are you asking, basically, how much should we lemma-tize functoriality?

[Eric Wieser]

I think I'm more generally advocating against breaking a big bundled object into smaller ones, unless the object is heavily used (eg the work to do precisely this for WithLp.equiv)

[Wrenna Robson]

I think I am quite pro- breaking up when convenient but I take your point about needing a consistent approach. I do instinctively feel Units is Notably A Pain but I can't entirely justify this.

[Yakov Pechersky]

If one approaches it from the "functorial" perspective, how does one show that the functor Units from CommMon_ to CommGrp_ preserves (co)products? Wouldn't one have to provide the homs here as witnesses?

[Wrenna Robson]

I think I find that fairly compelling. As an aside (but related): Units.map could do with better API. Honestly I think if it had it that might actually render this somewhat redundant. Similarly I have to say I don't see why Prod.map_apply' is not in the simp set but Prod.map_apply is.

[Wrenna Robson]

I am going to look at a PR for Units.map improvements.

[Eric Wieser]

PRs adding new theorems for existing definitions are generally much easier to review than PRs adding new definitions :)

[Wrenna Robson]

Indeed!

[Wrenna Robson]

Alright, I think in the end I can't see a nicer way of defining Units.map unless one were to use, say, Invertible, which doesn't seem to be the general style.

[Wrenna Robson]

And I am finding that fst, snd, etc. have utility - they are just nice, it is good to get access to these constructions easily.

[Wrenna Robson]

I do note that we seem to lack Invertible.prod.

[Wrenna Robson]

Oh: idealProdEquiv is a good example of somewhere where we do something fairly similar to this, and there we absolutely do define fst, snd, and prod.

[Wrenna Robson]

So I really am convinced this API would be good and not redundant.