Group isomorphism gives an order isomorphism on subgroups

Stream: Is there code for X?

[Kim Morrison]

import Mathlib
variable (G :Type*) [Group G] (H : Type*) [Group H]

example (f : G ≃* H) : Subgroup G ≃o Subgroup H := sorry

[Kevin Buzzard]

Didn't you write a tactic to do this once? ;-)

[Eric Wieser]

example (f : G ≃* H) : Subgroup G ≃o Subgroup H where
  toFun := Subgroup.map f
  invFun := Subgroup.map f.symm
  left_inv sg := by simp [Subgroup.map_map]
  right_inv sh := by simp [Subgroup.map_map]
  map_rel_iff' {sg1 sg2} :=
    ⟨fun h => by simpa [Subgroup.map_map] using
      Subgroup.map_mono (f := (f.symm : H →* G)) h, Subgroup.map_mono⟩

[Eric Wieser]

I can't find it for any subobjects

[Kim Morrison]

Thanks Eric!

[Junyan Xu]

There's docs#Submodule.orderIsoMapComap
and more examples, though most are not about the same type of subobjects:
@loogle Submodule, OrderIso

[loogle]

:search: AddSubgroup.toIntSubmodule, AddSubmonoid.toNatSubmodule, and 32 more

[Kevin Buzzard]

I would have been tempted to use Subgroup.comap because it's better definitionally...

[Kim Morrison]

Yes, I'd already made that change locally. Note however that the function Junyan found above uses map for the forward direction and comap for the backward direction, thereby avoiding mentioning f.symm directly. Not sure what will turn out best.

[Kevin Buzzard]

I would have used comap in both directions :-)

[Kevin Buzzard]

import Mathlib.Tactic

variable (G H : Type*) [Group G] [Group H]

example (f : G ≃* H) : Subgroup G ≃o Subgroup H where
  toFun := Subgroup.comap f.symm
  invFun := Subgroup.comap f
  left_inv sg := by simp [Subgroup.comap_comap]
  right_inv sh := by simp [Subgroup.comap_comap]
  map_rel_iff' {sg1 sg2} := by
    simpa using Subgroup.comap_le_comap_of_surjective f.symm.surjective

[Kevin Buzzard]

I don't know why simp [Subgroup.comap_le_comap_of_surjective f.symm.surjective] gives the error

application type mismatch
  Subgroup.comap_le_comap_of_surjective (MulEquiv.surjective f.symm)
argument
  MulEquiv.surjective f.symm
has type
  Function.Surjective ⇑f.symm : Prop
but is expected to have type
  Function.Surjective ⇑?m.6925 : Prop

[Andrew Yang]

You need simp [Subgroup.comap_le_comap_of_surjective (f := f.symm.toMonoidHom) f.symm.surjective] because lean cannot figure out the toMonoidHom part on its own without the type signature of the goal as a hint.