Module

FiniteRamifiedPrimes.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.FiniteRamifiedPrimes

3 declarations indexed from sourceView source ↗

Module documentation

Finiteness of ramified primes in Dedekind extensions

In a finite separable extension of Dedekind domains, only finitely many height-one primes of either the extension ring or the base ring ramify.

Imports2

Mathlib.RingTheory.DedekindDomain.Different
Mathlib.RingTheory.DedekindDomain.Factorization

Imported by7

def

heightOnePrimeBelow

L35 ↗

AlgebraicNumberTheory.Ramification.heightOnePrimeBelow

Documentation

The height-one prime of the base lying below a height-one prime of a finite Dedekind extension.

Source context 9 commands

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

noncomputable section
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace AlgebraicNumberTheory.Ramification
variable (A B : Type*)
variable [CommRing A] [CommRing B] [Algebra A B]
variable [IsDedekindDomain A] [IsDedekindDomain B]
variable [Module.IsTorsionFree A B] [Module.Finite A B]
variable [Algebra.IsSeparable (FractionRing A) (FractionRing B)]
variable {A B}

Lean source · full declaration

def heightOnePrimeBelow (w : IsDedekindDomain.HeightOneSpectrum B) :
    IsDedekindDomain.HeightOneSpectrum A where
  asIdeal := w.asIdeal.under A
  isPrime := inferInstance
  ne_bot := by
    have : Algebra.IsIntegral A B := Algebra.IsIntegral.of_finite A B
    exact mt Ideal.eq_bot_of_under_eq_bot w.ne_bot

theorem

finite_ramified_heightOne_primes

L47 ↗

AlgebraicNumberTheory.Ramification.finite_ramified_heightOne_primes

Documentation

Only finitely many height-one primes of a finite separable Dedekind extension ramify over the base.

Source context 10 commands

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

noncomputable section
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace AlgebraicNumberTheory.Ramification
variable (A B : Type*)
variable [CommRing A] [CommRing B] [Algebra A B]
variable [IsDedekindDomain A] [IsDedekindDomain B]
variable [Module.IsTorsionFree A B] [Module.Finite A B]
variable [Algebra.IsSeparable (FractionRing A) (FractionRing B)]
variable {A B}
variable (A B)

Lean source · statement

theorem finite_ramified_heightOne_primes :
    {v : IsDedekindDomain.HeightOneSpectrum B |
        ¬ Algebra.IsUnramifiedAt A v.asIdeal}.Finite

theorem

finite_ramified_base_heightOne_primes

L58 ↗

AlgebraicNumberTheory.Ramification.finite_ramified_base_heightOne_primes

Documentation

Only finitely many height-one primes of the base ramify in a finite separable Dedekind extension.

Source context 10 commands

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

noncomputable section
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra
namespace AlgebraicNumberTheory.Ramification
variable (A B : Type*)
variable [CommRing A] [CommRing B] [Algebra A B]
variable [IsDedekindDomain A] [IsDedekindDomain B]
variable [Module.IsTorsionFree A B] [Module.Finite A B]
variable [Algebra.IsSeparable (FractionRing A) (FractionRing B)]
variable {A B}
variable (A B)

Lean source · statement

theorem finite_ramified_base_heightOne_primes :
    {v : IsDedekindDomain.HeightOneSpectrum A |
        ∃ w : IsDedekindDomain.HeightOneSpectrum B,
          w.asIdeal.LiesOver v.asIdeal ∧ ¬ Algebra.IsUnramifiedAt A w.asIdeal}.Finite

Module documentation

Finiteness of ramified primes in Dedekind extensions

Declarations

heightOnePrimeBelow

finite_ramified_heightOne_primes

finite_ramified_base_heightOne_primes