Basic lemmas about group extensions

This file gives basic lemmas about group extensions.

For the main definitions, see Mathlib/GroupTheory/GroupExtension/Defs.lean.

noncomputable def GroupExtension.quotientKerRightHomEquivRight {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] (S : GroupExtension N E G) : E ⧸ S.rightHom.ker ≃* G

The isomorphism E ⧸ S.rightHom.ker ≃* G induced by S.rightHom

noncomputable def AddGroupExtension.quotientKerRightHomEquivRight {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] (S : AddGroupExtension N E G) : E ⧸ S.rightHom.ker ≃+ G

The isomorphism E ⧸ S.rightHom.ker ≃+ G induced by S.rightHom

noncomputable def GroupExtension.quotientRangeInlEquivRight {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] (S : GroupExtension N E G) : E ⧸ S.inl.range ≃* G

The isomorphism E ⧸ S.inl.range ≃* G induced by S.rightHom

noncomputable def AddGroupExtension.quotientRangeInlEquivRight {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] (S : AddGroupExtension N E G) : E ⧸ S.inl.range ≃+ G

The isomorphism E ⧸ S.inl.range ≃+ G induced by S.rightHom

noncomputable def GroupExtension.surjInvRightHom {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] (S : GroupExtension N E G) : S.Section

An arbitrarily chosen section

noncomputable def AddGroupExtension.surjInvRightHom {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] (S : AddGroupExtension N E G) : S.Section

An arbitrarily chosen section

theorem GroupExtension.Section.mul_inv_mem_range_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (σ σ' : S.Section) (g : G) : σ g * (σ' g)⁻¹ ∈ S.inl.range

theorem AddGroupExtension.Section.add_neg_mem_range_inl {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} (σ σ' : S.Section) (g : G) : σ g + -σ' g ∈ S.inl.range

theorem GroupExtension.Section.inv_mul_mem_range_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (σ σ' : S.Section) (g : G) : (σ g)⁻¹ * σ' g ∈ S.inl.range

theorem AddGroupExtension.Section.neg_add_mem_range_inl {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} (σ σ' : S.Section) (g : G) : -σ g + σ' g ∈ S.inl.range

theorem GroupExtension.Section.exists_eq_inl_mul {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (σ σ' : S.Section) (g : G) : ∃ (n : N), σ g = S.inl n * σ' g

theorem AddGroupExtension.Section.exists_eq_inl_add {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} (σ σ' : S.Section) (g : G) : ∃ (n : N), σ g = S.inl n + σ' g

theorem GroupExtension.Section.exists_eq_mul_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (σ σ' : S.Section) (g : G) : ∃ (n : N), σ g = σ' g * S.inl n

theorem AddGroupExtension.Section.exists_eq_add_inl {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} (σ σ' : S.Section) (g : G) : ∃ (n : N), σ g = σ' g + S.inl n

theorem GroupExtension.Section.mul_mul_mul_inv_mem_range_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (σ : S.Section) (g₁ g₂ : G) : σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹ ∈ S.inl.range

theorem AddGroupExtension.Section.add_add_add_neg_mem_range_inl {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G) : σ g₁ + σ g₂ + -σ (g₁ + g₂) ∈ S.inl.range

theorem GroupExtension.Section.mul_inv_mul_mul_mem_range_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (σ : S.Section) (g₁ g₂ : G) : (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂ ∈ S.inl.range

theorem AddGroupExtension.Section.add_neg_add_add_mem_range_inl {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G) : -σ (g₁ + g₂) + σ g₁ + σ g₂ ∈ S.inl.range

theorem GroupExtension.Section.exists_mul_eq_inl_mul_mul {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (σ : S.Section) (g₁ g₂ : G) : ∃ (n : N), σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂

theorem AddGroupExtension.Section.exists_add_eq_inl_add_add {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G) : ∃ (n : N), σ (g₁ + g₂) = S.inl n + σ g₁ + σ g₂

theorem GroupExtension.Section.exists_mul_eq_mul_mul_inl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (σ : S.Section) (g₁ g₂ : G) : ∃ (n : N), σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n

theorem AddGroupExtension.Section.exists_add_eq_add_add_inl {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G) : ∃ (n : N), σ (g₁ + g₂) = σ g₁ + σ g₂ + S.inl n

def GroupExtension.Section.equivComp {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} {E' : Type u_4} [Group E'] {S' : GroupExtension N E' G} (σ : S.Section) (equiv : S.Equiv S') : S'.Section

The composition of an isomorphism between equivalent group extensions and a section

def AddGroupExtension.Section.equivComp {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} {E' : Type u_4} [AddGroup E'] {S' : AddGroupExtension N E' G} (σ : S.Section) (equiv : S.Equiv S') : S'.Section

The composition of an isomorphism between equivalent additive group extensions and a section

@[simp]

theorem GroupExtension.Section.equivComp_apply {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} {E' : Type u_4} [Group E'] {S' : GroupExtension N E' G} (σ : S.Section) (equiv : S.Equiv S') (a✝ : G) : (σ.equivComp equiv) a✝ = equiv (σ a✝)

@[simp]

theorem AddGroupExtension.Section.equivComp_apply {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} {E' : Type u_4} [AddGroup E'] {S' : AddGroupExtension N E' G} (σ : S.Section) (equiv : S.Equiv S') (a✝ : G) : (σ.equivComp equiv) a✝ = equiv (σ a✝)

noncomputable def GroupExtension.Equiv.ofMonoidHom {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} {E' : Type u_4} [Group E'] {S' : GroupExtension N E' G} (f : E →* E') (comp_inl : f.comp S.inl = S'.inl) (rightHom_comp : S'.rightHom.comp f = S.rightHom) : S.Equiv S'

An equivalence of group extensions from a homomorphism making a commuting diagram. Such a homomorphism is necessarily an isomorphism.

noncomputable def AddGroupExtension.Equiv.ofAddMonoidHom {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] {S : AddGroupExtension N E G} {E' : Type u_4} [AddGroup E'] {S' : AddGroupExtension N E' G} (f : E →+ E') (comp_inl : f.comp S.inl = S'.inl) (rightHom_comp : S'.rightHom.comp f = S.rightHom) : S.Equiv S'

An equivalence of additive group extensions from a homomorphism making a commuting diagram. Such a homomorphism is necessarily an isomorphism.

noncomputable def GroupExtension.Splitting.conjAct {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (s : S.Splitting) : G →* MulAut N

G acts on N by conjugation.

noncomputable def GroupExtension.Splitting.semidirectProductToGroupExtensionEquiv {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (s : S.Splitting) : (SemidirectProduct.toGroupExtension s.conjAct).Equiv S

A split group extension is equivalent to the extension associated to a semidirect product.

noncomputable def GroupExtension.Splitting.semidirectProductMulEquiv {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] {S : GroupExtension N E G} (s : S.Splitting) : N ⋊[s.conjAct] G ≃* E

The group associated to a split extension is isomorphic to a semidirect product.

theorem GroupExtension.IsConj.refl {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] (S : GroupExtension N E G) (s : S.Splitting) : S.IsConj s s

N-conjugacy is reflexive.

theorem AddGroupExtension.IsAddConj.refl {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] (S : AddGroupExtension N E G) (s : S.Splitting) : S.IsAddConj s s

N-conjugacy is reflexive.

theorem GroupExtension.IsConj.symm {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] (S : GroupExtension N E G) {s₁ s₂ : S.Splitting} (h : S.IsConj s₁ s₂) : S.IsConj s₂ s₁

N-conjugacy is symmetric.

theorem AddGroupExtension.IsAddConj.symm {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] (S : AddGroupExtension N E G) {s₁ s₂ : S.Splitting} (h : S.IsAddConj s₁ s₂) : S.IsAddConj s₂ s₁

N-conjugacy is symmetric.

theorem GroupExtension.IsConj.trans {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] (S : GroupExtension N E G) {s₁ s₂ s₃ : S.Splitting} (h₁ : S.IsConj s₁ s₂) (h₂ : S.IsConj s₂ s₃) : S.IsConj s₁ s₃

N-conjugacy is transitive.

theorem AddGroupExtension.IsAddConj.trans {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] (S : AddGroupExtension N E G) {s₁ s₂ s₃ : S.Splitting} (h₁ : S.IsAddConj s₁ s₂) (h₂ : S.IsAddConj s₂ s₃) : S.IsAddConj s₁ s₃

N-conjugacy is transitive.

def GroupExtension.IsConj.setoid {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] (S : GroupExtension N E G) : Setoid S.Splitting

The setoid of splittings with N-conjugacy

def AddGroupExtension.IsAddConj.setoid {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] (S : AddGroupExtension N E G) : Setoid S.Splitting

The setoid of splittings with N-conjugacy

def GroupExtension.ConjClasses {N : Type u_1} {G : Type u_2} [Group N] [Group G] {E : Type u_3} [Group E] (S : GroupExtension N E G) : Type (max u_2 u_3)

The N-conjugacy classes of splittings

def AddGroupExtension.AddConjClasses {N : Type u_1} {G : Type u_2} [AddGroup N] [AddGroup G] {E : Type u_3} [AddGroup E] (S : AddGroupExtension N E G) : Type (max u_2 u_3)

The N-conjugacy classes of splittings

theorem SemidirectProduct.right_splitting {N : Type u_1} {G : Type u_2} [Group N] [Group G] {φ : G →* MulAut N} (s : (toGroupExtension φ).Splitting) (g : G) : (s g).right = g