Module

CyclicPrimeSubextension.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.CyclicPrimeSubextension

25 declarations indexed from sourceView source ↗

Module documentation

The prime-degree subextension of a cyclic prime-power extension

This file constructs a prime-degree intermediate field. For a nontrivial cyclic Galois extension whose group has order p ^ exponent, the index-p subgroup constructed in SplittingGroupTheory is sent through the finite Galois correspondence. Its fixed field is an actual cyclic Galois extension of the base of degree p.

The finite-place decomposition group in that subextension is obtained by restricting the decomposition group of L / K. Thus complete splitting descends to the prime-degree subextension, and nonsplitting there ascends to L.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.Splitting.FinitePlace

Imported by9

def

restrictAbsoluteValueExtensionToIntermediate

L42 ↗

Documentation

Restrict an actual extension of an absolute value to an intermediate field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section ValuationRestriction
variable {F E : Type}
    [Field F] [Field E] [Algebra F E]

Lean source · full declaration

def restrictAbsoluteValueExtensionToIntermediate
    (vF : AbsoluteValue F ℝ)
    (w : AbsoluteValueExtension vF E)
    (M : IntermediateField F E) :
    AbsoluteValueExtension vF M where
  val :=
    w.1.comp (f := M.val.toRingHom)
      M.val.injective
  property x := by
    change w.1 (algebraMap F E x) = vF x
    exact w.2 x

theorem

restrictAbsoluteValueExtensionToIntermediate_apply

L55 ↗

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section ValuationRestriction
variable {F E : Type}
    [Field F] [Field E] [Algebra F E]

Lean source · statement

theorem restrictAbsoluteValueExtensionToIntermediate_apply
    (vF : AbsoluteValue F ℝ)
    (w : AbsoluteValueExtension vF E)
    (M : IntermediateField F E)
    (x : M) :
    (restrictAbsoluteValueExtensionToIntermediate
      vF w M).1 x = w.1 x

def

absoluteValueExtensionOverIntermediate

L66 ↗

Documentation

Regard the original extension as an extension of its restriction to an intermediate field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section ValuationRestriction
variable {F E : Type}
    [Field F] [Field E] [Algebra F E]

Lean source · full declaration

def absoluteValueExtensionOverIntermediate
    (vF : AbsoluteValue F ℝ)
    (w : AbsoluteValueExtension vF E)
    (M : IntermediateField F E) :
    AbsoluteValueExtension
      (restrictAbsoluteValueExtensionToIntermediate
        vF w M).1 E where
  val := w.1
  property _ := rfl

theorem

restrictAbsoluteValueExtensionToIntermediate_isNontrivial

L78 ↗

Documentation

Restriction of an extension of a nontrivial absolute value remains nontrivial.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section ValuationRestriction
variable {F E : Type}
    [Field F] [Field E] [Algebra F E]

Lean source · statement

theorem restrictAbsoluteValueExtensionToIntermediate_isNontrivial
    (vF : AbsoluteValue F ℝ)
    (hvF : vF.IsNontrivial)
    (w : AbsoluteValueExtension vF E)
    (M : IntermediateField F E) :
    (restrictAbsoluteValueExtensionToIntermediate
      vF w M).1.IsNontrivial

theorem

absoluteValueDecompositionGroup_map_restrictNormalHom

L100 ↗

Documentation

For a normal subextension represented by a field type, its decomposition group is the restriction image of the decomposition group upstairs.

The reverse inclusion uses valuation-extension counting over the subextension: a lift of a valuation-preserving automorphism is corrected by an automorphism fixing that field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section ValuationRestriction
variable {F E : Type}
    [Field F] [Field E] [Algebra F E]

Lean source · statement

theorem absoluteValueDecompositionGroup_map_restrictNormalHom
    {M : Type*}
    [Field M] [Algebra F M] [Algebra M E]
    [IsScalarTower F M E]
    [IsGalois F E]
    [Normal F M]
    (vF : AbsoluteValue F ℝ)
    (hvF : vF.IsNontrivial)
    (w : AbsoluteValueExtension vF E) :
    (absoluteValueDecompositionGroup F w.1).map
        (AlgEquiv.restrictNormalHom
          (F := F) (K₁ := E) M) =
      absoluteValueDecompositionGroup F
        (w.1.comp (f := algebraMap M E)
          (algebraMap M E).injective)

theorem

absoluteValueDecompositionGroup_eq_of_absoluteValue_isEquiv

L254 ↗

Documentation

Decomposition groups depend only on the valuation class.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section DecompositionGroupChoice
variable {F L : Type*}
    [Field F] [Field L] [Algebra F L]

Lean source · statement

theorem absoluteValueDecompositionGroup_eq_of_absoluteValue_isEquiv
    (w w' : AbsoluteValue L ℝ)
    (hww' : w.IsEquiv w') :
    absoluteValueDecompositionGroup F w =
      absoluteValueDecompositionGroup F w'

theorem

absoluteValueDecompositionGroup_conjugate_eq_of_isMulCommutative

L275 ↗

Documentation

In an abelian Galois extension, conjugating an exact extension does not change its decomposition subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section DecompositionGroupChoice
variable {F L : Type*}
    [Field F] [Field L] [Algebra F L]

Lean source · statement

theorem absoluteValueDecompositionGroup_conjugate_eq_of_isMulCommutative
    [IsMulCommutative (L ≃ₐ[F] L)]
    (vF : AbsoluteValue F ℝ)
    (w : AbsoluteValueExtension vF L)
    (ρ : L ≃ₐ[F] L) :
    absoluteValueDecompositionGroup F
        (absoluteValueExtensionConjugate
          vF w ρ).1 =
      absoluteValueDecompositionGroup F w.1

theorem

absoluteValueDecompositionGroup_eq_of_exactExtensions_of_isMulCommutative

L314 ↗

Documentation

In an abelian Galois extension the decomposition subgroup is independent of the exact extension above the base place.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section DecompositionGroupChoice
variable {F L : Type*}
    [Field F] [Field L] [Algebra F L]

Lean source · statement

theorem absoluteValueDecompositionGroup_eq_of_exactExtensions_of_isMulCommutative
    [IsGalois F L]
    [IsMulCommutative (L ≃ₐ[F] L)]
    (vF : AbsoluteValue F ℝ)
    (hvF : vF.IsNontrivial)
    (w w' : AbsoluteValueExtension vF L) :
    absoluteValueDecompositionGroup F w.1 =
      absoluteValueDecompositionGroup F w'.1

theorem

absoluteValueDecompositionGroup_conjugate_eq_bot

L337 ↗

Documentation

Triviality of a decomposition group is preserved when the chosen extension is conjugated.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section ValuationRestriction
variable {F E : Type}
    [Field F] [Field E] [Algebra F E]

Lean source · statement

theorem absoluteValueDecompositionGroup_conjugate_eq_bot
    (vF : AbsoluteValue F ℝ)
    (w : AbsoluteValueExtension vF E)
    (ρ : E ≃ₐ[F] E)
    (hbot :
      absoluteValueDecompositionGroup F w.1 = ⊥) :
    absoluteValueDecompositionGroup F
        (absoluteValueExtensionConjugate
          vF w ρ).1 = ⊥

theorem

absoluteValueDecompositionGroup_eq_bot_independent_extension

L373 ↗

Documentation

For a Galois extension, triviality of the decomposition group is independent of the chosen extension of the base absolute value.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section ValuationRestriction
variable {F E : Type}
    [Field F] [Field E] [Algebra F E]

Lean source · statement

theorem absoluteValueDecompositionGroup_eq_bot_independent_extension
    [IsGalois F E]
    (vF : AbsoluteValue F ℝ)
    (hvF : vF.IsNontrivial)
    (w w' : AbsoluteValueExtension vF E)
    (hbot :
      absoluteValueDecompositionGroup F w.1 = ⊥) :
    absoluteValueDecompositionGroup F w'.1 = ⊥

theorem

exists_index_prime_normal_subgroup

L400 ↗

Documentation

A cyclic group of nonzero prime-power order has an actual normal subgroup of index p.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField K] [NumberField L] [IsGalois K L] in

Lean source · statement

theorem exists_index_prime_normal_subgroup
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    ∃ P : Subgroup (L ≃ₐ[K] L),
      P.index = p ∧
      P.Normal ∧
      Nat.card ((L ≃ₐ[K] L) ⧸ P) = p

def

cyclicPrimeIndexSubgroup

L430 ↗

Documentation

The chosen index-p subgroup of the global cyclic Galois group.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

def cyclicPrimeIndexSubgroup
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    Subgroup (L ≃ₐ[K] L)

theorem

cyclicPrimeIndexSubgroup_index

L443 ↗

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField K] [NumberField L] [IsGalois K L] in

Lean source · statement

theorem cyclicPrimeIndexSubgroup_index
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    (cyclicPrimeIndexSubgroup
      (K := K) (L := L)
      hp hexponent hcard).index = p

theorem

cyclicPrimeIndexSubgroup_normal

L458 ↗

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField K] [NumberField L] [IsGalois K L] in

Lean source · statement

theorem cyclicPrimeIndexSubgroup_normal
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    (cyclicPrimeIndexSubgroup
      (K := K) (L := L)
      hp hexponent hcard).Normal

theorem

cyclicPrimeIndexSubgroup_quotient_card

L473 ↗

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField K] [NumberField L] [IsGalois K L] in

Lean source · statement

theorem cyclicPrimeIndexSubgroup_quotient_card
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    Nat.card
        ((L ≃ₐ[K] L) ⧸
          cyclicPrimeIndexSubgroup
            (K := K) (L := L)
            hp hexponent hcard) =
      p

def

cyclicPrimeSubextension

L491 ↗

Documentation

The actual degree-p intermediate field in the cyclic prime-power reduction.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

def cyclicPrimeSubextension
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    IntermediateField K L

instance

cyclicPrimeSubextension_isGalois

L506 ↗

Documentation

The constructed intermediate extension is Galois over K.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField K] [NumberField L] in

Lean source · statement

instance cyclicPrimeSubextension_isGalois
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    IsGalois K
      (cyclicPrimeSubextension
        (K := K) (L := L)
        hp hexponent hcard)

theorem

cyclicPrimeSubextension_finrank

L530 ↗

Documentation

The constructed intermediate extension has degree exactly p.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField K] [NumberField L] in

Lean source · statement

theorem cyclicPrimeSubextension_finrank
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    Module.finrank K
        (cyclicPrimeSubextension
          (K := K) (L := L)
          hp hexponent hcard) =
      p

theorem

cyclicPrimeSubextension_isCyclic

L573 ↗

Documentation

The Galois group of the constructed degree-p extension is cyclic.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField K] [NumberField L] in

Lean source · statement

theorem cyclicPrimeSubextension_isCyclic
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent) :
    IsCyclic
      (cyclicPrimeSubextension
          (K := K) (L := L)
          hp hexponent hcard ≃ₐ[K]
        cyclicPrimeSubextension
          (K := K) (L := L)
          hp hexponent hcard)

def

cyclicPrimeSubextensionDecompositionGroup

L606 ↗

Documentation

The decomposition subgroup in the constructed subextension, obtained by restricting the decomposition subgroup in L / K.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

def cyclicPrimeSubextensionDecompositionGroup
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K)) :
    Subgroup
      (cyclicPrimeSubextension
          (K := K) (L := L)
          hp hexponent hcard ≃ₐ[K]
        cyclicPrimeSubextension
          (K := K) (L := L)
          hp hexponent hcard)

theorem

cyclicPrimeSubextensionDecompositionGroup_eq_quotient_image

L638 ↗

Documentation

The restricted decomposition group agrees with the quotient decomposition group transported by the fixed-field Galois correspondence.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField L] in

Lean source · statement

theorem cyclicPrimeSubextensionDecompositionGroup_eq_quotient_image
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K)) :
    cyclicPrimeSubextensionDecompositionGroup
        (K := K) (L := L)
        hp hexponent hcard v =
      (finitePlaceDecompositionGroupInQuotient
        (K := K) (L := L) v
        (cyclicPrimeIndexSubgroup
          (K := K) (L := L)
          hp hexponent hcard)).map
        (IsGalois.normalAutEquivQuotient
          (cyclicPrimeIndexSubgroup
            (K := K) (L := L)
            hp hexponent hcard)).toMonoidHom

theorem

finitePlaceSplitsCompletely_in_cyclicPrimeSubextension

L688 ↗

Documentation

Complete splitting in L implies complete splitting in the constructed prime-degree subextension.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField L] in

Lean source · statement

theorem finitePlaceSplitsCompletely_in_cyclicPrimeSubextension
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    cyclicPrimeSubextensionDecompositionGroup
        (K := K) (L := L)
        hp hexponent hcard v = ⊥

theorem

finitePlaceSplitsCompletely_in_cyclicPrimeSubextension_actual

L714 ↗

Documentation

Complete splitting in L implies complete splitting, in the standard chosen-extension sense, in the actual fixed intermediate field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField L] in

Lean source · statement

theorem finitePlaceSplitsCompletely_in_cyclicPrimeSubextension_actual
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K))
    (hsplit :
      FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    FinitePlaceSplitsCompletely
      (K := K)
      (L := cyclicPrimeSubextension
        (K := K) (L := L)
        hp hexponent hcard) v

theorem

finitePlace_not_splitsCompletely_of_not_in_cyclicPrimeSubextension_actual

L773 ↗

Documentation

Contrapositive in the standard chosen-extension sense: a place nonsplit in the constructed degree-p field is nonsplit in L.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField L] in

Lean source · statement

theorem finitePlace_not_splitsCompletely_of_not_in_cyclicPrimeSubextension_actual
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K))
    (hnonsplit :
      ¬ FinitePlaceSplitsCompletely
        (K := K)
        (L := cyclicPrimeSubextension
          (K := K) (L := L)
          hp hexponent hcard) v) :
    ¬ FinitePlaceSplitsCompletely
        (K := K) (L := L) v

theorem

finitePlace_not_splitsCompletely_of_not_in_cyclicPrimeSubextension

L799 ↗

Documentation

Contrapositive form: a finite place nonsplit in the prime-degree subextension is already nonsplit in L.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField L] in

Lean source · statement

theorem finitePlace_not_splitsCompletely_of_not_in_cyclicPrimeSubextension
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard :
      Nat.card (L ≃ₐ[K] L) =
        p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K))
    (hnonsplit :
      cyclicPrimeSubextensionDecompositionGroup
          (K := K) (L := L)
          hp hexponent hcard v ≠ ⊥) :
    ¬ FinitePlaceSplitsCompletely
        (K := K) (L := L) v

Module documentation

The prime-degree subextension of a cyclic prime-power extension

Declarations