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:

• G N are Groups

• H is a Subgroup of G

• x is an element of type G or type A

• f g : N →* G are group homomorphisms

• s k are sets of elements of type G

Definitions in the file:

• Subgroup.comap H f : the preimage of a subgroup H along the group homomorphism f is also a subgroup

• Subgroup.map f H : the image of a subgroup H along the group homomorphism f is also a subgroup

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) : Subgroup G

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

Equations

• Subgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

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

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

Equations

• AddSubgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Subgroup.coe_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup N) (f : G →* N) : ↑(Subgroup.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) : ↑(AddSubgroup.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 ∈ Subgroup.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 ∈ AddSubgroup.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' → Subgroup.comap f K ≤ Subgroup.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' → AddSubgroup.comap f K ≤ AddSubgroup.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) : Subgroup.comap f (Subgroup.comap g K) = Subgroup.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) : AddSubgroup.comap f (AddSubgroup.comap g K) = AddSubgroup.comap (g.comp f) K

@[simp]

theorem Subgroup.comap_id {N : Type u_5} [Group N] (K : Subgroup N) : Subgroup.comap (MonoidHom.id N) K = K

@[simp]

theorem AddSubgroup.comap_id {N : Type u_5} [AddGroup N] (K : AddSubgroup N) : AddSubgroup.comap (AddMonoidHom.id N) K = K

@[simp]

theorem Subgroup.toAddSubgroup_comap {G : Type u_1} [Group G] {G₂ : Type u_7} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) : AddSubgroup.comap (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.comap f s)

@[simp]

theorem AddSubgroup.toSubgroup_comap {A : Type u_7} {A₂ : Type u_8} [AddGroup A] [AddGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂) : Subgroup.comap (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.comap f s)

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

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) : AddSubgroup N

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) : ↑(Subgroup.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) : ↑(AddSubgroup.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 ∈ Subgroup.map f K ↔ ∃ x ∈ K, 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 ∈ AddSubgroup.map f K ↔ ∃ x ∈ K, 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 ∈ Subgroup.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 ∈ AddSubgroup.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 ∈ Subgroup.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 ∈ AddSubgroup.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' → Subgroup.map f K ≤ Subgroup.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' → AddSubgroup.map f K ≤ AddSubgroup.map f K'

@[simp]

theorem Subgroup.map_id {G : Type u_1} [Group G] (K : Subgroup G) : Subgroup.map (MonoidHom.id G) K = K

@[simp]

theorem AddSubgroup.map_id {G : Type u_1} [AddGroup G] (K : AddSubgroup G) : AddSubgroup.map (AddMonoidHom.id G) K = K

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) : Subgroup.map g (Subgroup.map f K) = Subgroup.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) : AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.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] : Subgroup.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] : AddSubgroup.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} : x ∈ Subgroup.map f.toMonoidHom K ↔ f.symm x ∈ K

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} : x ∈ AddSubgroup.map f.toAddMonoidHom K ↔ f.symm x ∈ K

@[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 ∈ Subgroup.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 ∈ AddSubgroup.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) : Subgroup.map f.toMonoidHom K = Subgroup.comap f.symm.toMonoidHom 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) : AddSubgroup.map f.toAddMonoidHom K = AddSubgroup.comap f.symm.toAddMonoidHom 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) : Subgroup.map (↑f) K = Subgroup.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) : AddSubgroup.map (↑f) K = AddSubgroup.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) : Subgroup.comap (↑f) K = Subgroup.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) : AddSubgroup.comap (↑f) K = AddSubgroup.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) : Subgroup.comap f.toMonoidHom K = Subgroup.map f.symm.toMonoidHom 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) : AddSubgroup.comap f.toAddMonoidHom K = AddSubgroup.map f.symm.toAddMonoidHom K

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} : Subgroup.map (↑e.symm) H = K ↔ Subgroup.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} : AddSubgroup.map (↑e.symm) H = K ↔ AddSubgroup.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} : Subgroup.map f K ≤ H ↔ K ≤ Subgroup.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} : AddSubgroup.map f K ≤ H ↔ K ≤ AddSubgroup.comap f H

theorem Subgroup.gc_map_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : GaloisConnection (Subgroup.map f) (Subgroup.comap f)

theorem AddSubgroup.gc_map_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f)

theorem Subgroup.map_sup {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H K : Subgroup G) (f : G →* N) : Subgroup.map f (H ⊔ K) = Subgroup.map f H ⊔ Subgroup.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) : AddSubgroup.map f (H ⊔ K) = AddSubgroup.map f H ⊔ AddSubgroup.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) : Subgroup.map f (iSup s) = ⨆ (i : ι), Subgroup.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) : AddSubgroup.map f (iSup s) = ⨆ (i : ι), AddSubgroup.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) : Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.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) : AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.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) : Subgroup.map f (iInf s) = ⨅ (i : ι), Subgroup.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) : AddSubgroup.map f (iInf s) = ⨅ (i : ι), AddSubgroup.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) : Subgroup.comap f H ⊔ Subgroup.comap f K ≤ Subgroup.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) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K ≤ AddSubgroup.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 : ι), Subgroup.comap f (s i) ≤ Subgroup.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 : ι), AddSubgroup.comap f (s i) ≤ AddSubgroup.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) : Subgroup.comap f (H ⊓ K) = Subgroup.comap f H ⊓ Subgroup.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) : AddSubgroup.comap f (H ⊓ K) = AddSubgroup.comap f H ⊓ AddSubgroup.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) : Subgroup.comap f (iInf s) = ⨅ (i : ι), Subgroup.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) : AddSubgroup.comap f (iInf s) = ⨅ (i : ι), AddSubgroup.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) : Subgroup.map f (H ⊓ K) ≤ Subgroup.map f H ⊓ Subgroup.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) : AddSubgroup.map f (H ⊓ K) ≤ AddSubgroup.map f H ⊓ AddSubgroup.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) : Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.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) : AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K

@[simp]

theorem Subgroup.map_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup.map f ⊥ = ⊥

@[simp]

theorem AddSubgroup.map_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.map f ⊥ = ⊥

@[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) : Subgroup.map 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) : AddSubgroup.map f ⊤ = ⊤

@[simp]

theorem Subgroup.comap_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup.comap f ⊤ = ⊤

@[simp]

theorem AddSubgroup.comap_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.comap f ⊤ = ⊤

def Subgroup.subgroupOf {G : Type u_1} [Group G] (H K : Subgroup G) : Subgroup ↥K

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

Equations

• H.subgroupOf K = Subgroup.comap K.subtype H

def AddSubgroup.addSubgroupOf {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : AddSubgroup ↥K

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

Equations

• H.addSubgroupOf K = AddSubgroup.comap K.subtype H

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

• AddSubgroup.addSubgroupOfEquivOfLe h = { toFun := fun (g : ↥(H.addSubgroupOf K)) => ⟨↑↑g, ⋯⟩, invFun := fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem Subgroup.subgroupOfEquivOfLe_apply_coe {G : Type u_7} [Group G] {H K : Subgroup G} (h : H ≤ K) (g : ↥(H.subgroupOf K)) : ↑((Subgroup.subgroupOfEquivOfLe h) 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) : ↑↑((Subgroup.subgroupOfEquivOfLe h).symm 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) : ↑↑((AddSubgroup.addSubgroupOfEquivOfLe 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)) : ↑((AddSubgroup.addSubgroupOfEquivOfLe h) g) = ↑↑g

@[simp]

theorem Subgroup.comap_subtype {G : Type u_1} [Group G] (H K : Subgroup G) : Subgroup.comap K.subtype H = H.subgroupOf K

@[simp]

theorem AddSubgroup.comap_subtype {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : AddSubgroup.comap K.subtype H = H.addSubgroupOf K

@[simp]

theorem Subgroup.comap_inclusion_subgroupOf {G : Type u_1} [Group G] {K₁ K₂ : Subgroup G} (h : K₁ ≤ K₂) (H : Subgroup G) : Subgroup.comap (Subgroup.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) : AddSubgroup.comap (AddSubgroup.inclusion h) (H.addSubgroupOf K₂) = H.addSubgroupOf K₁

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) : Subgroup.map K.subtype (H.subgroupOf K) = H ⊓ K

@[simp]

theorem AddSubgroup.addSubgroupOf_map_subtype {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : AddSubgroup.map K.subtype (H.addSubgroupOf K) = H ⊓ K

@[simp]

theorem Subgroup.bot_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : ⊥.subgroupOf H = ⊥

@[simp]

theorem AddSubgroup.bot_addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⊥.addSubgroupOf H = ⊥

@[simp]

theorem Subgroup.top_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : ⊤.subgroupOf H = ⊤

@[simp]

theorem AddSubgroup.top_addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⊤.addSubgroupOf H = ⊤

theorem Subgroup.subgroupOf_bot_eq_bot {G : Type u_1} [Group G] (H : Subgroup G) : H.subgroupOf ⊥ = ⊥

theorem AddSubgroup.addSubgroupOf_bot_eq_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.addSubgroupOf ⊥ = ⊥

theorem Subgroup.subgroupOf_bot_eq_top {G : Type u_1} [Group G] (H : Subgroup G) : H.subgroupOf ⊥ = ⊤

theorem AddSubgroup.addSubgroupOf_bot_eq_top {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.addSubgroupOf ⊥ = ⊤

@[simp]

theorem Subgroup.subgroupOf_self {G : Type u_1} [Group G] (H : Subgroup G) : H.subgroupOf H = ⊤

@[simp]

theorem AddSubgroup.addSubgroupOf_self {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.addSubgroupOf H = ⊤

@[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) : (H ⊓ K).subgroupOf K = H.subgroupOf K

@[simp]

theorem AddSubgroup.inf_addSubgroupOf_right {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : (H ⊓ K).addSubgroupOf K = H.addSubgroupOf K

@[simp]

theorem Subgroup.inf_subgroupOf_left {G : Type u_1} [Group G] (H K : Subgroup G) : (K ⊓ H).subgroupOf K = H.subgroupOf K

@[simp]

theorem AddSubgroup.inf_addSubgroupOf_left {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : (K ⊓ H).addSubgroupOf K = H.addSubgroupOf K

@[simp]

theorem Subgroup.subgroupOf_eq_bot {G : Type u_1} [Group G] {H K : Subgroup G} : H.subgroupOf K = ⊥ ↔ Disjoint H K

@[simp]

theorem AddSubgroup.addSubgroupOf_eq_bot {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H.addSubgroupOf K = ⊥ ↔ Disjoint H K

@[simp]

theorem Subgroup.subgroupOf_eq_top {G : Type u_1} [Group G] {H K : Subgroup G} : H.subgroupOf K = ⊤ ↔ K ≤ H

@[simp]

theorem AddSubgroup.addSubgroupOf_eq_top {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H.addSubgroupOf K = ⊤ ↔ K ≤ H

instance Subgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') [H.IsCommutative] : (Subgroup.map f H).IsCommutative

Equations

• ⋯ = ⋯

instance AddSubgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [H.IsCommutative] : (AddSubgroup.map f H).IsCommutative

Equations

• ⋯ = ⋯

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] : (Subgroup.comap 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] : (AddSubgroup.comap f H).IsCommutative

instance Subgroup.subgroupOf_isCommutative {G : Type u_1} [Group G] (K H : Subgroup G) [H.IsCommutative] : (H.subgroupOf K).IsCommutative

Equations

• ⋯ = ⋯

instance AddSubgroup.addSubgroupOf_isCommutative {G : Type u_1} [AddGroup G] (K H : AddSubgroup G) [H.IsCommutative] : (H.addSubgroupOf K).IsCommutative

Equations

• ⋯ = ⋯

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

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

• f.comapSubgroup = { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem MulEquiv.comapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_5} [Group H] (f : G ≃* H) (H✝ : Subgroup G) : (RelIso.symm f.comapSubgroup) H✝ = Subgroup.comap (↑f.symm) H✝

@[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✝

def MulEquiv.mapSubgroup {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) : Subgroup G ≃o Subgroup 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

• f.mapSubgroup = { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem MulEquiv.mapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) (H✝ : Subgroup H) : (RelIso.symm f.mapSubgroup) H✝ = Subgroup.map (↑f.symm) 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✝

theorem Subgroup.map_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup.map f (Subgroup.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) : AddSubgroup.map f (AddSubgroup.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 ≤ Subgroup.comap f (Subgroup.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 ≤ AddSubgroup.comap f (AddSubgroup.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) : Subgroup.map f H = Subgroup.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) : AddSubgroup.map f H = AddSubgroup.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 ≃* ↥(Subgroup.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

• H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_mul' := ⋯ }

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 ≃+ ↥(AddSubgroup.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

• H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_add' := ⋯ }

@[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

• f.subgroupComap H' = f.submonoidComap H'.toSubmonoid

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

• f.addSubgroupComap H' = f.addSubmonoidComap H'.toAddSubmonoid

@[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

• f.subgroupMap H = f.submonoidMap H.toSubmonoid

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

• f.addSubgroupMap H = f.addSubmonoidMap H.toAddSubmonoid

@[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) : Function.Surjective ⇑(f.subgroupMap H)

theorem AddMonoidHom.addSubgroupMap_surjective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : Function.Surjective ⇑(f.addSubgroupMap H)

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

• MulEquiv.subgroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }

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

• AddEquiv.addSubgroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }

@[simp]

theorem MulEquiv.subgroupCongr_apply {G : Type u_1} [Group G] {H K : Subgroup G} (h : H = K) (x : ↥H) : ↑((MulEquiv.subgroupCongr h) x) = ↑x

@[simp]

theorem AddEquiv.addSubgroupCongr_apply {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H = K) (x : ↥H) : ↑((AddEquiv.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) : ↑((MulEquiv.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) : ↑((AddEquiv.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

• e.subgroupMap H = e.submonoidMap H.toSubmonoid

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

• e.addSubgroupMap H = e.addSubmonoidMap H.toAddSubmonoid

@[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) : Subgroup.closure (⇑f ⁻¹' s) ≤ Subgroup.comap f (Subgroup.closure s)

theorem AddMonoidHom.closure_preimage_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (s : Set N) : AddSubgroup.closure (⇑f ⁻¹' s) ≤ AddSubgroup.comap f (AddSubgroup.closure s)

theorem MonoidHom.map_closure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (s : Set G) : Subgroup.map f (Subgroup.closure s) = Subgroup.closure (⇑f '' s)

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) : AddSubgroup.map f (AddSubgroup.closure s) = AddSubgroup.closure (⇑f '' s)

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') : H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H

@[simp]

theorem AddSubgroup.equivMapOfInjective_coe_addEquiv {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (e : G ≃+ G') : H.equivMapOfInjective ↑e ⋯ = e.addSubgroupMap H