Monoid isomorphisms preserve the lattice of submonoids

Stream: Is there code for X?

[Michał Mrugała]

Is this in mathlib?

import Mathlib.Algebra.Group.Subgroup.Ker

namespace Subgroup
variable {G H : Type*} [Group G] [Group H]

@[to_additive]
def congr (e : G ≃* H) : Subgroup G ≃o Subgroup H where
  toFun := comap e.symm
  invFun := comap e
  left_inv _ := by simp [comap_comap]
  right_inv _ := by simp [comap_comap]
  map_rel_iff' {_ _} := comap_le_comap_of_surjective e.symm.surjective

end Subgroup

[Aaron Liu]

docs#MulEquiv.mapSubgroup and docs#MulEquiv.comapSubgroup.
We don't have the additive version.

[Kevin Buzzard]

attribute [to_additive] MulEquiv.mapSubgroup
attribute [to_additive] MulEquiv.comapSubgroup

creates them.

[Michał Mrugała]

We will PR that :+1:

[Kevin Buzzard]

Thanks! You can just put @[to_additive] before the declarations rather than adding the attributes later.

[Aaron Liu]

Don't forget to change the docstrings too! So something like

@[to_additive (attr := simps)
    "An isomorphism of additive groups gives an order isomorphism between
    the lattices of subgroups, defined by sending subgroups to their forward images.

    See also `AddEquiv.comapAddSubgroup` which maps subgroups to their inverse images."]