NYLL
Module

Core.lean

Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitPreparation.Core
4 declarations indexed from sourceView source ↗

Module documentation

Rank and kernel coordinates for S-unit preparation

The endpoint of the S-unit preparation construction: the rank bound, the exact restriction-kernel cardinality, and prime-power coordinates.

Imports6
Imported by3

Declarations

theorem

galoisRank_le_totalPlaceCard_enlargedS

L37 ↗
KummerTheory.galoisRank_le_totalPlaceCard_enlargedS
Documentation

The cardinal comparison in the finite S-unit preparation argument: if Gal(E/K) ≃ (Z/nZ)^r, then r ≤ s for the source-produced enlarged set of places.

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 galoisRank_le_totalPlaceCard_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 : ℕ+) (hn : 1 < (n : ℕ))
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    r ≤
      totalPlaceCard (K := K)
        (enlargeByFiniteKummerRadicalSupport
          (K := K) (L := E) n hmu S)
theorem

card_enlargedSUnitKummerRestrictionHom_ker

L95 ↗
KummerTheory.card_enlargedSUnitKummerRestrictionHom_ker
Documentation

The restriction kernel in the finite S-unit preparation argument has the expected cardinality n ^ (s - r). Both fields and the restriction map are the concrete objects constructed 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
theorem card_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 : ℕ+) (hn : 1 < (n : ℕ))
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Nat.card
        (enlargedSUnitKummerRestrictionHom
          (K := K) (Omega := Omega) E n hmu
          (galois_pow_eq_one_of_equiv_pi_zmod E n r eG)
          S).ker =
      (n : ℕ) ^
        (totalPlaceCard (K := K)
            (enlargeByFiniteKummerRadicalSupport
              (K := K) (L := E) n hmu S) - r)
theorem

exists_enlargedSUnitKummerRestrictionKernelEquivPiZMod

L185 ↗
KummerTheory.exists_enlargedSUnitKummerRestrictionKernelEquivPiZMod
Documentation

In the prime-power case, the actual relative Galois group Gal(N/E) is a free ZMod n-module of rank s - r. This is the concrete basis source used to choose the fields N_i in 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
theorem
    exists_enlargedSUnitKummerRestrictionKernelEquivPiZMod
    {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)
    (p v : ℕ) (hp : p.Prime) (hv : 0 < v)
    (hn : (n : ℕ) = p ^ v)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Nonempty
      ((enlargedSUnitKummerRestrictionHom
          (K := K) (Omega := Omega) E n hmu
          (galois_pow_eq_one_of_equiv_pi_zmod E n r eG)
          S).ker ≃*
        (Fin
            (totalPlaceCard (K := K)
              (enlargeByFiniteKummerRadicalSupport
                (K := K) (L := E) n hmu S) - r) →
          Multiplicative (ZMod (n : ℕ))))
def

chosenEnlargedSUnitKummerRestrictionKernelEquivPiZMod

L280 ↗
KummerTheory.chosenEnlargedSUnitKummerRestrictionKernelEquivPiZMod
Documentation

A chosen coordinate equivalence for the actual relative Galois group in 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
    chosenEnlargedSUnitKummerRestrictionKernelEquivPiZMod
    {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)
    (p v : ℕ) (hp : p.Prime) (hv : 0 < v)
    (hn : (n : ℕ) = p ^ v)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (enlargedSUnitKummerRestrictionHom
        (K := K) (Omega := Omega) E n hmu
        (galois_pow_eq_one_of_equiv_pi_zmod E n r eG)
        S).ker ≃*
      (Fin
          (totalPlaceCard (K := K)
            (enlargeByFiniteKummerRadicalSupport
              (K := K) (L := E) n hmu S) - r) →
        Multiplicative (ZMod (n : ℕ)))

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