Multiplicative subgroups of a ring

Stream: maths

[Adam Topaz]

Suppose that $A$ is a (semi)ring. Does anyone have any thoughts about how we might teach lean about the multiplicative subgroups of $A^\times$? Of course, we could just work with subgroup A\^x, but for many applications it would be nice to be able to write $a \in H$ for such a multiplicative subgroup.

We could define mul_subgroup A := subgroup A\^x with a different has_mem instance.
We could also define mul_subgroup A as a bespoke structure with a carrier : set A field and various assumptions.

Thoughts? Ideas?

[Yaël Dillies]

Could you generalize docs#subgroup to not require working over a group?

[Adam Topaz]

(You could take $A$ to be any monoid in the above)

[Adam Topaz]

@Yaël Dillies I'm not sure what you mean...

[Yaël Dillies]

Replace the [group G] assumption by [has_mul G] [has_one G] and find a way to rephrase docs#subgroup.inv_mem' without referring to ⁻¹.

[Adam Topaz]

How would you do that?

[Yaël Dillies]

Something like ∀ a b, a * b = 1 → a ∈ carrier → b ∈ carrier. The problem with this approach is that your subgroups don't inherit any inverse from G, precisely because G doesn't have any...

[Adam Topaz]

I guess you could say "for all elements which are units, and are members of the carrier, their inverses are members of the carrier"

[Reid Barton]

But that's not what you want, you want "has an inverse which is also a member"

[Yaël Dillies]

Maybe you can then define a⁻¹ for a : H : subgroup G as ↑a.to_unit where we need to define subgroup.unit appropriately.

[Adam Topaz]

Oops! yeah of course

[Yaël Dillies]

Oh right, Reid. You should also add ∀ a ∈ carrier, is_unit a, or carrier → units G.

[Yaël Dillies]

Do we care about definitional equality here? If we define the inverse of elements of subgroups using Gˣ, we lose the defeq ↑a⁻¹ = (↑a)⁻¹, but that's not one you were gonna have with your mul_subgroup either.

[Adam Topaz]

We could arrange to have good defeq properties.

[Yaël Dillies]

At any rate, I value not duplicating the subgroup API over defeq properties.

[Eric Wieser]

This sounds a bit like a previous discussion about subfields of (noncommutative) rings

[Adam Topaz]

Yeah, it's a very similar discussion. How did that resolve?

[Jireh Loreaux]

I'll just point out that this discussion may be relevant even for docs#unitary as a special case.

[Yury G. Kudryashov]

If we define subgroup G to be old_subgroup Gˣ, then we won't need classical.choice for simple facts about subgroups.

[Yury G. Kudryashov]

This is a pro compared to the is_unit approach.