NYLL
Module

Sylow.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Sylow
6 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity theorem: the Sylow step in the first reduction

This file formalizes the source-producing group-theoretic part of the first reduction. For a Sylow p-subgroup P of the actual finite quotient G(L/K), the already constructed fixed field M = L^P is an actual (not necessarily Galois over K) intermediate field. The actual quotient G(L/M) is a p-group and hence solvable, while [M:K] = (G(L/K) : P) is prime to p.

For an abelian group B, multiplication by [M:K] is therefore surjective on every Sylow p-subgroup of B, without assuming that the ambient group is finite. Equivalently, that Sylow subgroup lies in the image of the [M:K]-fold map. In the abstract reciprocity theorem the ambient norm quotient is only known at this point to have bounded exponent; its individual cyclic subgroups are finite. This avoids using the desired reciprocity surjectivity to prove finiteness. No reciprocity surjectivity or the finite reciprocity equivalence comparison is assumed here.

The fixed field of a Sylow subgroup

Sylow subgroups in a possibly infinite abelian target

Imports2
Imported by2

Declarations

theorem

abstractReciprocity_sylow_lowerQuotient_isPGroup

L51 ↗
ClassFormation.FiniteGaloisSubextension.abstractReciprocity_sylow_lowerQuotient_isPGroup
Documentation

For M = L^P, the actual lower quotient G(L/M) is a p-group. This is the identification G(L/M) \cong P, applied to an actual Sylow subgroup of the actual finite quotient G(L/K).

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem abstractReciprocity_sylow_lowerQuotient_isPGroup
    (L : FiniteGaloisSubextension K) {p : ℕ}
    (P : Sylow p L.extensionQuotient) :
    IsPGroup p
      ((L.intermediateField (P : Subgroup L.extensionQuotient)).toSubgroup ⧸
        extensionSubgroup
          (L.intermediateField (P : Subgroup L.extensionQuotient)) L.field
          (L.field_le_intermediateField
            (P : Subgroup L.extensionQuotient)))
theorem

abstractReciprocity_sylow_lowerQuotient_isSolvable

L70 ↗
ClassFormation.FiniteGaloisSubextension.abstractReciprocity_sylow_lowerQuotient_isSolvable
Documentation

Consequently, the actual extension L/M cut out by a Sylow subgroup is solvable. Mathlib proves this by the standard chain finite p-group \Rightarrow nilpotent \Rightarrow solvable.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
section SylowSolvability
local notation "IsSolvable" => Group.IsSolvable
Lean source · statement
theorem abstractReciprocity_sylow_lowerQuotient_isSolvable
    (L : FiniteGaloisSubextension K) {p : ℕ} [Fact p.Prime]
    (P : Sylow p L.extensionQuotient) :
    IsSolvable
      ((L.intermediateField (P : Subgroup L.extensionQuotient)).toSubgroup ⧸
        extensionSubgroup
          (L.intermediateField (P : Subgroup L.extensionQuotient)) L.field
          (L.field_le_intermediateField
            (P : Subgroup L.extensionQuotient)))
theorem

abstractReciprocity_sylow_intermediateDegree_eq_index

L106 ↗
ClassFormation.FiniteGaloisSubextension.abstractReciprocity_sylow_intermediateDegree_eq_index
Documentation

The degree of the actual fixed field M = L^P over K is the index of P in G(L/K). No normality of P, and hence none of M/K, is used.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem abstractReciprocity_sylow_intermediateDegree_eq_index
    (L : FiniteGaloisSubextension K) {p : ℕ}
    (P : Sylow p L.extensionQuotient) :
    (L.intermediateFiniteAbstractExtension
      (P : Subgroup L.extensionQuotient)).degree =
      (P : Subgroup L.extensionQuotient).index
theorem

abstractReciprocity_sylow_intermediateDegree_coprime

L125 ↗
ClassFormation.FiniteGaloisSubextension.abstractReciprocity_sylow_intermediateDegree_coprime
Documentation

Hence the actual degree [M:K] is prime to the chosen Sylow prime p, as asserted.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem abstractReciprocity_sylow_intermediateDegree_coprime
    (L : FiniteGaloisSubextension K) {p : ℕ} [Fact p.Prime]
    (P : Sylow p L.extensionQuotient) :
    Nat.Coprime
      (L.intermediateFiniteAbstractExtension
        (P : Subgroup L.extensionQuotient)).degree p
theorem

sylowAddSubgroup_le_nsmul_range_of_coprime

L144 ↗
ClassFormation.FiniteGaloisSubextension.sylowAddSubgroup_le_nsmul_range_of_coprime
Documentation

Let S be a Sylow p-subgroup of an abelian group B. If n is prime to p, then S lies in the range of the additive n-fold map on B.

The proof follows the sentence literally: S has p-power order, so the n-fold map is a bijection on S; a preimage in S is in particular a preimage in B.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem sylowAddSubgroup_le_nsmul_range_of_coprime
    {B : Type*} [AddCommGroup B]
    {p n : ℕ} [Fact p.Prime]
    (S : Sylow p (Multiplicative B)) (hn : Nat.Coprime n p) :
    Subgroup.toAddSubgroup'
        (S : Subgroup (Multiplicative B)) ≤
      (nsmulAddMonoidHom (α := B) n).range
theorem

abstractReciprocity_sylowAddSubgroup_le_intermediateDegree_nsmul_range

L164 ↗
ClassFormation.FiniteGaloisSubextension.abstractReciprocity_sylowAddSubgroup_le_intermediateDegree_nsmul_range
Documentation

The exact specialization: for M = L^P, every Sylow p-subgroup of an abelian group B lies in the image of the [M:K]-fold map on B. This is the group-theoretic input which the identity N_{M/K} ∘ i = [M:K] later converts into norm-map containment.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem abstractReciprocity_sylowAddSubgroup_le_intermediateDegree_nsmul_range
    (L : FiniteGaloisSubextension K) {p : ℕ} [Fact p.Prime]
    (P : Sylow p L.extensionQuotient)
    {B : Type*} [AddCommGroup B]
    (S : Sylow p (Multiplicative B)) :
    Subgroup.toAddSubgroup'
        (S : Subgroup (Multiplicative B)) ≤
      (nsmulAddMonoidHom (α := B)
        (L.intermediateFiniteAbstractExtension
          (P : Subgroup L.extensionQuotient)).degree).range

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.