Basic operations on group extensions

This file provides operations on an existing group extension.

Main definitions and results

• GroupExtension.card_fiber_rightHom: every fiber of the projection has the cardinality of the kernel term.
• GroupExtension.relabelKer: relabels the kernel term of a group extension.
• GroupExtension.Section.monoidHomComp: transports a section along a homomorphism of extensions over the identity of the quotient group.
• GroupExtension.surjective_of_comp_inl_eq: a homomorphism of extensions over the identity of the quotient group is surjective as soon as it is surjective on the kernel terms.

The constructions are mirrored for additive groups by to_additive.

theorem GroupExtension.card_fiber_rightHom {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] (S : GroupExtension N E G) (g : G) : Nat.card ↑(⇑S.rightHom ⁻¹' {g}) = Nat.card N

Every fiber of the projection in a group extension has the cardinality of its kernel term.

theorem AddGroupExtension.card_fiber_rightHom {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) (g : G) : Nat.card ↑(⇑S.rightHom ⁻¹' {g}) = Nat.card N

Every fiber of the projection in an additive group extension has the cardinality of its kernel term.

def GroupExtension.relabelKer {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] (S : GroupExtension N E G) {N' : Type u_1} [Group N'] (e : N' ≃* N) : GroupExtension N' E G

Relabel the kernel term of a group extension along a multiplicative equivalence.

Equations

• S.relabelKer e = { inl := S.inl.comp e.toMonoidHom, rightHom := S.rightHom, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := ⋯ }

def AddGroupExtension.relabelKer {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) {N' : Type u_1} [AddGroup N'] (e : N' ≃+ N) : AddGroupExtension N' E G

Relabel the kernel term of an additive group extension along an additive equivalence.

Equations

• S.relabelKer e = { inl := S.inl.comp e.toAddMonoidHom, rightHom := S.rightHom, inl_injective := ⋯, range_inl_eq_ker_rightHom := ⋯, rightHom_surjective := ⋯ }

@[simp]

theorem GroupExtension.relabelKer_inl {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] (S : GroupExtension N E G) {N' : Type u_1} [Group N'] (e : N' ≃* N) : (S.relabelKer e).inl = S.inl.comp e.toMonoidHom

The inclusion of S.relabelKer e is the original inclusion after e.

@[simp]

theorem AddGroupExtension.relabelKer_inl {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) {N' : Type u_1} [AddGroup N'] (e : N' ≃+ N) : (S.relabelKer e).inl = S.inl.comp e.toAddMonoidHom

The inclusion of S.relabelKer e is the original inclusion after e.

@[simp]

theorem GroupExtension.relabelKer_rightHom {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] (S : GroupExtension N E G) {N' : Type u_1} [Group N'] (e : N' ≃* N) : (S.relabelKer e).rightHom = S.rightHom

Relabelling the kernel does not change the projection.

@[simp]

theorem AddGroupExtension.relabelKer_rightHom {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) {N' : Type u_1} [AddGroup N'] (e : N' ≃+ N) : (S.relabelKer e).rightHom = S.rightHom

Relabelling the kernel does not change the projection.

def GroupExtension.Section.monoidHomComp {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] {N' : Type u_1} {E' : Type u_2} [Group N'] [Group E'] {S : GroupExtension N E G} {S' : GroupExtension N' E' G} (σ : S.Section) (φ : E →* E') (hright : S'.rightHom.comp φ = S.rightHom) : S'.Section

Transport a section of an extension along a homomorphism φ of extensions over the identity of the quotient group: φ ∘ σ is a section of the target extension. The kernel terms of the two extensions may differ; for an equivalence of extensions with the same kernel this is GroupExtension.Section.equivComp.

Equations

• σ.monoidHomComp φ hright = { toFun := fun (g : G) => φ (σ g), rightInverse_rightHom := ⋯ }

def AddGroupExtension.Section.addMonoidHomComp {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] {N' : Type u_1} {E' : Type u_2} [AddGroup N'] [AddGroup E'] {S : AddGroupExtension N E G} {S' : AddGroupExtension N' E' G} (σ : S.Section) (φ : E →+ E') (hright : S'.rightHom.comp φ = S.rightHom) : S'.Section

Transport a section of an additive extension along a homomorphism φ of extensions over the identity of the quotient group: φ ∘ σ is a section of the target extension. The kernel terms of the two extensions may differ; for an equivalence of extensions with the same kernel this is AddGroupExtension.Section.equivComp.

Equations

• σ.addMonoidHomComp φ hright = { toFun := fun (g : G) => φ (σ g), rightInverse_rightHom := ⋯ }

@[simp]

theorem GroupExtension.Section.monoidHomComp_apply {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] {N' : Type u_1} {E' : Type u_2} [Group N'] [Group E'] {S : GroupExtension N E G} {S' : GroupExtension N' E' G} (σ : S.Section) (φ : E →* E') (hright : S'.rightHom.comp φ = S.rightHom) (g : G) : (σ.monoidHomComp φ hright) g = φ (σ g)

@[simp]

theorem AddGroupExtension.Section.addMonoidHomComp_apply {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] {N' : Type u_1} {E' : Type u_2} [AddGroup N'] [AddGroup E'] {S : AddGroupExtension N E G} {S' : AddGroupExtension N' E' G} (σ : S.Section) (φ : E →+ E') (hright : S'.rightHom.comp φ = S.rightHom) (g : G) : (σ.addMonoidHomComp φ hright) g = φ (σ g)

theorem GroupExtension.surjective_of_comp_inl_eq {N : Type u} {E : Type v} {G : Type w} [Group N] [Group E] [Group G] {N' : Type u_1} {E' : Type u_2} [Group N'] [Group E'] {S : GroupExtension N E G} {S' : GroupExtension N' E' G} (f : N →* N') (hf : Function.Surjective ⇑f) (φ : E →* E') (hinl : φ.comp S.inl = S'.inl.comp f) (hright : S'.rightHom.comp φ = S.rightHom) : Function.Surjective ⇑φ

A homomorphism of extensions over the identity of the quotient group is surjective as soon as its restriction f to the kernel terms is. It meets every fibre of the projection, because it covers the identity, and within a fibre it reaches every translate of the kernel, because f is surjective.

theorem AddGroupExtension.surjective_of_comp_inl_eq {N : Type u} {E : Type v} {G : Type w} [AddGroup N] [AddGroup E] [AddGroup G] {N' : Type u_1} {E' : Type u_2} [AddGroup N'] [AddGroup E'] {S : AddGroupExtension N E G} {S' : AddGroupExtension N' E' G} (f : N →+ N') (hf : Function.Surjective ⇑f) (φ : E →+ E') (hinl : φ.comp S.inl = S'.inl.comp f) (hright : S'.rightHom.comp φ = S.rightHom) : Function.Surjective ⇑φ

A homomorphism of additive extensions over the identity of the quotient group is surjective as soon as its restriction f to the kernel terms is. It meets every fibre of the projection, because it covers the identity, and within a fibre it reaches every translate of the kernel, because f is surjective.