Restricting homomorphisms of extensions to their kernels

A homomorphism between group extensions over the identity of the quotient induces a unique homomorphism between their kernel terms. This restriction intertwines the conjugation actions, so it can be used as a coefficient map when comparing extension classes.

noncomputable def GroupExtension.kernelMap {G : Type u_1} {M : Type u_2} {N : Type u_3} {E : Type u_4} {E' : Type u_5} [Group G] [Group M] [Group N] [Group E] [Group E'] (S : GroupExtension M E G) (T : GroupExtension N E' G) (φ : E →* E') (hright : T.rightHom.comp φ = S.rightHom) : M →* N

The restriction of a homomorphism of extensions over the identity of the quotient to their kernel terms.

@[simp]

theorem GroupExtension.inl_kernelMap {G : Type u_1} {M : Type u_2} {N : Type u_3} {E : Type u_4} {E' : Type u_5} [Group G] [Group M] [Group N] [Group E] [Group E'] (S : GroupExtension M E G) (T : GroupExtension N E' G) (φ : E →* E') (hright : T.rightHom.comp φ = S.rightHom) (m : M) : T.inl ((S.kernelMap T φ hright) m) = φ (S.inl m)

Including the kernel restriction into the target recovers the original homomorphism on included kernel elements.

theorem GroupExtension.kernelMap_unique {G : Type u_1} {M : Type u_2} {N : Type u_3} {E : Type u_4} {E' : Type u_5} [Group G] [Group M] [Group N] [Group E] [Group E'] (S : GroupExtension M E G) (T : GroupExtension N E' G) (φ : E →* E') (hright : T.rightHom.comp φ = S.rightHom) (f : M →* N) (hinl : T.inl.comp f = φ.comp S.inl) : f = S.kernelMap T φ hright

The commuting inclusion square uniquely determines the restriction to the kernels.

@[simp]

theorem GroupExtension.kernelMap_conjAct {G : Type u_1} {M : Type u_2} {N : Type u_3} {E : Type u_4} {E' : Type u_5} [Group G] [Group M] [Group N] [Group E] [Group E'] (S : GroupExtension M E G) (T : GroupExtension N E' G) (φ : E →* E') (hright : T.rightHom.comp φ = S.rightHom) (e : E) (m : M) : (S.kernelMap T φ hright) ((S.conjAct e) m) = (T.conjAct (φ e)) ((S.kernelMap T φ hright) m)

Restriction to the kernels intertwines conjugation by corresponding elements of the total groups.