Module

EnlargedSUnitRestriction.lean

Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitPreparation.EnlargedSUnitRestriction

16 declarations indexed from sourceView source ↗

Module documentation

Restriction from an enlarged S-unit Kummer extension

The concrete embedding and Galois restriction map, its fixing subgroup, and the cyclic fixed fields attached to kernel elements.

Imports2

Imported by2

theorem

le_fullSUnitKummerExtension_of_enlargedS

L32 ↗

KummerTheory.le_fullSUnitKummerExtension_of_enlargedS

Documentation

The actual field containment L ≤ N for finite S-unit preparation, after producing the required finite enlargement of S.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem le_fullSUnitKummerExtension_of_enlargedS
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    E ≤
      fullSUnitKummerExtension
        (K := K) (Omega := Omega) n
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := E) n hmu S)

def

enlargedSUnitKummerAlgebra

L64 ↗

KummerTheory.enlargedSUnitKummerAlgebra

Documentation

The actual inclusion algebra E → N supplied by the source-produced containment above.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

def enlargedSUnitKummerAlgebra
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Algebra E
      (fullSUnitKummerExtension
        (K := K) (Omega := Omega) n
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := E) n hmu S))

def

enlargedSUnitKummerRestrictionHom

L85 ↗

KummerTheory.enlargedSUnitKummerRestrictionHom

Documentation

Restriction from the full S-unit Kummer extension N to the actual extension E ≤ N produced above.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

def enlargedSUnitKummerRestrictionHom
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Gal(fullSUnitKummerExtension
          (K := K) (Omega := Omega) n
          (enlargeByFiniteKummerRadicalSupport
            (K := K) (L := E) n hmu S)/K) →*
      Gal(E/K)

theorem

enlargedSUnitKummerRestrictionHom_surjective

L114 ↗

KummerTheory.enlargedSUnitKummerRestrictionHom_surjective

Documentation

The restriction map Gal(N/K) → Gal(E/K) is onto.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem enlargedSUnitKummerRestrictionHom_surjective
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Surjective
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu hexponent S)

def

enlargedSUnitKummerEmbeddedExtension

L147 ↗

KummerTheory.enlargedSUnitKummerEmbeddedExtension

Documentation

The actual embedded copy of E inside the full S-unit Kummer extension N.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

def enlargedSUnitKummerEmbeddedExtension
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    IntermediateField K
      (fullSUnitKummerExtension
        (K := K) (Omega := Omega) n
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := E) n hmu S))

theorem

enlargedSUnitKummerRestrictionHom_ker_eq_fixingSubgroup

L175 ↗

KummerTheory.enlargedSUnitKummerRestrictionHom_ker_eq_fixingSubgroup

Documentation

The kernel of restriction is precisely the subgroup fixing the concrete embedded copy of E in N.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem enlargedSUnitKummerRestrictionHom_ker_eq_fixingSubgroup
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (enlargedSUnitKummerRestrictionHom
      (K := K) (Omega := Omega) E n hmu hexponent S).ker =
      (enlargedSUnitKummerEmbeddedExtension
        (K := K) (Omega := Omega) E n hmu
        hexponent S).fixingSubgroup

theorem

fixedField_enlargedSUnitKummerRestrictionHom_ker

L238 ↗

KummerTheory.fixedField_enlargedSUnitKummerRestrictionHom_ker

Documentation

The field fixed by the concrete restriction kernel is exactly the embedded copy of E.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem fixedField_enlargedSUnitKummerRestrictionHom_ker
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    IntermediateField.fixedField
        (enlargedSUnitKummerRestrictionHom
          (K := K) (Omega := Omega) E n hmu
          hexponent S).ker =
      enlargedSUnitKummerEmbeddedExtension
        (K := K) (Omega := Omega) E n hmu
        hexponent S

def

enlargedSUnitKummerCyclicFixedField

L282 ↗

KummerTheory.enlargedSUnitKummerCyclicFixedField

Documentation

For an element sigma of the relative Galois subgroup Gal(N/E), this is the actual cyclic fixed field N_sigma = N ^ ⟨sigma⟩ used in the prime construction of the finite S-unit preparation argument.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

def enlargedSUnitKummerCyclicFixedField
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker) :
    IntermediateField K
      (fullSUnitKummerExtension
        (K := K) (Omega := Omega) n
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := E) n hmu S))

theorem

enlargedSUnitKummerEmbeddedExtension_le_cyclicFixedField

L311 ↗

KummerTheory.enlargedSUnitKummerEmbeddedExtension_le_cyclicFixedField

Documentation

The embedded extension E lies in every cyclic fixed field attached to an element of Gal(N/E).

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem enlargedSUnitKummerEmbeddedExtension_le_cyclicFixedField
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker) :
    enlargedSUnitKummerEmbeddedExtension
        (K := K) (Omega := Omega) E n hmu
        hexponent S ≤
      enlargedSUnitKummerCyclicFixedField
        (K := K) (Omega := Omega) E n hmu
        hexponent S sigma

theorem

enlargedSUnitKummerCyclicFixedField_isGalois

L339 ↗

KummerTheory.enlargedSUnitKummerCyclicFixedField_isGalois

Documentation

The top Kummer field is Galois over each cyclic fixed field.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem enlargedSUnitKummerCyclicFixedField_isGalois
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker) :
    IsGalois
      (enlargedSUnitKummerCyclicFixedField
        (K := K) (Omega := Omega) E n hmu
        hexponent S sigma)
      (fullSUnitKummerExtension
        (K := K) (Omega := Omega) n
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := E) n hmu S))

theorem

enlargedSUnitKummerCyclicFixedField_finrank

L382 ↗

KummerTheory.enlargedSUnitKummerCyclicFixedField_finrank

Documentation

The relative degree of N/N_sigma is the order of sigma.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem enlargedSUnitKummerCyclicFixedField_finrank
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker) :
    Module.finrank
        (enlargedSUnitKummerCyclicFixedField
          (K := K) (Omega := Omega) E n hmu
          hexponent S sigma)
        (fullSUnitKummerExtension
          (K := K) (Omega := Omega) n
          (enlargeByFiniteKummerRadicalSupport
            (K := K) (L := E) n hmu S)) =
      orderOf
        (sigma :
          Gal(fullSUnitKummerExtension
            (K := K) (Omega := Omega) n
            (enlargeByFiniteKummerRadicalSupport
              (K := K) (L := E) n hmu S)/K))

theorem

enlargedSUnitKummerCyclicFixedField_isCyclic

L430 ↗

KummerTheory.enlargedSUnitKummerCyclicFixedField_isCyclic

Documentation

The relative Galois group Gal(N/N_sigma) is cyclic.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem enlargedSUnitKummerCyclicFixedField_isCyclic
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker) :
    IsCyclic
      ((fullSUnitKummerExtension
          (K := K) (Omega := Omega) n
          (enlargeByFiniteKummerRadicalSupport
            (K := K) (L := E) n hmu S)) ≃ₐ[
        enlargedSUnitKummerCyclicFixedField
          (K := K) (Omega := Omega) E n hmu
          hexponent S sigma]
        (fullSUnitKummerExtension
          (K := K) (Omega := Omega) n
          (enlargeByFiniteKummerRadicalSupport
            (K := K) (L := E) n hmu S)))

theorem

orderOf_enlargedSUnitKummerRestrictionKernel_dvd

L477 ↗

KummerTheory.orderOf_enlargedSUnitKummerRestrictionKernel_dvd

Documentation

The order of every relative automorphism divides the Kummer exponent n.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem orderOf_enlargedSUnitKummerRestrictionKernel_dvd
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker) :
    orderOf
        (sigma :
          Gal(fullSUnitKummerExtension
            (K := K) (Omega := Omega) n
            (enlargeByFiniteKummerRadicalSupport
              (K := K) (L := E) n hmu S)/K)) ∣
      (n : ℕ)

theorem

exists_orderOf_enlargedSUnitKummerRestrictionKernel_eq_prime_pow

L511 ↗

KummerTheory.exists_orderOf_enlargedSUnitKummerRestrictionKernel_eq_prime_pow

Documentation

If n = p^v, then the cyclic degree attached to every relative automorphism is a power of p.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem exists_orderOf_enlargedSUnitKummerRestrictionKernel_eq_prime_pow
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (p v : ℕ) (hp : p.Prime)
    (hn : (n : ℕ) = p ^ v)
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker) :
    ∃ k ≤ v,
      orderOf
          (sigma :
            Gal(fullSUnitKummerExtension
              (K := K) (Omega := Omega) n
              (enlargeByFiniteKummerRadicalSupport
                (K := K) (L := E) n hmu S)/K)) =
        p ^ k

theorem

enlargedSUnitKummerCyclicFixedField_ne_top

L544 ↗

KummerTheory.enlargedSUnitKummerCyclicFixedField_ne_top

Documentation

A nonidentity relative automorphism gives a genuinely nontrivial cyclic subextension.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem enlargedSUnitKummerCyclicFixedField_ne_top
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker)
    (hsigma :
      (sigma :
        Gal(fullSUnitKummerExtension
          (K := K) (Omega := Omega) n
          (enlargeByFiniteKummerRadicalSupport
            (K := K) (L := E) n hmu S)/K)) ≠ 1) :
    enlargedSUnitKummerCyclicFixedField
        (K := K) (Omega := Omega) E n hmu
        hexponent S sigma ≠ ⊤

theorem

exists_pos_orderOf_enlargedSUnitKummerRestrictionKernel_eq_prime_pow

L577 ↗

KummerTheory.exists_pos_orderOf_enlargedSUnitKummerRestrictionKernel_eq_prime_pow

Documentation

In the prime-power case, a nonidentity relative automorphism has order p^k with positive exponent.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]

Lean source · statement

theorem exists_pos_orderOf_enlargedSUnitKummerRestrictionKernel_eq_prime_pow
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hexponent : ∀ sigma : Gal(E/K), sigma ^ (n : ℕ) = 1)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (p v : ℕ) (hp : p.Prime)
    (hn : (n : ℕ) = p ^ v)
    (sigma :
      (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        hexponent S).ker)
    (hsigma :
      (sigma :
        Gal(fullSUnitKummerExtension
          (K := K) (Omega := Omega) n
          (enlargeByFiniteKummerRadicalSupport
            (K := K) (L := E) n hmu S)/K)) ≠ 1) :
    ∃ k, 0 < k ∧ k ≤ v ∧
      orderOf
          (sigma :
            Gal(fullSUnitKummerExtension
              (K := K) (Omega := Omega) n
              (enlargeByFiniteKummerRadicalSupport
                (K := K) (L := E) n hmu S)/K)) =
        p ^ k

Module documentation

Restriction from an enlarged S-unit Kummer extension

Declarations