Documentation

Mathlib.Algebra.Group.Subgroup.Map

map and comap for subgroups #

We prove results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.

Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.

Main definitions #

Notation used here:

Definitions in the file:

Implementation notes #

Subgroup inclusion is denoted rather than , although is defined as membership of a subgroup's underlying set.

Tags #

subgroup, subgroups

def Subgroup.comap {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (H : Subgroup N) :

The preimage of a subgroup along a monoid homomorphism is a subgroup.

Equations
    Instances For
      def AddSubgroup.comap {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :

      The preimage of an AddSubgroup along an AddMonoid homomorphism is an AddSubgroup.

      Equations
        Instances For
          @[simp]
          theorem Subgroup.coe_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup N) (f : G →* N) :
          (comap f K) = f ⁻¹' K
          @[simp]
          theorem AddSubgroup.coe_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup N) (f : G →+ N) :
          (comap f K) = f ⁻¹' K
          @[simp]
          theorem Subgroup.mem_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {K : Subgroup N} {f : G →* N} {x : G} :
          x comap f K f x K
          @[simp]
          theorem AddSubgroup.mem_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {K : AddSubgroup N} {f : G →+ N} {x : G} :
          x comap f K f x K
          theorem Subgroup.comap_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K K' : Subgroup N} :
          K K'comap f K comap f K'
          theorem AddSubgroup.comap_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K K' : AddSubgroup N} :
          K K'comap f K comap f K'
          theorem Subgroup.comap_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {P : Type u_6} [Group P] (K : Subgroup P) (g : N →* P) (f : G →* N) :
          comap f (comap g K) = comap (g.comp f) K
          theorem AddSubgroup.comap_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (K : AddSubgroup P) (g : N →+ P) (f : G →+ N) :
          comap f (comap g K) = comap (g.comp f) K
          @[simp]
          theorem Subgroup.comap_id {N : Type u_5} [Group N] (K : Subgroup N) :
          @[simp]
          theorem AddSubgroup.comap_id {N : Type u_5} [AddGroup N] (K : AddSubgroup N) :
          @[simp]
          theorem Subgroup.toAddSubgroup_comap {G : Type u_1} [Group G] {G₂ : Type u_7} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) :
          @[simp]
          theorem AddSubgroup.toSubgroup_comap {A : Type u_7} {A₂ : Type u_8} [AddGroup A] [AddGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂) :
          def Subgroup.map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) :

          The image of a subgroup along a monoid homomorphism is a subgroup.

          Equations
            Instances For
              def AddSubgroup.map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :

              The image of an AddSubgroup along an AddMonoid homomorphism is an AddSubgroup.

              Equations
                Instances For
                  @[simp]
                  theorem Subgroup.coe_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (K : Subgroup G) :
                  (map f K) = f '' K
                  @[simp]
                  theorem AddSubgroup.coe_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) :
                  (map f K) = f '' K
                  @[simp]
                  theorem Subgroup.map_toSubmonoid {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (K : Subgroup G) :
                  @[simp]
                  theorem AddSubgroup.map_toAddSubmonoid {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (K : AddSubgroup G) :
                  @[simp]
                  theorem Subgroup.mem_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {y : N} :
                  y map f K xK, f x = y
                  @[simp]
                  theorem AddSubgroup.mem_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {y : N} :
                  y map f K xK, f x = y
                  theorem Subgroup.mem_map_of_mem {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {K : Subgroup G} {x : G} (hx : x K) :
                  f x map f K
                  theorem AddSubgroup.mem_map_of_mem {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {K : AddSubgroup G} {x : G} (hx : x K) :
                  f x map f K
                  theorem Subgroup.apply_coe_mem_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (K : Subgroup G) (x : K) :
                  f x map f K
                  theorem AddSubgroup.apply_coe_mem_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) (x : K) :
                  f x map f K
                  theorem Subgroup.map_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K K' : Subgroup G} :
                  K K'map f K map f K'
                  theorem AddSubgroup.map_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K K' : AddSubgroup G} :
                  K K'map f K map f K'
                  @[simp]
                  theorem Subgroup.map_id {G : Type u_1} [Group G] (K : Subgroup G) :
                  @[simp]
                  theorem AddSubgroup.map_id {G : Type u_1} [AddGroup G] (K : AddSubgroup G) :
                  theorem Subgroup.map_map {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] {P : Type u_6} [Group P] (g : N →* P) (f : G →* N) :
                  map g (map f K) = map (g.comp f) K
                  theorem AddSubgroup.map_map {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (g : N →+ P) (f : G →+ N) :
                  map g (map f K) = map (g.comp f) K
                  @[simp]
                  theorem Subgroup.map_one_eq_bot {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] :
                  map 1 K =
                  @[simp]
                  theorem AddSubgroup.map_zero_eq_bot {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] :
                  map 0 K =
                  theorem Subgroup.mem_map_equiv {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G ≃* N} {K : Subgroup G} {x : N} :
                  theorem AddSubgroup.mem_map_equiv {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G ≃+ N} {K : AddSubgroup G} {x : N} :
                  @[simp]
                  theorem Subgroup.mem_map_iff_mem {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective f) {K : Subgroup G} {x : G} :
                  f x map f K x K
                  @[simp]
                  theorem AddSubgroup.mem_map_iff_mem {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective f) {K : AddSubgroup G} {x : G} :
                  f x map f K x K
                  theorem Subgroup.map_equiv_eq_comap_symm' {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G ≃* N) (K : Subgroup G) :
                  theorem Subgroup.map_equiv_eq_comap_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G ≃* N) (K : Subgroup G) :
                  map (↑f) K = comap (↑f.symm) K
                  theorem AddSubgroup.map_equiv_eq_comap_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G ≃+ N) (K : AddSubgroup G) :
                  map (↑f) K = comap (↑f.symm) K
                  theorem Subgroup.comap_equiv_eq_map_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : N ≃* G) (K : Subgroup G) :
                  comap (↑f) K = map (↑f.symm) K
                  theorem AddSubgroup.comap_equiv_eq_map_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : N ≃+ G) (K : AddSubgroup G) :
                  comap (↑f) K = map (↑f.symm) K
                  theorem Subgroup.comap_equiv_eq_map_symm' {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : N ≃* G) (K : Subgroup G) :
                  theorem Subgroup.map_symm_eq_iff_map_eq {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] {H : Subgroup N} {e : G ≃* N} :
                  map (↑e.symm) H = K map (↑e) K = H
                  theorem AddSubgroup.map_symm_eq_iff_map_eq {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {H : AddSubgroup N} {e : G ≃+ N} :
                  map (↑e.symm) H = K map (↑e) K = H
                  theorem Subgroup.map_le_iff_le_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {H : Subgroup N} :
                  map f K H K comap f H
                  theorem AddSubgroup.map_le_iff_le_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {H : AddSubgroup N} :
                  map f K H K comap f H
                  theorem Subgroup.gc_map_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                  theorem AddSubgroup.gc_map_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                  theorem Subgroup.map_sup {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) :
                  map f (HK) = map f Hmap f K
                  theorem AddSubgroup.map_sup {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) :
                  map f (HK) = map f Hmap f K
                  theorem Subgroup.map_iSup {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ιSubgroup G) :
                  map f (iSup s) = ⨆ (i : ι), map f (s i)
                  theorem AddSubgroup.map_iSup {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ιAddSubgroup G) :
                  map f (iSup s) = ⨆ (i : ι), map f (s i)
                  theorem Subgroup.map_inf {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
                  map f (HK) = map f Hmap f K
                  theorem AddSubgroup.map_inf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective f) :
                  map f (HK) = map f Hmap f K
                  theorem Subgroup.map_iInf {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} [Nonempty ι] (f : G →* N) (hf : Function.Injective f) (s : ιSubgroup G) :
                  map f (iInf s) = ⨅ (i : ι), map f (s i)
                  theorem AddSubgroup.map_iInf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} [Nonempty ι] (f : G →+ N) (hf : Function.Injective f) (s : ιAddSubgroup G) :
                  map f (iInf s) = ⨅ (i : ι), map f (s i)
                  theorem Subgroup.comap_sup_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup N) (f : G →* N) :
                  comap f Hcomap f K comap f (HK)
                  theorem AddSubgroup.comap_sup_comap_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup N) (f : G →+ N) :
                  comap f Hcomap f K comap f (HK)
                  theorem Subgroup.iSup_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ιSubgroup N) :
                  ⨆ (i : ι), comap f (s i) comap f (iSup s)
                  theorem AddSubgroup.iSup_comap_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ιAddSubgroup N) :
                  ⨆ (i : ι), comap f (s i) comap f (iSup s)
                  theorem Subgroup.comap_inf {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup N) (f : G →* N) :
                  comap f (HK) = comap f Hcomap f K
                  theorem AddSubgroup.comap_inf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup N) (f : G →+ N) :
                  comap f (HK) = comap f Hcomap f K
                  theorem Subgroup.comap_iInf {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ιSubgroup N) :
                  comap f (iInf s) = ⨅ (i : ι), comap f (s i)
                  theorem AddSubgroup.comap_iInf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ιAddSubgroup N) :
                  comap f (iInf s) = ⨅ (i : ι), comap f (s i)
                  theorem Subgroup.map_inf_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) :
                  map f (HK) map f Hmap f K
                  theorem AddSubgroup.map_inf_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) :
                  map f (HK) map f Hmap f K
                  theorem Subgroup.map_inf_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
                  map f (HK) = map f Hmap f K
                  theorem AddSubgroup.map_inf_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective f) :
                  map f (HK) = map f Hmap f K
                  @[simp]
                  theorem Subgroup.map_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                  @[simp]
                  theorem AddSubgroup.map_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                  theorem Subgroup.map_top_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (h : Function.Surjective f) :
                  theorem AddSubgroup.map_top_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (h : Function.Surjective f) :
                  @[simp]
                  theorem Subgroup.map_equiv_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] {F : Type u_7} [EquivLike F G N] [MulEquivClass F G N] (f : F) :
                  map f =
                  @[simp]
                  theorem AddSubgroup.map_equiv_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {F : Type u_7} [EquivLike F G N] [AddEquivClass F G N] (f : F) :
                  map f =
                  @[simp]
                  theorem Subgroup.comap_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
                  @[simp]
                  theorem AddSubgroup.comap_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
                  def Subgroup.subgroupOf {G : Type u_1} [Group G] (H K : Subgroup G) :

                  For any subgroups H and K, view H ⊓ K as a subgroup of K.

                  Equations
                    Instances For

                      For any subgroups H and K, view H ⊓ K as a subgroup of K.

                      Equations
                        Instances For
                          def Subgroup.subgroupOfEquivOfLe {G : Type u_7} [Group G] {H K : Subgroup G} (h : H K) :
                          (H.subgroupOf K) ≃* H

                          If H ≤ K, then H as a subgroup of K is isomorphic to H.

                          Equations
                            Instances For
                              def AddSubgroup.addSubgroupOfEquivOfLe {G : Type u_7} [AddGroup G] {H K : AddSubgroup G} (h : H K) :
                              (H.addSubgroupOf K) ≃+ H

                              If H ≤ K, then H as a subgroup of K is isomorphic to H.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem Subgroup.subgroupOfEquivOfLe_apply_coe {G : Type u_7} [Group G] {H K : Subgroup G} (h : H K) (g : (H.subgroupOf K)) :
                                  ((subgroupOfEquivOfLe h) g) = g
                                  @[simp]
                                  theorem AddSubgroup.addSubgroupOfEquivOfLe_symm_apply_coe_coe {G : Type u_7} [AddGroup G] {H K : AddSubgroup G} (h : H K) (g : H) :
                                  ((addSubgroupOfEquivOfLe h).symm g) = g
                                  @[simp]
                                  theorem Subgroup.subgroupOfEquivOfLe_symm_apply_coe_coe {G : Type u_7} [Group G] {H K : Subgroup G} (h : H K) (g : H) :
                                  ((subgroupOfEquivOfLe h).symm g) = g
                                  @[simp]
                                  theorem AddSubgroup.addSubgroupOfEquivOfLe_apply_coe {G : Type u_7} [AddGroup G] {H K : AddSubgroup G} (h : H K) (g : (H.addSubgroupOf K)) :
                                  ((addSubgroupOfEquivOfLe h) g) = g
                                  @[simp]
                                  theorem Subgroup.comap_subtype {G : Type u_1} [Group G] (H K : Subgroup G) :
                                  @[simp]
                                  @[simp]
                                  theorem Subgroup.comap_inclusion_subgroupOf {G : Type u_1} [Group G] {K₁ K₂ : Subgroup G} (h : K₁ K₂) (H : Subgroup G) :
                                  comap (inclusion h) (H.subgroupOf K₂) = H.subgroupOf K₁
                                  @[simp]
                                  theorem AddSubgroup.comap_inclusion_addSubgroupOf {G : Type u_1} [AddGroup G] {K₁ K₂ : AddSubgroup G} (h : K₁ K₂) (H : AddSubgroup G) :
                                  theorem Subgroup.coe_subgroupOf {G : Type u_1} [Group G] (H K : Subgroup G) :
                                  (H.subgroupOf K) = K.subtype ⁻¹' H
                                  theorem AddSubgroup.coe_addSubgroupOf {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :
                                  (H.addSubgroupOf K) = K.subtype ⁻¹' H
                                  theorem Subgroup.mem_subgroupOf {G : Type u_1} [Group G] {H K : Subgroup G} {h : K} :
                                  h H.subgroupOf K h H
                                  theorem AddSubgroup.mem_addSubgroupOf {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} {h : K} :
                                  h H.addSubgroupOf K h H
                                  @[simp]
                                  theorem Subgroup.subgroupOf_map_subtype {G : Type u_1} [Group G] (H K : Subgroup G) :
                                  map K.subtype (H.subgroupOf K) = HK
                                  @[simp]
                                  theorem AddSubgroup.addSubgroupOf_map_subtype {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :
                                  map K.subtype (H.addSubgroupOf K) = HK
                                  theorem Subgroup.map_subgroupOf_eq_of_le {G : Type u_1} [Group G] {H K : Subgroup G} (h : H K) :
                                  @[simp]
                                  theorem Subgroup.bot_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) :
                                  @[simp]
                                  theorem Subgroup.top_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) :
                                  @[simp]
                                  theorem Subgroup.subgroupOf_self {G : Type u_1} [Group G] (H : Subgroup G) :
                                  @[simp]
                                  theorem Subgroup.subgroupOf_inj {G : Type u_1} [Group G] {H₁ H₂ K : Subgroup G} :
                                  H₁.subgroupOf K = H₂.subgroupOf K H₁K = H₂K
                                  @[simp]
                                  theorem AddSubgroup.addSubgroupOf_inj {G : Type u_1} [AddGroup G] {H₁ H₂ K : AddSubgroup G} :
                                  H₁.addSubgroupOf K = H₂.addSubgroupOf K H₁K = H₂K
                                  @[simp]
                                  theorem Subgroup.inf_subgroupOf_right {G : Type u_1} [Group G] (H K : Subgroup G) :
                                  (HK).subgroupOf K = H.subgroupOf K
                                  @[simp]
                                  @[simp]
                                  theorem Subgroup.inf_subgroupOf_left {G : Type u_1} [Group G] (H K : Subgroup G) :
                                  (KH).subgroupOf K = H.subgroupOf K
                                  @[simp]
                                  @[simp]
                                  theorem Subgroup.subgroupOf_eq_bot {G : Type u_1} [Group G] {H K : Subgroup G} :
                                  @[simp]
                                  theorem Subgroup.subgroupOf_eq_top {G : Type u_1} [Group G] {H K : Subgroup G} :
                                  @[simp]
                                  instance Subgroup.map_isMulCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') [IsMulCommutative H] :
                                  instance AddSubgroup.map_isAddCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [IsAddCommutative H] :
                                  @[deprecated Subgroup.map_isMulCommutative (since := "2025-04-09")]
                                  theorem Subgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') [IsMulCommutative H] :

                                  Alias of Subgroup.map_isMulCommutative.

                                  @[deprecated AddSubgroup.map_isAddCommutative (since := "2025-04-09")]
                                  theorem AddSubgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [IsAddCommutative H] :

                                  Alias of AddSubgroup.map_isAddCommutative.

                                  theorem Subgroup.comap_injective_isMulCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G' →* G} (hf : Function.Injective f) [IsMulCommutative H] :
                                  theorem AddSubgroup.comap_injective_isAddCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G' →+ G} (hf : Function.Injective f) [IsAddCommutative H] :
                                  @[deprecated Subgroup.comap_injective_isMulCommutative (since := "2025-04-09")]
                                  theorem Subgroup.comap_injective_isCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G' →* G} (hf : Function.Injective f) [IsMulCommutative H] :

                                  Alias of Subgroup.comap_injective_isMulCommutative.

                                  @[deprecated AddSubgroup.comap_injective_isAddCommutative (since := "2025-04-09")]
                                  theorem AddSubgroup.comap_injective_isCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G' →+ G} (hf : Function.Injective f) [IsAddCommutative H] :

                                  Alias of AddSubgroup.comap_injective_isAddCommutative.

                                  @[deprecated Subgroup.subgroupOf_isMulCommutative (since := "2025-04-09")]

                                  Alias of Subgroup.subgroupOf_isMulCommutative.

                                  @[deprecated AddSubgroup.addSubgroupOf_isAddCommutative (since := "2025-04-09")]

                                  Alias of AddSubgroup.addSubgroupOf_isAddCommutative.

                                  def MulEquiv.comapSubgroup {G : Type u_1} [Group G] {H : Type u_5} [Group H] (f : G ≃* H) :

                                  An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their inverse images.

                                  See also MulEquiv.mapSubgroup which maps subgroups to their forward images.

                                  Equations
                                    Instances For
                                      def AddEquiv.comapAddSubgroup {G : Type u_1} [AddGroup G] {H : Type u_5} [AddGroup H] (f : G ≃+ H) :

                                      An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their inverse images.

                                      See also AddEquiv.mapAddSubgroup which maps subgroups to their forward images.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem MulEquiv.comapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_5} [Group H] (f : G ≃* H) (H✝ : Subgroup G) :
                                          @[simp]
                                          theorem MulEquiv.comapSubgroup_apply {G : Type u_1} [Group G] {H : Type u_5} [Group H] (f : G ≃* H) (H✝ : Subgroup H) :
                                          f.comapSubgroup H✝ = Subgroup.comap (↑f) H✝
                                          @[simp]
                                          theorem AddEquiv.comapAddSubgroup_symm_apply {G : Type u_1} [AddGroup G] {H : Type u_5} [AddGroup H] (f : G ≃+ H) (H✝ : AddSubgroup G) :
                                          @[simp]
                                          theorem AddEquiv.comapAddSubgroup_apply {G : Type u_1} [AddGroup G] {H : Type u_5} [AddGroup H] (f : G ≃+ H) (H✝ : AddSubgroup H) :
                                          @[simp]
                                          theorem MulEquiv.coe_comapSubgroup {G : Type u_1} [Group G] {H : Type u_5} [Group H] (e : G ≃* H) :
                                          @[simp]
                                          theorem MulEquiv.symm_comapSubgroup {G : Type u_1} [Group G] {H : Type u_5} [Group H] (e : G ≃* H) :
                                          def MulEquiv.mapSubgroup {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) :

                                          An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their forward images.

                                          See also MulEquiv.comapSubgroup which maps subgroups to their inverse images.

                                          Equations
                                            Instances For
                                              def AddEquiv.mapAddSubgroup {G : Type u_1} [AddGroup G] {H : Type u_6} [AddGroup H] (f : G ≃+ H) :

                                              An isomorphism of 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.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem AddEquiv.mapAddSubgroup_symm_apply {G : Type u_1} [AddGroup G] {H : Type u_6} [AddGroup H] (f : G ≃+ H) (H✝ : AddSubgroup H) :
                                                  @[simp]
                                                  theorem MulEquiv.mapSubgroup_apply {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) (H✝ : Subgroup G) :
                                                  f.mapSubgroup H✝ = Subgroup.map (↑f) H✝
                                                  @[simp]
                                                  theorem AddEquiv.mapAddSubgroup_apply {G : Type u_1} [AddGroup G] {H : Type u_6} [AddGroup H] (f : G ≃+ H) (H✝ : AddSubgroup G) :
                                                  f.mapAddSubgroup H✝ = AddSubgroup.map (↑f) H✝
                                                  @[simp]
                                                  theorem MulEquiv.mapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) (H✝ : Subgroup H) :
                                                  @[simp]
                                                  theorem MulEquiv.coe_mapSubgroup {G : Type u_1} [Group G] {H : Type u_5} [Group H] (e : G ≃* H) :
                                                  @[simp]
                                                  @[simp]
                                                  theorem MulEquiv.symm_mapSubgroup {G : Type u_1} [Group G] {H : Type u_5} [Group H] (e : G ≃* H) :
                                                  @[simp]
                                                  @[simp]
                                                  theorem Subgroup.comap_toSubmonoid {G : Type u_1} [Group G] {N : Type u_5} [Group N] (e : G ≃* N) (s : Subgroup N) :
                                                  theorem Subgroup.map_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) :
                                                  map f (comap f H) H
                                                  theorem AddSubgroup.map_comap_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) :
                                                  map f (comap f H) H
                                                  theorem Subgroup.le_comap_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) :
                                                  H comap f (map f H)
                                                  theorem AddSubgroup.le_comap_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) :
                                                  H comap f (map f H)
                                                  theorem Subgroup.map_eq_comap_of_inverse {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (hl : Function.LeftInverse g f) (hr : Function.RightInverse g f) (H : Subgroup G) :
                                                  map f H = comap g H
                                                  theorem AddSubgroup.map_eq_comap_of_inverse {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (hl : Function.LeftInverse g f) (hr : Function.RightInverse g f) (H : AddSubgroup G) :
                                                  map f H = comap g H
                                                  noncomputable def Subgroup.equivMapOfInjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
                                                  H ≃* (map f H)

                                                  A subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use MulEquiv.subgroupMap for better definitional equalities.

                                                  Equations
                                                    Instances For
                                                      noncomputable def AddSubgroup.equivMapOfInjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective f) :
                                                      H ≃+ (map f H)

                                                      An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use AddEquiv.addSubgroupMap for better definitional equalities.

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem Subgroup.coe_equivMapOfInjective_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) (hf : Function.Injective f) (h : H) :
                                                          ((H.equivMapOfInjective f hf) h) = f h
                                                          @[simp]
                                                          theorem AddSubgroup.coe_equivMapOfInjective_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective f) (h : H) :
                                                          ((H.equivMapOfInjective f hf) h) = f h
                                                          def MonoidHom.subgroupComap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H' : Subgroup G') :
                                                          (Subgroup.comap f H') →* H'

                                                          The MonoidHom from the preimage of a subgroup to itself.

                                                          Equations
                                                            Instances For
                                                              def AddMonoidHom.addSubgroupComap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') :
                                                              (AddSubgroup.comap f H') →+ H'

                                                              the AddMonoidHom from the preimage of an additive subgroup to itself.

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem AddMonoidHom.addSubgroupComap_apply_coe {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') (x : (AddSubmonoid.comap f H'.toAddSubmonoid)) :
                                                                  ((f.addSubgroupComap H') x) = f x
                                                                  @[simp]
                                                                  theorem MonoidHom.subgroupComap_apply_coe {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H' : Subgroup G') (x : (Submonoid.comap f H'.toSubmonoid)) :
                                                                  ((f.subgroupComap H') x) = f x
                                                                  theorem MonoidHom.subgroupComap_surjective_of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H' : Subgroup G') (hf : Function.Surjective f) :
                                                                  def MonoidHom.subgroupMap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) :
                                                                  H →* (Subgroup.map f H)

                                                                  The MonoidHom from a subgroup to its image.

                                                                  Equations
                                                                    Instances For
                                                                      def AddMonoidHom.addSubgroupMap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) :
                                                                      H →+ (AddSubgroup.map f H)

                                                                      the AddMonoidHom from an additive subgroup to its image

                                                                      Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem AddMonoidHom.addSubgroupMap_apply_coe {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) (x : H.toAddSubmonoid) :
                                                                          ((f.addSubgroupMap H) x) = f x
                                                                          @[simp]
                                                                          theorem MonoidHom.subgroupMap_apply_coe {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) (x : H.toSubmonoid) :
                                                                          ((f.subgroupMap H) x) = f x
                                                                          theorem MonoidHom.subgroupMap_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) :
                                                                          def MulEquiv.subgroupCongr {G : Type u_1} [Group G] {H K : Subgroup G} (h : H = K) :
                                                                          H ≃* K

                                                                          Makes the identity isomorphism from a proof two subgroups of a multiplicative group are equal.

                                                                          Equations
                                                                            Instances For
                                                                              def AddEquiv.addSubgroupCongr {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H = K) :
                                                                              H ≃+ K

                                                                              Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.

                                                                              Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem MulEquiv.subgroupCongr_apply {G : Type u_1} [Group G] {H K : Subgroup G} (h : H = K) (x : H) :
                                                                                  ((subgroupCongr h) x) = x
                                                                                  @[simp]
                                                                                  theorem AddEquiv.addSubgroupCongr_apply {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H = K) (x : H) :
                                                                                  ((addSubgroupCongr h) x) = x
                                                                                  @[simp]
                                                                                  theorem MulEquiv.subgroupCongr_symm_apply {G : Type u_1} [Group G] {H K : Subgroup G} (h : H = K) (x : K) :
                                                                                  ((subgroupCongr h).symm x) = x
                                                                                  @[simp]
                                                                                  theorem AddEquiv.addSubgroupCongr_symm_apply {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H = K) (x : K) :
                                                                                  ((addSubgroupCongr h).symm x) = x
                                                                                  def MulEquiv.subgroupMap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) :
                                                                                  H ≃* (Subgroup.map (↑e) H)

                                                                                  A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map, use Subgroup.equiv_map_of_injective.

                                                                                  Equations
                                                                                    Instances For
                                                                                      def AddEquiv.addSubgroupMap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) :
                                                                                      H ≃+ (AddSubgroup.map (↑e) H)

                                                                                      An additive subgroup is isomorphic to its image under an isomorphism. If you only have an injective map, use AddSubgroup.equiv_map_of_injective.

                                                                                      Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem MulEquiv.coe_subgroupMap_apply {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : H) :
                                                                                          ((e.subgroupMap H) g) = e g
                                                                                          @[simp]
                                                                                          theorem AddEquiv.coe_addSubgroupMap_apply {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : H) :
                                                                                          ((e.addSubgroupMap H) g) = e g
                                                                                          @[simp]
                                                                                          theorem MulEquiv.subgroupMap_symm_apply {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : (Subgroup.map (↑e) H)) :
                                                                                          (e.subgroupMap H).symm g = e.symm g,
                                                                                          @[simp]
                                                                                          theorem AddEquiv.addSubgroupMap_symm_apply {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : (AddSubgroup.map (↑e) H)) :
                                                                                          (e.addSubgroupMap H).symm g = e.symm g,
                                                                                          theorem MonoidHom.closure_preimage_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (s : Set N) :
                                                                                          theorem MonoidHom.map_closure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (s : Set G) :

                                                                                          The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup generated by the image of the set.

                                                                                          theorem AddMonoidHom.map_closure {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (s : Set G) :

                                                                                          The image under an AddMonoid hom of the AddSubgroup generated by a set equals the AddSubgroup generated by the image of the set.

                                                                                          @[simp]
                                                                                          theorem Subgroup.equivMapOfInjective_coe_mulEquiv {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (e : G ≃* G') :
                                                                                          @[simp]
                                                                                          theorem AddSubgroup.equivMapOfInjective_coe_addEquiv {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (e : G ≃+ G') :