Module

FinitePlace.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.Splitting.FinitePlace

15 declarations indexed from sourceView source ↗

Module documentation

Decomposition groups and complete splitting at finite places

For a finite Galois extension of number fields L / K, this file attaches an actual decomposition subgroup to every finite place of K. The extension of the adic absolute value is the one constructed in LocalNormApproximation; no place above v is supplied as an additional hypothesis.

The stabilizer is identified with the automorphism group of the algebraic localization. The finite-localization theorem supplies finite dimensionality, so the order of the decomposition group is exactly the local degree. Consequently complete splitting is equivalent both to cardinality one and to local degree one.

Imports2

Imported by10

def

finitePlaceDecompositionGroup

L45 ↗

Documentation

The actual decomposition subgroup at the chosen extension of the finite place v.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def finitePlaceDecompositionGroup
    (v : HeightOneSpectrum (𝓞 K)) :
    Subgroup (L ≃ₐ[K] L)

def

FinitePlaceSplitsCompletely

L55 ↗

Documentation

A finite place splits completely when its chosen decomposition subgroup is trivial. Conjugacy of extensions makes this independent of the chosen extension, but the chosen representative gives a concrete subgroup for subsequent constructions.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def FinitePlaceSplitsCompletely
    (v : HeightOneSpectrum (𝓞 K)) : Prop

theorem

mem_finitePlaceDecompositionGroup_iff

L64 ↗

Documentation

Membership in the finite-place decomposition group is exactly stabilization of the chosen extension of the absolute value.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem mem_finitePlaceDecompositionGroup_iff
    (v : HeightOneSpectrum (𝓞 K))
    (σ : L ≃ₐ[K] L) :
    σ ∈ finitePlaceDecompositionGroup
        (K := K) (L := L) v ↔
      absoluteValueExtensionConjugate
          (NumberField.HeightOneSpectrum.adicAbv K v)
          (chosenFinitePlaceExtension (L := L) v) σ =
        chosenFinitePlaceExtension (L := L) v

def

finitePlaceLocalDegree

L81 ↗

Documentation

The local degree at v, defined using the actual algebraic localization selected above.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def finitePlaceLocalDegree
    (v : HeightOneSpectrum (𝓞 K)) : ℕ

theorem

finitePlaceDecompositionGroup_card_eq_localDegree

L100 ↗

Documentation

The decomposition-group localization equivalence together with the finite-localization theorem the finite-localization theorem: the order of the decomposition group equals the local degree.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceDecompositionGroup_card_eq_localDegree
    (v : HeightOneSpectrum (𝓞 K)) :
    Nat.card
        (finitePlaceDecompositionGroup
          (K := K) (L := L) v) =
      finitePlaceLocalDegree
        (K := K) (L := L) v

theorem

finitePlaceSplitsCompletely_iff_card_eq_one

L147 ↗

Documentation

A finite place splits completely exactly when its decomposition group has one element.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem finitePlaceSplitsCompletely_iff_card_eq_one
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePlaceSplitsCompletely
        (K := K) (L := L) v ↔
      Nat.card
          (finitePlaceDecompositionGroup
            (K := K) (L := L) v) = 1

theorem

finitePlaceSplitsCompletely_iff_localDegree_eq_one

L160 ↗

Documentation

Complete splitting is equivalent to local degree one.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlaceSplitsCompletely_iff_localDegree_eq_one
    (v : HeightOneSpectrum (𝓞 K)) :
    FinitePlaceSplitsCompletely
        (K := K) (L := L) v ↔
      finitePlaceLocalDegree
          (K := K) (L := L) v = 1

theorem

finitePlace_not_splitsCompletely_iff_exists_nontrivial_stabilizer

L172 ↗

Documentation

A finite place fails to split completely exactly when its decomposition group contains a nonidentity automorphism.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem finitePlace_not_splitsCompletely_iff_exists_nontrivial_stabilizer
    (v : HeightOneSpectrum (𝓞 K)) :
    ¬ FinitePlaceSplitsCompletely
        (K := K) (L := L) v ↔
      ∃ σ : L ≃ₐ[K] L,
        absoluteValueExtensionConjugate
            (NumberField.HeightOneSpectrum.adicAbv K v)
            (chosenFinitePlaceExtension (L := L) v) σ =
          chosenFinitePlaceExtension (L := L) v ∧
        σ ≠ 1

theorem

finitePlace_not_splitsCompletely_iff_one_lt_card

L213 ↗

Documentation

Nonsplitting is equivalently strict positivity above one of the decomposition-group order.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlace_not_splitsCompletely_iff_one_lt_card
    (v : HeightOneSpectrum (𝓞 K)) :
    ¬ FinitePlaceSplitsCompletely
        (K := K) (L := L) v ↔
      1 < Nat.card
          (finitePlaceDecompositionGroup
            (K := K) (L := L) v)

theorem

finitePlace_not_splitsCompletely_iff_one_lt_localDegree

L226 ↗

Documentation

Nonsplitting is equivalently local degree greater than one.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlace_not_splitsCompletely_iff_one_lt_localDegree
    (v : HeightOneSpectrum (𝓞 K)) :
    ¬ FinitePlaceSplitsCompletely
        (K := K) (L := L) v ↔
      1 < finitePlaceLocalDegree
          (K := K) (L := L) v

theorem

finitePlace_not_splitsCompletely_of_decompositionGroup_eq_top

L239 ↗

Documentation

In a nontrivial finite Galois extension, a place whose decomposition group is the whole Galois group cannot split completely. This bridges the cyclic prime-power criterion, where "nonsplit" means full decomposition group, and the normal-closure criterion.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem finitePlace_not_splitsCompletely_of_decompositionGroup_eq_top
    (hdegree : 1 < Module.finrank K L)
    (v : HeightOneSpectrum (𝓞 K))
    (hfull :
      finitePlaceDecompositionGroup
          (K := K) (L := L) v = ⊤) :
    ¬ FinitePlaceSplitsCompletely
        (K := K) (L := L) v

theorem

absoluteValueDecompositionGroup_eq_bot_over_intermediate

L273 ↗

Documentation

Complete splitting of a valuation over K remains complete after enlarging the base to an intermediate field M.

This is the subgroup-intersection criterion, combined with injectivity of scalar restriction.

Source context 10 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section IntermediateField
variable {M : Type}
    [Field M] [Algebra K M] [Algebra M L]
    [IsScalarTower K M L]
omit [NumberField K] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem absoluteValueDecompositionGroup_eq_bot_over_intermediate
    (w : AbsoluteValue L ℝ)
    (hsplit :
      absoluteValueDecompositionGroup K w = ⊥) :
    absoluteValueDecompositionGroup M w = ⊥

def

finitePlaceDecompositionGroupInQuotient

L293 ↗

Documentation

The image of the finite-place decomposition subgroup in a group quotient. In the Galois correspondence this is the decomposition group in the corresponding intermediate extension.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Quotient

Lean source · statement

def finitePlaceDecompositionGroupInQuotient
    (v : HeightOneSpectrum (𝓞 K))
    (P : Subgroup (L ≃ₐ[K] L))
    [P.Normal] :
    Subgroup ((L ≃ₐ[K] L) ⧸ P)

theorem

finitePlaceDecompositionGroupInQuotient_eq_bot_iff

L305 ↗

Documentation

The quotient decomposition group is trivial exactly when the original decomposition group is contained in the quotient kernel.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Quotient
omit [FiniteDimensional K L] in

Lean source · statement

theorem finitePlaceDecompositionGroupInQuotient_eq_bot_iff
    (v : HeightOneSpectrum (𝓞 K))
    (P : Subgroup (L ≃ₐ[K] L))
    [P.Normal] :
    finitePlaceDecompositionGroupInQuotient
        (K := K) (L := L) v P = ⊥ ↔
      finitePlaceDecompositionGroup
          (K := K) (L := L) v ≤ P

theorem

finitePlace_exists_index_prime_quotient_of_decompositionGroup_ne_top

L322 ↗

Documentation

In a cyclic extension of prime-power degree, every proper finite-place decomposition group is contained in a normal subgroup of index p; the resulting order-p quotient has trivial decomposition image. This is the group/prime bridge used in the cyclic prime-power splitting argument.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Quotient

Lean source · statement

theorem finitePlace_exists_index_prime_quotient_of_decompositionGroup_ne_top
    [IsCyclic (L ≃ₐ[K] L)]
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K))
    (hproper :
      finitePlaceDecompositionGroup
          (K := K) (L := L) v ≠ ⊤) :
    ∃ P : Subgroup (L ≃ₐ[K] L),
      finitePlaceDecompositionGroup
          (K := K) (L := L) v ≤ P ∧
      P.index = p ∧
      P.Normal ∧
      Nat.card ((L ≃ₐ[K] L) ⧸ P) = p ∧
      finitePlaceDecompositionGroupInQuotient
          (K := K) (L := L) v P = ⊥

Module documentation

Decomposition groups and complete splitting at finite places

Declarations