Module

CompletelySplitFinset.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.CompletelySplitFinset

1 declaration indexed from sourceView source ↗

Module documentation

A finite set of primes witnessing complete splitting

The Galois orbit of the centre of one actual extended finite place is free when the rational prime splits completely. Its prime ideals form a finite set of cardinality equal to the number-field degree.

Imports7

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.CompletelySplitPrimes
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.Splitting.FinitePlaceIdeal
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.ExtensionIndex
Nyll.ClassFieldTheory.AlgebraicNumberTheory.SUnit.GaloisAction
Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Mathlib.RingTheory.Ideal.Maps
Mathlib.Data.Finset.Card

Imported by2

theorem

exists_finset_maximalIdeals_of_finitePlaceSplitsCompletely

L30 ↗

AlgebraicNumberTheory.PrimeSelection.exists_finset_maximalIdeals_of_finitePlaceSplitsCompletely

Documentation

A completely split rational prime gives exactly a field-degree-sized finite set of distinct maximal ideals containing that rational prime.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem exists_finset_maximalIdeals_of_finitePlaceSplitsCompletely
    (F : Type) [Field F] [NumberField F] [IsGalois ℚ F]
    (q : Nat.Primes)
    (hsplit : FinitePlaceSplitsCompletely (K := ℚ) (L := F)
      ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q)) :
    ∃ factors : Finset (Ideal (𝓞 F)),
      factors.card = Module.finrank ℚ F ∧
        ∀ P ∈ factors, P.IsMaximal ∧ (q.val : 𝓞 F) ∈ P

Module documentation

A finite set of primes witnessing complete splitting

Declarations

exists_finset_maximalIdeals_of_finitePlaceSplitsCompletely