Module

CofinitelySplitFiniteExtension.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Cohomology.CofinitelySplitFiniteExtension

2 declarations indexed from sourceView source ↗

Module documentation

Cofinitely split finite extensions are trivial

For a finite extension of number fields L / K, if all but finitely many finite places of K split completely in L, then L / K has degree one. The normal-closure and splitting-transport constructions used in the proof live in their general algebraic-number-theory modules; this file contains only the global class-field-theoretic conclusion.

Imports4

Imported by2

theorem

finrank_eq_one_of_finite_nonSplittingPlaces

L47 ↗

GlobalClassFieldTheory.Cohomology.finrank_eq_one_of_finite_nonSplittingPlaces

Documentation

If all but finitely many finite places of K split completely in the finite extension L / K, then the extension has degree one.

The proof passes to the finite normal closure M. If M / K were nontrivial, a prime-order automorphism would give an intermediate field K' for which M / K' is cyclic of prime degree. The infinitude of full-decomposition places in cyclic prime-degree extensions then supplies infinitely many nonsplitting places of K', contradicting the finiteness transported from M / K.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Cohomology
variable
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]

Lean source · statement

theorem finrank_eq_one_of_finite_nonSplittingPlaces
    (hfinite :
      {v : HeightOneSpectrum (𝓞 K) |
        ¬ FinitePlaceSplitsCompletelyInExtension
          (K := K) (E := L) v}.Finite) :
    Module.finrank K L = 1

def

algEquivBaseOfFiniteNonSplittingPlaces

L129 ↗

GlobalClassFieldTheory.Cohomology.algEquivBaseOfFiniteNonSplittingPlaces