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
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
@[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
  • Subgroup.map f H = { carrier := f '' H, mul_mem' := , one_mem' := , inv_mem' := }
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
  • AddSubgroup.map f H = { carrier := f '' H, add_mem' := , zero_mem' := , neg_mem' := }
@[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.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 (H K) = map f H map 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 (H K) = map f H map 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 (H K) = map f H map 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 (H K) = map f H map 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 H comap f K comap f (H K)
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 H comap f K comap f (H K)
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 (H K) = comap f H comap 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 (H K) = comap f H comap 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 (H K) map f H map 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 (H K) map f H map 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 (H K) = map f H map 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 (H K) = map f H map 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) :
@[simp]
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) :
@[simp]
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.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

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

Equations
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
  • Subgroup.subgroupOfEquivOfLe h = { toFun := fun (g : (H.subgroupOf K)) => g, , invFun := fun (g : H) => g, , , left_inv := , right_inv := , map_mul' := }
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
@[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 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 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 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) = H K
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) :
@[simp]
theorem Subgroup.inf_subgroupOf_left {G : Type u_1} [Group G] (H K : Subgroup G) :
@[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_isCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') [H.IsCommutative] :
instance AddSubgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [H.IsCommutative] :
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) [H.IsCommutative] :
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) [H.IsCommutative] :
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
@[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 MulEquiv.comapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_5} [Group H] (f : G ≃* H) (H✝ : Subgroup G) :
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
@[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 MulEquiv.mapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) (H✝ : Subgroup H) :
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
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
@[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
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
@[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
@[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
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
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
@[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
@[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
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
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
@[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
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
@[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') :