Abelian Subgroup

Stream: maths

[Thomas Browning]

In mathlib, what's the best way to say "H is an abelian subgroup of G"? I don't think that {G : Type*} [group G] {H : subgroup G} [comm_group H] works, since the comm_group H instance won't match the group H instance.

[Adam Topaz]

You may have to write out the commutativity condition, unfortunately

[Thomas Browning]

I do want a comm_group H instance eventually, so would I then have to manually produce it?

[Johan Commelin]

I guess we need a predicate subgroup.is_comm (maybe a def, maybe a class). And then we can have a def/instance of comm_group H under that assumption.

[Adam Topaz]

Commutativity should probably just be a mixin anyway

[Eric Wieser]

Does docs#subgroup.normal mean commutative?

[Johan Commelin]

Nope

[Johan Commelin]

Every subgroup of a commutative group is normal, but not every normal subgroup is commutative.

[Johan Commelin]

Example: A_n is a normal subgroup of S_n since it is the kernel of the sign map S_n -> Z/2 that maps a permutation to it's sign. But for n > 3, the subgroup A_n is not commutative.

[Eric Wieser]

You could probably add a new instance [group G] (S : subgroup G) [h : is_commutative S (*)] : comm_group S := { mul_comm := h.comm, ..S.to_group } instance

[Eric Wieser]

Then your lemma would assume docs#is_commutative instead of comm_group S.

[Johan Commelin]

Which could be a special case of a def [group G] [is_commutative G (*)] : comm_group G :=

[Johan Commelin]

But that one shouldn't be an instance because of loops. For S : subgroup G it's not a problem.

[Eric Wieser]

I'm not sure the def is useful since it's basically just one line to implement, and you have to remember to make it reducible if it's a def

[Yaël Dillies]

Actually any group is normal to itself, but clearly not all groups are abelian.

[Johan Commelin]

ooh lol, that's a lot simpler

[Eric Wieser]

Eric Wieser said:

You could probably add a new instance [group G] (S : subgroup G) [h : is_commutative S (*)] : comm_group S := { mul_comm := h.comm, ..S.to_group } instance

This forms a loop, don't do this!

-- deep recursion was detected at 'expression equality test'
instance {R : Type*} [group R] (S : subgroup R) : comm_group S := by apply_instance