Pi.unitEquiv

Stream: Is there code for X?

[Wrenna Robson]

import Mathlib.Algebra.Group.Pi

def Pi.unitsEquiv [Monoid β] : (α → β)ˣ ≃* (α → βˣ) where
  toFun f a := ⟨(f : α → β) a, ((f⁻¹ : (α → β)ˣ) : α → β) a,
    by simp_rw [← Pi.mul_apply (f.1), Units.mul_inv, Pi.one_apply],
    by simp_rw [← Pi.mul_apply ((f⁻¹ : (α → β)ˣ) : α → β), Units.inv_mul, Pi.one_apply]⟩
  invFun f := ⟨(↑) ∘ f, (↑) ∘ f⁻¹,
    by simp_rw [Pi.mul_def, Function.comp_apply, Pi.inv_apply, Units.mul_inv, Pi.one_def],
    by simp_rw [Pi.mul_def, Function.comp_apply, Pi.inv_apply, Units.inv_mul, Pi.one_def]⟩
  left_inv f := by ext ; simp only [Units.inv_eq_val_inv, Function.comp_apply]
  right_inv f := by ext ; simp only [Units.inv_eq_val_inv, Function.comp_apply]
  map_mul' f g := by ext ; simp only [Units.val_mul, Pi.mul_apply]

I am right in saying we don't have this, right? Any reason we couldn't?

[Eric Wieser]

Golfed:

def Pi.unitsEquiv [Monoid β] : (α → β)ˣ ≃* (α → βˣ) where
  toFun f a := ⟨(f : α → β) a, ((f⁻¹ : (α → β)ˣ) : α → β) a, congr_fun f.mul_inv a, congr_fun f.inv_mul a⟩
  invFun f := ⟨(f ·), (f⁻¹ ·), funext (f · |>.mul_inv), funext (f · |>.inv_mul)⟩
  left_inv _ := Units.ext <| funext fun _ => rfl
  right_inv _ := funext fun _ => Units.ext rfl
  map_mul' _ _ := funext fun _ => Units.ext rfl

[Yaël Dillies]

That's a neat statement! I would call it MulEquiv.unitsPi, however.

[Eric Wieser]

We should have the Prod version too

[Wrenna Robson]

Thanks Eric. By the Prod version, what do you mean?

[Yaël Dillies]

(α × β)ˣ ≃* αˣ × βˣ

[Wrenna Robson]

#docs MulEquiv.prodUnits

[Wrenna Robson]

Err, I can't remember how to do that right. But we have it!

[Yaël Dillies]

docs#MulEquiv.prodUnits

[Yaël Dillies]

Damn, I guessed the name right :sweat_smile:

[Wrenna Robson]

should probably be MulEquiv.piUnits or MulEquiv.arrowUnits (I think the former?)

[Yaël Dillies]

Ah no, not quite. I swapped Pi and Units.

[Yaël Dillies]

Also, you should prove the dependent type version.

[Eric Wieser]

Yaël Dillies said:

docs#MulEquiv.prodUnits

I'll stop trying to prove it then!

[Wrenna Robson]

There will be a dependent-Pi and dependent-Sigma version, presumably.

[Yaël Dillies]

What's a disjoint sum of monoids? :monocle:

[Wrenna Robson]

I don't know, some nonsense.

[Eric Wieser]

So:

@[simps]
def MulEquiv.piUnits {β : α → Type*} [∀ a, Monoid (β a)] : (∀ a, β a)ˣ ≃* (∀ a, (β a)ˣ) where
  toFun f a := ⟨f.val a, f.inv a, congr_fun f.mul_inv a, congr_fun f.inv_mul a⟩
  invFun f := ⟨(f ·), (f⁻¹ ·), funext (f · |>.mul_inv), funext (f · |>.inv_mul)⟩
  left_inv _ := Units.ext <| funext fun _ => rfl
  right_inv _ := funext fun _ => Units.ext rfl
  map_mul' _ _ := funext fun _ => Units.ext rfl

[Wrenna Robson]

I would imagine it also works if you are pulling α though an Equiv.

[Eric Wieser]

That's a different equiv though

[Wrenna Robson]

Right, yes.

[Eric Wieser]

Which is to say, it's easy to build by composing with the one above

[Adam Topaz]

Yaël Dillies said:

What's a disjoint sum of monoids? :monocle:

Do you mean the coproduct? That exists, but the functor sending a monoid to its unit group is a right adjoint so it preserves limits, not colimits (which coproducts are).

[Wrenna Robson]

What's the corresponding left adjoint?

[Adam Topaz]

The forgetful functor

[Adam Topaz]

If G is a group and M is a monoid then the Homs from G to M are the same as the Homs from G to the units of M

[Kevin Buzzard]

It might still be true that units of coproduct is coproduct of units. What's definitely not true is that units of quotient (another colimit) is quotient of units, as $(\Z/N\Z)^*$ is generally bigger than the image of the units of $\Z$.

[Adam Topaz]

You're right, it might be true, but if so, it would be "by accident".

[Adam Topaz]

In any case, do we even have the free product of two (or more) monoids in mathlib?

[Adam Topaz]

I guess we do docs#Monoid.CoprodI

[Kevin Buzzard]

I have this picture in my head. It goes like this. I have a collection of monoids M_i for i in some index set I, then an element of their coproduct is just represented by a list of elements in these monoids with the property that two adjacent elements of the list can't come from the same M_i and none of them are 1 (you identify all the 1s into one term, the empty list). You multiply these things together in the obvious way (remove 1s and merge two terms in the same M_i). With this model, units of coproduct = coproduct of units just feels completely obvious; the map from the coproduct of the units into the (units of the) coproduct is obviously injective because it's the same picture, and is obviously surjective onto the units because if you've got an list of monoid elements and you times it by another list of monoid elements and the product becomes the empty list then just look at what happened, it's obvious everything in sight was a unit because there's nowhere else to go but 1 so you inverted it. In a lecture I might be tempted to write down the model and then claim that the result was an "easy exercise" and say no more about it. But Adam points out that this isn't a freebie via some category theory magic wand, and looking at the above proof it would I imagine be quite a challenge to formalise.

[Kevin Buzzard]

Aw crap I bet I'm assuming commutativity ;-) Sorry, that's my world :-/ OK I'm only claiming the above for commutative monoids, I'm not sure I understand units properly in the non-commutative case, I can have xy=1 without yx=1 in that case :-/