subgroups of a monoid

Stream: mathlib4

[Kevin Buzzard]

Why does Subgroup eat a group rather than a monoid? This came up in FLT-related work, because some Imperial students want to talk about maximal subfields of a K-algebra D where D is not a field (or even a division ring). They can't use docs#IntermediateField because this wants to eat fields. I realised that this convention stretches right down to the basics.

[Yury G. Kudryashov]

Workaround: you can use Subgroup (Units M)

[Yury G. Kudryashov]

If you want ⁻¹ on the subgroup to be defeq to the restriction of ⁻¹ on the original group (in case of groups), then you have to assume Group G.

[Kevin Buzzard]

This workaround does not work for intermediate fields (as subfields of a noncommutative ring) as there is no "maximal commutative subring" of a non-commutative ring.

[Oliver Nash]

I just encountered this independently. Any thoughts on the following possible design:

import Mathlib

variable (G : Type*)

-- Candidate replacement for `Subgroup`
structure Subgroup' [Monoid G] extends Submonoid G where
  inv_mem' {x} : x ∈ carrier → ∃ y ∈ carrier, x * y = 1

namespace Subgroup'

instance [Monoid G] : SetLike (Subgroup' G) G where
  coe s := s.carrier
  coe_injective' := sorry

-- Only define instance when ambient is a `Group`
instance instInvOfGroup [Group G] (H : Subgroup' G) : Inv H where
  inv h := ⟨(h : G)⁻¹, by sorry⟩

/-- Not an instance because we want good defeq properties of `instInvOfGroup` when have ambient
`Group` etc. -/
noncomputable def inv [Monoid G] (H : Subgroup' G) : Inv H where
  inv h := ⟨(H.inv_mem' (x := h) h.property).choose, (H.inv_mem' (x := h) h.property).choose_spec.1⟩

-- Usual API etc

end Subgroup'

[Kenny Lau]

@Oliver Nash I think you basically want an "IsGroup" typeclass on groups, and then Subgroup' is just Submonoid + IsGroup

[Kenny Lau]

I've heard that we also need similar things for subfields of a ring, and that we're stuck on this front for some reason

[Oliver Nash]

I don't quite see that IsGroup is what I want here (though perhaps it is).

The issue I see (highlighted by Yury above) is that Group carries the data of the inverse function and so when defining the inverse for a Subgroup we want to use this same data for definitional convenience. I don't see how a Prop-valued typeclass (which is what I understand by IsGroup) can control the definitional property in the way that we seek.

[Aaron Liu]

Make it a subgroup of the units

[Oliver Nash]

Indeed this is what is possible today but it's not quite as convenient as I'd like. Sadly I must now disappear to join a call!

[Aaron Liu]

I guess this only works because forget (Group -> Monoid) has a right adjoint

[Eric Wieser]

Oliver Nash said:

/-- Not an instance because we want good defeq properties of `instInvOfGroup` when have ambient
`Group` etc. -/

this will become painful when you have the same comment on DivInvMonoid and Group and CommGroup

[Kenny Lau]

Oliver Nash said:

definitional property

but there is no defintional property in your code above, since everything is noncomputable

[Kenny Lau]

your inv_mem' is a Prop already