Module

Finite.lean

Nyll.GaloisCohomology.GroupTheory.Finite

11 declarations indexed from sourceView source ↗

Module documentation

Finite group theory for the splitting corollaries

This file isolates the finite-group inputs for prime-power and normal-closure splitting arguments.

For the prime-power subgroup reduction, a proper subgroup of a finite group of order p ^ v is contained in a subgroup of index p. The proof below gives the slightly stronger statement for arbitrary finite p-groups. In the cyclic case the resulting subgroup is normal, hence produces the degree-p quotient used to choose the intermediate field.

For the normal-closure splitting argument, the normal closure is encoded by a core-free subgroup H. The canonical map from left cosets to double cosets is surjective. If it does not decrease cardinality, its right subgroup is contained in the normal core of H; therefore it is trivial when H is core-free.

Imports2

Mathlib.GroupTheory.DoubleCoset
Mathlib.GroupTheory.Sylow

Imported by3

theorem

exists_index_prime_supergroup_of_card_prime_power

L45 ↗

Documentation

A proper subgroup of a finite group of prime-power order is contained in a subgroup of index p.

This is the group-theoretic step in the prime-power subgroup reduction. Mathlib's Sylow extension theorem proves the stronger result without a cyclicity assumption.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section PrimePower
variable {G : Type uG} [Group G] [Finite G]

Lean source · statement

theorem exists_index_prime_supergroup_of_card_prime_power
    {p v : ℕ}
    (hp : p.Prime)
    (hv : 0 < v)
    (hGcard : Nat.card G = p ^ v)
    (D : Subgroup G)
    (hD : D ≠ ⊤) :
    ∃ P : Subgroup G, D ≤ P ∧ P.index = p

theorem

cyclic_exists_normal_index_prime_supergroup

L96 ↗

Documentation

In a cyclic finite group of prime-power order, the index-p supergroup is normal and its quotient has order p.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section PrimePower
variable {G : Type uG} [Group G] [Finite G]

Lean source · statement

theorem cyclic_exists_normal_index_prime_supergroup
    [IsCyclic G]
    {p v : ℕ}
    (hp : p.Prime)
    (hv : 0 < v)
    (hGcard : Nat.card G = p ^ v)
    (D : Subgroup G)
    (hD : D ≠ ⊤) :
    ∃ P : Subgroup G,
      D ≤ P ∧
      P.index = p ∧
      P.Normal ∧
      Nat.card (G ⧸ P) = p

theorem

subgroup_le_index_prime_subgroup_of_ne_top_cyclic_prime_power

L122 ↗

Documentation

In a cyclic group of finite prime-power cardinality, every proper subgroup is contained in every subgroup of index p.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section PrimePower
variable {G : Type uG} [Group G] [Finite G]
omit [Finite G] in

Lean source · statement

theorem subgroup_le_index_prime_subgroup_of_ne_top_cyclic_prime_power
    [IsCyclic G]
    {p exponent : ℕ}
    (hp : p.Prime)
    (hcard : Nat.card G = p ^ exponent)
    (P D : Subgroup G)
    (hPindex : P.index = p)
    (hD : D ≠ ⊤) :
    D ≤ P

theorem

exists_element_of_prime_order

L173 ↗

Documentation

Every nontrivial finite group contains an element of prime order. This supplies the cyclic prime-degree subgroup used after passing to a normal closure.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section PrimeOrder
variable (G : Type uG) [Group G] [Finite G] [Nontrivial G]

Lean source · statement

theorem exists_element_of_prime_order :
    ∃ (p : ℕ) (g : G),
      p.Prime ∧ orderOf g = p

theorem

exists_cyclic_subgroup_of_prime_card

L188 ↗

Documentation

Every nontrivial finite group contains an actual cyclic subgroup of prime cardinality.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section PrimeOrder
variable (G : Type uG) [Group G] [Finite G] [Nontrivial G]

Lean source · statement

theorem exists_cyclic_subgroup_of_prime_card :
    ∃ (p : ℕ) (P : Subgroup G),
      p.Prime ∧ Nat.card P = p ∧ IsCyclic P

def

doubleCosetRightProjection

L205 ↗

Documentation

The canonical projection H \ G = H \ G / 1 → H \ G / D.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section DoubleCosets
variable {G : Type uG} [Group G]

Lean source · statement

def doubleCosetRightProjection
    (H D : Subgroup G) :
    DoubleCoset.Quotient
        (H : Set G) (⊥ : Subgroup G) →
      DoubleCoset.Quotient (H : Set G) D

theorem

doubleCosetRightProjection_mk

L220 ↗

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section DoubleCosets
variable {G : Type uG} [Group G]

Lean source · statement

theorem doubleCosetRightProjection_mk
    (H D : Subgroup G)
    (g : G) :
    doubleCosetRightProjection H D
        (DoubleCoset.mk H (⊥ : Subgroup G) g) =
      DoubleCoset.mk H D g

theorem

doubleCosetRightProjection_surjective

L229 ↗

Documentation

The projection from left cosets to double cosets is onto.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section DoubleCosets
variable {G : Type uG} [Group G]

Lean source · statement

theorem doubleCosetRightProjection_surjective
    (H D : Subgroup G) :
    Function.Surjective
      (doubleCosetRightProjection H D)

theorem

rightSubgroup_le_normalCore_of_doubleCoset_projection_injective

L241 ↗

Documentation

If the left-coset to double-coset projection is injective, then the right subgroup lies in the normal core of the left subgroup.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section DoubleCosets
variable {G : Type uG} [Group G]

Lean source · statement

theorem rightSubgroup_le_normalCore_of_doubleCoset_projection_injective
    (H D : Subgroup G)
    (hinj : Function.Injective
      (doubleCosetRightProjection H D)) :
    D ≤ H.normalCore

theorem

rightSubgroup_le_normalCore_of_doubleCoset_card_eq

L279 ↗

Documentation

Equality between the number of left cosets and the number of double cosets forces the right subgroup into the normal core.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section DoubleCosets
variable {G : Type uG} [Group G]

Lean source · statement

theorem rightSubgroup_le_normalCore_of_doubleCoset_card_eq
    [Finite G]
    (H D : Subgroup G)
    (hcard :
      Nat.card
          (DoubleCoset.Quotient (H : Set G) D) =
        Nat.card
          (DoubleCoset.Quotient (H : Set G)
            (⊥ : Subgroup G))) :
    D ≤ H.normalCore

theorem

doubleCoset_card_eq_leftCoset_iff_of_normalCore_eq_bot

L314 ↗

Documentation

For a core-free subgroup H, the double-coset count equals the left-coset count exactly when the right subgroup is trivial.

This is the finite-group content of the normal-closure reduction.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe uG
section DoubleCosets
variable {G : Type uG} [Group G]

Lean source · statement

theorem doubleCoset_card_eq_leftCoset_iff_of_normalCore_eq_bot
    [Finite G]
    (H D : Subgroup G)
    (hcore : H.normalCore = ⊥) :
    Nat.card
          (DoubleCoset.Quotient (H : Set G) D) =
        Nat.card
          (DoubleCoset.Quotient (H : Set G)
            (⊥ : Subgroup G)) ↔
      D = ⊥

Module documentation

Finite group theory for the splitting corollaries

Declarations