Maps of subgroups

Mathlib's MonoidHom.subgroupComap sends the preimage K.comap f of a subgroup K to K. This file records how surjective homomorphisms act on centres and on derived subgroups.

An isomorphism carrying a subgroup A onto a subgroup B restricts to an isomorphism ↥A ≃* ↥B, and carries the coset space G ⧸ A bijectively onto H ⧸ B. That restriction is TauCeti.Subgroup.congrOfMapEq, and every subgroup a construction transports along an isomorphism — here the derived subgroup, elsewhere the fixed subgroup of an endomorphism — uses it rather than repeating the composition of MulEquiv.subgroupMap with MulEquiv.subgroupCongr.

Main definitions

• TauCeti.Subgroup.congrOfMapEq: the isomorphism of subgroups restricted from an isomorphism of groups carrying the one onto the other.
• MulEquiv.commutatorCongr: its instance for the derived subgroup.
• MonoidHom.subgroupCongr: a homomorphism of subgroups transported along equalities of its domain and codomain, for reading a construction through two presentations of the subgroups it connects.
• TauCeti.QuotientGroup.congrOfMapEq: its coset-space companion — an isomorphism carrying A onto B gives a bijection G ⧸ A ≃ H ⧸ B. Neither subgroup need be normal, which is what distinguishes it from Mathlib's QuotientGroup.congr.

Main results

• QuotientGroup.congrOfSurjectiveOfKerLe: coset spaces transport along a surjection whose kernel lies in the subgroup.
• MonoidHom.center_le_ker: the centre lies in the kernel of a surjection onto a centreless group.
• TauCeti.Subgroup.map_commutator_eq_commutator: a surjective homomorphism carries the derived subgroup onto the derived subgroup.
• Subgroup.map_inf_comap: the image of H ⊓ f⁻¹(K) is f(H) ⊓ K.
• Subgroup.map_conj_map_conj: successive conjugations of a subgroup compose to one conjugation.
• Subgroup.map_map_conj: the image of a conjugate subgroup is the conjugate of the image.
• Subgroup.map_quotientGroupMap_map_mk': taking images in quotients commutes with the maps induced on quotients.
• MonoidHom.subgroupCongr_injective, MonoidHom.subgroupCongr_surjective: transport along equalities of the domain and codomain preserves injectivity and surjectivity.
• Subgroup.subtype_comp_subgroupOfEquivOfLe, TauCeti.Subgroup.subtype_comp_congrOfMapEq: the isomorphisms subgroupOfEquivOfLe and congrOfMapEq commute with the inclusions of subgroups.
• Subgroup.subgroupOf_smul_eq: the actions of V and of V.subgroupOf U on a G-set agree on elements with the same image in G.
• Subgroup.closure_coe_preimage_of_subset: for s ⊆ K, the subgroup of K generated by s is the pullback of the subgroup of G generated by s.

theorem MonoidHom.center_le_ker {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (hf : Function.Surjective ⇑f) (hH : Subgroup.center H = ⊥) : Subgroup.center G ≤ f.ker

The centre of a group lies in the kernel of every surjection onto a centreless group.

Mathlib's Subgroup.map_center_le_center bounds the image of the centre under any surjection by Subgroup.center H; this lemma is the special case where that bound is ⊥.

@[simp]

theorem Subgroup.subtype_comp_subgroupOfEquivOfLe {G : Type u_1} [Group G] {A B : Subgroup G} (h : A ≤ B) : A.subtype.comp ↑(subgroupOfEquivOfLe h) = B.subtype.comp (A.subgroupOf B).subtype

Along A ≤ B, the identification Subgroup.subgroupOfEquivOfLe of A.subgroupOf B with A commutes with the inclusions into G. This is the homomorphism form of Mathlib's pointwise Subgroup.subgroupOfEquivOfLe_apply_coe.

theorem Subgroup.subgroupOf_smul_eq {G : Type u_1} [Group G] (U V : Subgroup G) (M : Type u_3) [MulAction G M] (v : ↥(V.subgroupOf U)) (w : ↥V) (a : M) (h : ↑↑v = ↑w) : w • a = v • a

The actions of a subgroup V of G and of its copy V.subgroupOf U inside a subgroup U on a G-set agree on elements with the same image in G: both are restrictions of the action of G. This is the compatibility of actions under which TauCeti.DiscreteCoind.transIso identifies Coind_U^G (Coind_{V ⊓ U}^U M) with Coind_V^G M.

theorem Subgroup.closure_coe_preimage_of_subset {G : Type u_1} [Group G] {K : Subgroup G} {s : Set G} (hs : s ⊆ ↑K) : closure (Subtype.val ⁻¹' s) = comap K.subtype (closure s)

For s ⊆ K, the subgroup of K generated by the elements of s is the pullback of the subgroup of G generated by s. Mathlib's Subgroup.closure_preimage_le is the inequality that holds for every homomorphism.

Restricting an isomorphism to a subgroup

def TauCeti.Subgroup.congrOfMapEq {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {A : Subgroup G} {B : Subgroup H} (h : Subgroup.map (↑e) A = B) : ↥A ≃* ↥B

The isomorphism of subgroups restricted from an isomorphism of groups carrying the one onto the other.

Equations

• TauCeti.Subgroup.congrOfMapEq e h = (e.subgroupMap A).trans (MulEquiv.subgroupCongr h)

@[simp]

theorem TauCeti.Subgroup.coe_congrOfMapEq_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {A : Subgroup G} {B : Subgroup H} (h : Subgroup.map (↑e) A = B) (x : ↥A) : ↑((congrOfMapEq e h) x) = e ↑x

@[simp]

theorem TauCeti.Subgroup.coe_congrOfMapEq_symm_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {A : Subgroup G} {B : Subgroup H} (h : Subgroup.map (↑e) A = B) (y : ↥B) : ↑((congrOfMapEq e h).symm y) = e.symm ↑y

@[simp]

theorem TauCeti.Subgroup.congrOfMapEq_refl {G : Type u_1} [Group G] {A : Subgroup G} (h : Subgroup.map (↑(MulEquiv.refl G)) A = A) : congrOfMapEq (MulEquiv.refl G) h = MulEquiv.refl ↥A

@[simp]

theorem TauCeti.Subgroup.congrOfMapEq_trans {G : Type u_1} {H : Type u_2} [Group G] [Group H] {K : Type u_3} [Group K] (e : G ≃* H) {A : Subgroup G} {B : Subgroup H} (h : Subgroup.map (↑e) A = B) (f : H ≃* K) {C : Subgroup K} (h' : Subgroup.map (↑f) B = C) : (congrOfMapEq e h).trans (congrOfMapEq f h') = congrOfMapEq (e.trans f) ⋯

@[simp]

theorem TauCeti.Subgroup.subtype_comp_congrOfMapEq {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {A : Subgroup G} {B : Subgroup H} (h : Subgroup.map (↑e) A = B) : B.subtype.comp ↑(congrOfMapEq e h) = (↑e).comp A.subtype

Restricting an isomorphism to subgroups commutes with the inclusions of the subgroups. This is the homomorphism form of the pointwise Subgroup.coe_congrOfMapEq_apply.

theorem TauCeti.Subgroup.congrOfMapEq_symm {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {A : Subgroup G} {B : Subgroup H} (h : Subgroup.map (↑e) A = B) : (congrOfMapEq e h).symm = congrOfMapEq e.symm ⋯

def MonoidHom.subgroupCongr {G : Type u_1} {H : Type u_2} [Group G] [Group H] {A A' : Subgroup G} {B B' : Subgroup H} (hA : A' = A) (hB : B' = B) (f : ↥A →* ↥B) : ↥A' →* ↥B'

The homomorphism of subgroups obtained from a homomorphism between two other subgroups by transporting along equalities of the domain and of the codomain.

Equations

• MonoidHom.subgroupCongr hA hB f = (MulEquiv.subgroupCongr hB).symm.toMonoidHom.comp (f.comp (MulEquiv.subgroupCongr hA).toMonoidHom)

@[simp]

theorem MonoidHom.coe_subgroupCongr_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] {A A' : Subgroup G} {B B' : Subgroup H} (hA : A' = A) (hB : B' = B) (f : ↥A →* ↥B) (x : ↥A') : ↑((subgroupCongr hA hB f) x) = ↑(f ⟨↑x, ⋯⟩)

The transported homomorphism takes the same value in the ambient group as the original does at the corresponding element.

The equation is stated after coercion to H because its two sides land in the different subtypes ↥B' and ↥B. As a simp lemma it moves the transport off the homomorphism and onto its argument; MonoidHom.subgroupCongr_id and MonoidHom.subgroupCongr_comp rewrite the transported homomorphism itself instead.

@[simp]

theorem MonoidHom.subgroupCongr_id {G : Type u_1} [Group G] {A A' : Subgroup G} (hA : A' = A) : subgroupCongr hA hA (id ↥A) = id ↥A'

Transporting the identity homomorphism along one equality of subgroups, on both sides, gives the identity.

MonoidHom.subgroupCongr takes one equality at each end; they coincide here because the transported map is an endomorphism. Both subgroups are pinned by the left-hand side, which is what makes this a simp lemma where the composition companion MonoidHom.subgroupCongr_comp is not.

theorem MonoidHom.subgroupCongr_comp {G : Type u_1} {H : Type u_2} [Group G] [Group H] {K : Type u_3} [Group K] {A A' : Subgroup G} {B B' : Subgroup H} {C C' : Subgroup K} (hA : A' = A) (hB : B' = B) (hC : C' = C) (f : ↥A →* ↥B) (g : ↥B →* ↥C) : subgroupCongr hA hC (g.comp f) = (subgroupCongr hB hC g).comp (subgroupCongr hA hB f)

Transport commutes with composition: transporting g.comp f along the outer two equalities agrees with transporting f and g separately through a common middle subgroup.

Not a simp lemma: the middle subgroup B' and its presentation hB occur only on the right-hand side, so simp would have to invent them and would rewrite into an unrelated instantiation. MonoidHom.subgroupCongr_id is the identity companion.

theorem MonoidHom.subgroupCongr_injective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {A A' : Subgroup G} {B B' : Subgroup H} (hA : A' = A) (hB : B' = B) {f : ↥A →* ↥B} (hf : Function.Injective ⇑f) : Function.Injective ⇑(subgroupCongr hA hB f)

Transport along equalities of the domain and codomain preserves injectivity.

The transport composes f with two isomorphisms, so it is injective exactly when f is; only the direction a use site needs is recorded. MonoidHom.subgroupCongr_surjective is the companion for surjectivity.

theorem MonoidHom.subgroupCongr_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {A A' : Subgroup G} {B B' : Subgroup H} (hA : A' = A) (hB : B' = B) {f : ↥A →* ↥B} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(subgroupCongr hA hB f)

Transport along equalities of the domain and codomain preserves surjectivity.

The transport composes f with two isomorphisms, so it is surjective exactly when f is; only the direction a use site needs is recorded. MonoidHom.subgroupCongr_injective is the companion for injectivity.

Transporting the derived subgroup

theorem TauCeti.Subgroup.map_commutator_eq_commutator {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G →* H} (hf : Function.Surjective ⇑f) : Subgroup.map f (commutator G) = commutator H

A surjective homomorphism carries the derived subgroup onto the derived subgroup.

Without surjectivity only ≤ survives (Mathlib's map_derivedSeries_le_derivedSeries); Mathlib's Subgroup.map_commutator_eq keeps an equality for an arbitrary f, at the cost of describing the image as ⁅f.range, f.range⁆. Reach for this lemma rather than map_derivedSeries_eq whenever the derived subgroup is spelled commutator; MulEquiv.commutatorCongr below is the isomorphism it unlocks.

def MulEquiv.commutatorCongr {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) : ↥(commutator G) ≃* ↥(commutator H)

The isomorphism of derived subgroups restricted from an isomorphism of groups.

This is Subgroup.congrOfMapEq for the derived subgroup: the map equality is supplied internally, so a use site names only e, and the target is commutator H itself rather than the image (commutator G).map e that MulEquiv.subgroupMap would land in. It acts as e on elements, and its inverse as e.symm.

Equations

• e.commutatorCongr = TauCeti.Subgroup.congrOfMapEq e ⋯

@[simp]

theorem MulEquiv.coe_commutatorCongr_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) (x : ↥(commutator G)) : ↑(e.commutatorCongr x) = e ↑x

The restriction MulEquiv.commutatorCongr e to the derived subgroups agrees with e on underlying elements.

The equation is stated in the ambient group H because its two sides have the different types ↥(commutator H) and H. It is the derived-subgroup instance of Subgroup.coe_congrOfMapEq_apply, which simp cannot apply on its own because it cannot see through MulEquiv.commutatorCongr; MulEquiv.coe_commutatorCongr_symm_apply is the companion for the inverse, and Mathlib's MulEquiv.coe_subgroupMap_apply says the same for the literal image (commutator G).map e.

@[simp]

theorem MulEquiv.coe_commutatorCongr_symm_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) (y : ↥(commutator H)) : ↑(e.commutatorCongr.symm y) = e.symm ↑y

The inverse of the restriction MulEquiv.commutatorCongr e to the derived subgroups agrees with e.symm on underlying elements.

The equation is stated in the ambient group G because its two sides have the different types ↥(commutator G) and G. It is the derived-subgroup instance of Subgroup.coe_congrOfMapEq_symm_apply, which simp cannot apply on its own because it cannot see through MulEquiv.commutatorCongr; MulEquiv.coe_commutatorCongr_apply is the companion for the forward direction, MulEquiv.commutatorCongr_symm rewrites the whole inverse rather than a single value, and Mathlib's MulEquiv.subgroupMap_symm_apply says the same for the literal image (commutator G).map e but returns the subtype ⟨e.symm ↑y, _⟩ rather than its coercion.

@[simp]

theorem MulEquiv.commutatorCongr_refl {G : Type u_1} [Group G] : (refl G).commutatorCongr = refl ↥(commutator G)

Restricting the identity isomorphism of G to the derived subgroup gives the identity of ↥(commutator G).

The derived-subgroup instance of Subgroup.congrOfMapEq_refl, and a simp lemma in its own right: MulEquiv.commutatorCongr does not unfold, so that general lemma never fires on this left-hand side. MulEquiv.commutatorCongr_trans and MulEquiv.commutatorCongr_symm are the companion composition and inverse statements; Mathlib's abelianizationCongr_refl is the same coherence for the abelianization.

@[simp]

theorem MulEquiv.commutatorCongr_trans {G : Type u_1} {H : Type u_2} [Group G] [Group H] {K : Type u_3} [Group K] (e : G ≃* H) (f : H ≃* K) : e.commutatorCongr.trans f.commutatorCongr = (e.trans f).commutatorCongr

Restricting to derived subgroups is functorial: the restriction of e.trans f is the composite of the restrictions of e and of f.

The derived-subgroup instance of Subgroup.congrOfMapEq_trans, and a simp lemma in its own right: MulEquiv.commutatorCongr does not unfold, so that general lemma never fires on this left-hand side. Both map equalities are supplied internally, so a use site names only e and f. MulEquiv.commutatorCongr_refl and MulEquiv.commutatorCongr_symm are the companion identity and inverse statements; Mathlib's abelianizationCongr_trans is the same coherence for the abelianization.

theorem MulEquiv.commutatorCongr_symm {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) : e.commutatorCongr.symm = e.symm.commutatorCongr

Inverting the restriction of e to the derived subgroups gives the restriction of e.symm.

The derived-subgroup instance of Subgroup.congrOfMapEq_symm, whose map-equality hypothesis is supplied internally, so a use site names only e. This is the whole-isomorphism form, for when the inverse occurs as a map rather than applied to a point; MulEquiv.coe_commutatorCongr_symm_apply is the pointwise companion, and MulEquiv.commutatorCongr_refl and MulEquiv.commutatorCongr_trans are the identity and composition ones. Mathlib's abelianizationCongr_symm says the same for the abelianization.

theorem Subgroup.map_inf_comap {G : Type u_4} {N : Type u_5} [Group G] [Group N] (H : Subgroup G) (K : Subgroup N) (f : G →* N) : map f (H ⊓ comap f K) = map f H ⊓ K

The image of H ⊓ f⁻¹(K) under f is the part of K inside f(H).

theorem Subgroup.map_map_conj {G : Type u_1} {H : Type u_2} [Group G] [Group H] (R : Subgroup G) (f : G →* H) (g : G) : map f (map (MulEquiv.toMonoidHom (MulAut.conj g)) R) = map (MulEquiv.toMonoidHom (MulAut.conj (f g))) (map f R)

The image of a conjugate subgroup gRg⁻¹ under a homomorphism f is the conjugate of f(R) by f g.

Stated with Subgroup.map (MulAut.conj _).toMonoidHom, not the pointwise MulAut.conj _ • _: the two are definitionally equal (Subgroup.pointwise_smul_def is rfl) and Mathlib supplies no rewrite between them, so a use site in either spelling can apply this. It is Subgroup.map_map specialized to an inner conjugation, while Subgroup.Normal.map_conj_eq is the degenerate case in which conjugation fixes the subgroup instead of moving it.

theorem Subgroup.map_conj_map_conj {G : Type u_1} [Group G] (R : Subgroup G) (g h : G) : map (MulEquiv.toMonoidHom (MulAut.conj h)) (map (MulEquiv.toMonoidHom (MulAut.conj g)) R) = map (MulEquiv.toMonoidHom (MulAut.conj (h * g))) R

Conjugating a subgroup first by g and then by h is conjugation by h * g.

@[simp]

theorem Subgroup.map_quotientGroupMap_map_mk' {G : Type u_1} {H : Type u_2} [Group G] [Group H] (R : Subgroup G) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal] (f : G →* H) (h : N ≤ comap f M) : map (QuotientGroup.map N M f h) (map (QuotientGroup.mk' N) R) = map (QuotientGroup.mk' M) (map f R)

The image of a subgroup in G ⧸ N, pushed forward along the map G ⧸ N →* H ⧸ M induced by f, is the image in H ⧸ M of the image of the subgroup under f.

The subgroup-image form of Mathlib's pointwise QuotientGroup.map_mk'. R need not be related to N or M. As a simp lemma it fires left to right, so the normal form of an image taken in a quotient is "push down along f first, project afterwards", and QuotientGroup.map disappears. Subgroup.map_map_conj above is the same commuting square for conjugation.

Transporting a coset space along an isomorphism

def TauCeti.QuotientGroup.congrOfMapEq {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {A : Subgroup G} {B : Subgroup H} (h : Subgroup.map (↑e) A = B) : G ⧸ A ≃ H ⧸ B

Coset spaces transport along an isomorphism. If e : G ≃* H carries A onto B, then G ⧸ A ≃ H ⧸ B, by e on representatives.

Neither subgroup is assumed normal, so this is an equivalence of coset spaces. QuotientGroup.congr is the normal case, where the same data upgrades to a MulEquiv; it does not apply to a subgroup like Γ₁ ∩ gΓ₂g⁻¹, which is where this is needed. It is the coset-space companion of Subgroup.congrOfMapEq above.

Both subgroups are implicit and pinned by h, so neither is named at a use site, unlike QuotientGroup.congr. QuotientGroup.congrOfMapEq_mk is the @[simp] lemma that computes it on representatives, and QuotientGroup.congrOfSurjectiveOfKerLe below is the version for a map that is only surjective.

Equations

• TauCeti.QuotientGroup.congrOfMapEq e h = Quotient.congr e.toEquiv ⋯

@[simp]

theorem TauCeti.QuotientGroup.congrOfMapEq_mk {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {A : Subgroup G} {B : Subgroup H} (h : Subgroup.map (↑e) A = B) (a : G) : (congrOfMapEq e h) ↑a = ↑(e a)

QuotientGroup.congrOfMapEq acts by e on representatives: the transported coset of a is the coset of e a.

Downstream this lemma is not optional: congrOfMapEq is not @[expose]d, so outside this module the two sides are not definitionally equal and neither rfl nor the underlying Quotient.congr_mk closes the goal. QuotientGroup.congr_mk is Mathlib's version for normal subgroups, where the equivalence upgrades to a MulEquiv.

noncomputable def TauCeti.QuotientGroup.congrOfSurjectiveOfKerLe {G : Type u_1} {H : Type u_2} [Group G] [Group H] (ψ : G →* H) (hsurj : Function.Surjective ⇑ψ) {A : Subgroup G} {B : Subgroup H} (hker : ψ.ker ≤ A) (hmap : Subgroup.map ψ A = B) : G ⧸ A ≃ H ⧸ B

Coset spaces transport along a surjection whose kernel lies in the subgroup. For ψ surjective with ker ψ ≤ A and A.map ψ = B, the map G ⧸ A → H ⧸ B induced by ψ on representatives is a bijection.

Injectivity of ψ is not needed: ker ψ ≤ A makes the denominator absorb the kernel, so the index is unchanged. That is what lets a Hecke decomposition be carried into a group acting faithfully on the upper half-plane, where the collapsing of ±1 is the point rather than a defect. As with QuotientGroup.congrOfMapEq, neither subgroup need be normal.

Equations

• TauCeti.QuotientGroup.congrOfSurjectiveOfKerLe ψ hsurj hker hmap = Equiv.ofBijective (Quotient.map' ⇑ψ ⋯) ⋯

@[simp]

theorem TauCeti.QuotientGroup.congrOfSurjectiveOfKerLe_mk {G : Type u_1} {H : Type u_2} [Group G] [Group H] (ψ : G →* H) (hsurj : Function.Surjective ⇑ψ) {A : Subgroup G} {B : Subgroup H} (hker : ψ.ker ≤ A) (hmap : Subgroup.map ψ A = B) (a : G) : (congrOfSurjectiveOfKerLe ψ hsurj hker hmap) ↑a = ↑(ψ a)