is_subgroup H G

Stream: Is there code for X?

[Vasily Nesterov]

Hello! Suppose that one have, for example, a group G and its subgroup H in a mathematical sense, but both G and H have type Type. For example we can define special linear group as

def SL (n : Type u) (R : Type v) := {x : GL n R // x.det = 1}

I think it would be convenient to have class denoting that one type can be considered as a subgroup of another. Maybe something like this:

class is_subgroup (H : Type) (G : Type) [group G] [h : has_coe H G] :=
  (coe_inj : ∀ x y : H, (x : G) = (y : G) → x = y)
  (mem_1 : ∃ x : H, ↑x = (1 : G))
  (mem_mul : ∀ x y : H, ∃ z : H, (x : G) * (y : G) = (z : G))
  (mem_inv : ∀ x : H, ∃ y : H, (x : G) * (y : G) = 1)

I haven't found this in mathlib. Is there a way to do this using an existing subgroup class or some other convenient way?

[Adam Topaz]

There is docs#has_coe_to_sort for docs#subgroup so you can use terms of subgroup G as if they were types themselves (you get the subtype associated to the carrier set). So you could define your SL as a term of subgroup (GL n R).

[Adam Topaz]

Alternatively, you can work with injective morphisms of groups

[Junyan Xu]

For arbitrary (not necessarily injective) coercion you may use #17048

[Vasily Nesterov]

Thank you for the tips! I once again looked through what there is about this in mathlib, but some questions are still open. In this case objects such as GL and SL are already defined, and I do not want to change them by define SL as a subgroup of GL and then use coercion to Sort.
Another approach is to use coe_is_monoid_hom, but this requires H to already be a group, and I think it would be more natural to prove that H is a group from the is_subgroup H G as in subgroup.to_group.

So my question is: assume that I have class is_subgroup as described above. I can define the function

def subgroup_of_type {G : Type} [group G] (H : Type) [has_coe H G] [is_subgroup H G] : subgroup G := sorry

which take the type H and produce the corresponding object of type subgroup G. But is it possible to mark this as a coercion? Something like a "dependent" coercion.

[Junyan Xu]

You can easily construct a monoid_hom H →* G from your is_subgroup H G, then you can take docs#monoid_hom.range

[Junyan Xu]

But I think docs#matrix.special_linear_group.group should probably be made a subgroup.

[Junyan Xu]

But is it possible to mark this as a coercion? Something like a "dependent" coercion.

You want H : Type be coerced to subgroup_of_type H : subgroup G? That seems pretty strange and I don't think Lean can infer G.

[Eric Wieser]

Junyan Xu said:

But I think docs#matrix.special_linear_group.group should probably be made a subgroup.

A subgroup of what? units (matrix n n R)?

[Junyan Xu]

Oh I see special_linear_group is currently a subtype of matrix n n R which may be easier to work with than unit (matrix n n R).