Submonoid formed by the units

Stream: Is there code for X?

[Xavier Xarles]

Given a Monoid, how can one construct the Submonoid formed by the elements that have inverse? The Units are not a Submonoid, but something else...

[Yaël Dillies]

cc @Wrenna Robson

[Wrenna Robson]

So I think this is (\top : Submonoid M).units.ofUnits

[Wrenna Robson]

Or equivalently, actually, (\top : Subgroup M\times).ofUnits

[Wrenna Robson]

(not on pc, can't add proper symbols)

[Wrenna Robson]

But given a subgroup of units, ofUnits gives you the corresponding submonoid, and you want the subgroup of all units.

[Wrenna Robson]

If you want the subgroup of units corresponding to a given submonoid, that's what Submonoid.units is for

[Eric Wieser]

Is this also Units.coeHom.mrange?

[Wrenna Robson]

Well that's as a set, but yeah I think so

[Eric Wieser]

docs#MonoidHom.mrange disagrees with you

[Wrenna Robson]

Oh lol

[Wrenna Robson]

Then yes

[Eric Wieser]

Whoops, I meant mrange

[Wrenna Robson]

Ahhhhh

[Wrenna Robson]

Yeah

[Eric Wieser]

But range is a subgroup, not a set

[Wrenna Robson]

Yeah ofUnits is essentially just the image of coeHom so that sounds correct

[Xavier Xarles]

How do you feel about adding something like this in the Mathlib.GroupTheory.Submonoid.Units?

import Mathlib.GroupTheory.Submonoid.Units

variable {M : Type*}
variable [CommMonoid M]

theorem mem_ofUnits_of_top_iff_isUnit (x:M) :  x ∈ Subgroup.ofUnits ⊤ ↔ IsUnit x := by
  rw [Subgroup.mem_ofUnits_iff_exists_isUnit]
  exact exists_iff_of_forall fun _ => trivial

[Wrenna Robson]

Yeah we should probably have that.

[Wrenna Robson]

I'm wondering if there's any other analogous things that need adding

[Wrenna Robson]

We have one direction of it, it seems

[Wrenna Robson]

Subgroup.isUnit_of_mem_ofUnits

[Wrenna Robson]

Ah.

[Wrenna Robson]

And Subgroup.mem_ofUnits_of_isUnit_of_unit_mem is the other direction

[Wrenna Robson]

Or is once you consider everything is mem_top

[Wrenna Robson]

But your proof is also good

[Wrenna Robson]

Oh! Also, answering your original question again: it's also IsUnit.submonoid

[Wrenna Robson]

The table at the top of Submonoid/Units would say this, if it worked

[Wrenna Robson]

Yeah if you want the units as a submonoid of a monoid, use IsUnit.submonoid

[Wrenna Robson]

If you want the units as a submonoid of the monoid in which a submonoid lies, then that is S.units.ofUnits

[Wrenna Robson]

I guess Subgroup.ofUnits \top = IsUnit.submonoid M might be useful to have!

[Wrenna Robson]

Subgroup.ofUnits_top

[Wrenna Robson]

Yes, I think that would be good to have. We could also have the lemma you mention, which is naturally a consequence

[Xavier Xarles]

I don't like the proof, but something like this?

import Mathlib.GroupTheory.Submonoid.Units

variable {M : Type*}[CommMonoid M]

theorem Subgroup.ofUnits_top : Subgroup.ofUnits ⊤ = IsUnit.submonoid M := by
  refine Submonoid.ext ?h
  simp_rw [IsUnit.mem_submonoid_iff,Subgroup.mem_ofUnits_iff_exists_isUnit]
  exact fun x => exists_iff_of_forall fun _ => trivial

[Wrenna Robson]

Yes, precisely.

[Eric Wieser]

A shorter proof:

import Mathlib.GroupTheory.Submonoid.Units

variable {M : Type*} [Monoid M]

theorem Units.mrange_coeHom : MonoidHom.mrange (Units.coeHom M) = IsUnit.submonoid M := rfl

theorem Subgroup.ofUnits_top : Subgroup.ofUnits ⊤ = IsUnit.submonoid M := (MonoidHom.mrange_eq_map _).symm

[Wrenna Robson]

Very nice

[Wrenna Robson]

Units.mrange_coeHom wants to be in a different file

[Xavier Xarles]

I really don't get how can the proof be so shorter, and using a result that doesn't seem related...

[Wrenna Robson]

Well, ofUnits is by definition (coeHom M).map

[Wrenna Robson]

So the LHS is map, by definition. And it turns out in fact IsUnit.submonoid is defeq to mrange

[Wrenna Robson]

That's more surprising maybe

[Wrenna Robson]

Oh this does mean that Submonoid.units (IsUnit.submonoid M) = \top as well

[Wrenna Robson]

If we don't have that too, we should

[Wrenna Robson]

call it Submonoid.units_isUnit_eq_top or something

[Wrenna Robson]

(it's an immediate consequence of the above, given the Galois insertion)

[Wrenna Robson]

@Yaël Dillies how do I say "the lattice of subgroups of units is equivalent to the lattice of submonoids contained in IsUnit.subMonoid, with the units/ofUnits Galois Coinsertion defining the maps across"?

[Yaël Dillies]

Subgroup (Units M) o~= {s : Submonoid M // s <= IsUnit.submonoid}?

[Wrenna Robson]

Cool! I don't know if we tend to have theorems like that.

[Yaël Dillies]

Probably we have at least one direction

[Eric Wieser]

Isn't that just a special case of Subgroup M o~= {s : Submonoid N // s <= mrange f} or similar?

[Wrenna Robson]

Hmm, perhaps!

[Wrenna Robson]

Is that true for arbitrary f?

[Wrenna Robson]

ofUnits is just map, but units needed a little more to it, so it would seem surprising to me if it came out of that.

[Xavier Xarles]

It seems that we don't have

import Mathlib.Algebra.Group.Units

variable {M:Type*}

lemma IsUnit.exists_inv [Monoid M] {a : M}(h : IsUnit a) :
    ∃ b, (a * b = 1) ∧ (b * a = 1) := by
  rcases h with ⟨⟨a, b, hab,hba⟩, rfl⟩
  exact ⟨b, ⟨ hab, hba⟩⟩

theorem isUnit_iff_exists [Monoid M] {a : M} : IsUnit a ↔
    ∃ b, (a * b = 1) ∧ (b * a = 1) :=
  ⟨fun h => IsUnit.exists_inv h , fun ⟨b, hab,hba⟩ => by use ⟨_, b, hab,hba⟩ ⟩

[Eric Wieser]

I think that's probably because you never need those lemmas

[Xavier Xarles]

May be. Although I discovered because I need them...

[Eric Wieser]

It's usually more convenient to keep a Unit around than to unpack it into the val and inv

[Xavier Xarles]

In fact I need the other way: if I have such a b, then a is a Unit.

[Eric Wieser]

Can you share your context?

[Damiano Testa]

There are results around docs#isUnit_iff_exists_inv

[Jireh Loreaux]

If you actually have a b, you can easily just build a term of Units directly, and even use the lift tactic to turn a itself into a unit.

[Junyan Xu]

IsUnit a ↔ (∃ b, a * b = 1) ∧ (∃ c, c * a = 1) is probably more useful ...

[Wrenna Robson]

Why?

[Junyan Xu]

It's not just a rephrasing of the definition (i.e. you can't get it by permuting arguments of the constructors), instead you need associativity to prove the reverse direction.

[Xavier Xarles]

So, how do you feel about this result?

import Mathlib.GroupTheory.Submonoid.Units
variable {M : Type*} [Monoid M]

theorem isUnit_iff_exists_both_units  (a:M): IsUnit a ↔ (∃ b, a * b = 1) ∧ (∃ c, c * a = 1):= by
constructor <;> intro h
· rcases h with ⟨⟨a, b, hab,hba⟩, rfl⟩
  exact ⟨Exists.intro b hab, Exists.intro b hba⟩
· let ⟨b,hab⟩ := h.1
  let ⟨c,hca⟩ := h.2
  have beqc: b = c:= by
    calc
      b = 1*b := (one_mul b).symm
      _ = (c*a)*b := congrFun (congrArg HMul.hMul (id hca.symm)) b
      _ = c*(a*b) := mul_assoc c a b
      _ = c*1:= congrArg (HMul.hMul c) hab
      _ = c := mul_one c
  rw [←beqc] at hca
  use ⟨_, b, hab,hca⟩

[Wrenna Robson]

Junyan Xu said:

It's not just a rephrasing of the definition (i.e. you can't get it by permuting arguments of the constructors), instead you need associativity to prove the reverse direction.

Hmm. Yeah I suppose it being both directions is the interesting bit.

[Wrenna Robson]

Xavier Xarles said:

So, how do you feel about this result?

import Mathlib.GroupTheory.Submonoid.Units
variable {M : Type*} [Monoid M]

theorem isUnit_iff_exists_both_units  (a:M): IsUnit a ↔ (∃ b, a * b = 1) ∧ (∃ c, c * a = 1):= by
constructor <;> intro h
· rcases h with ⟨⟨a, b, hab,hba⟩, rfl⟩
  exact ⟨Exists.intro b hab, Exists.intro b hba⟩
· let ⟨b,hab⟩ := h.1
  let ⟨c,hca⟩ := h.2
  have beqc: b = c:= by
    calc
      b = 1*b := (one_mul b).symm
      _ = (c*a)*b := congrFun (congrArg HMul.hMul (id hca.symm)) b
      _ = c*(a*b) := mul_assoc c a b
      _ = c*1:= congrArg (HMul.hMul c) hab
      _ = c := mul_one c
  rw [←beqc] at hca
  use ⟨_, b, hab,hca⟩

It feels like in many ways we should have a defined predicate for "IsLeftUnit" but it's good.

[Eric Wieser]

That golfs to

theorem isUnit_iff_exists_both_units  (a : M) : IsUnit a ↔ (∃ b, a * b = 1) ∧ (∃ c, c * a = 1):= by
  constructor
  · rintro ⟨⟨a, b, hab, hba⟩, rfl⟩
    exact ⟨⟨b, hab⟩, ⟨b, hba⟩⟩
  · rintro ⟨⟨b, hab⟩, ⟨c, hca⟩⟩
    suffices b = c from ⟨⟨a, b, hab, this ▸ hca⟩, rfl⟩
    calc
      b = 1*b := (one_mul b).symm
      _ = (c*a)*b := congrArg (· * b) hca.symm
      _ = c*(a*b) := mul_assoc c a b
      _ = c*1 := congrArg (c * ·) hab
      _ = c := mul_one c

[Damiano Testa]

Or you could use regular elements:

theorem isUnit_iff_exists_both_units  (a : M) : IsUnit a ↔ (∃ b, a * b = 1) ∧ (∃ c, c * a = 1):= by
  constructor
  · rintro ⟨⟨a, b, hab, hba⟩, rfl⟩
    exact ⟨⟨b, hab⟩, ⟨b, hba⟩⟩
  · rintro ⟨⟨b, hab⟩, ⟨c, hca⟩⟩
    suffices b = c from ⟨⟨a, b, hab, this ▸ hca⟩, rfl⟩
    have : IsRegular a := ⟨isLeftRegular_of_mul_eq_one ‹_›, isRightRegular_of_mul_eq_one ‹_›⟩
    exact this.right (this.left (by simp [← mul_assoc, *]))

[Kevin Buzzard]

You can also use docs#left_inv_eq_right_inv

[Kevin Buzzard]

This is the only interesting theorem I know about monoids :-)