NYLL
Module

PrimeContractions.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.PrimeContractions
19 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: number-field prime contractions

This file specializes the fixed fields Z_P and T_P to rings of integers of number fields and defines the contracted primes p, P_Z, and P_T.

Imports1
Imported by3

Declarations

theorem

ringOfIntegers_moduleFinite

L35 ↗
HilbertRamification.Dedekind.ringOfIntegers_moduleFinite
Documentation

Number-field ring-of-integers extensions are finite as modules. Mathlib keeps the corresponding Algebra.IsIntegral.finite conversion out of instance search, so the HRT number-field layer records the source explicitly.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
theorem ringOfIntegers_moduleFinite :
    Module.Finite (𝓞 K) (𝓞 L)
theorem

ringOfIntegers_under_ne_bot

L43 ↗
HilbertRamification.Dedekind.ringOfIntegers_under_ne_bot
Documentation

The contraction of a maximal finite prime of a number-field ring of integers to a subfield ring of integers is nonzero.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
theorem ringOfIntegers_under_ne_bot
    {E F : Type*} [Field E] [Field F] [NumberField E] [NumberField F]
    [Algebra E F] (P : Ideal (𝓞 F)) [P.IsMaximal] :
    P.under (𝓞 E) ≠ ⊥
abbrev

basePrime

L54 ↗
HilbertRamification.Dedekind.basePrime
Documentation

prime-decomposition theory: p = P ∩ O_K, the prime ideal of the base number field below P.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
abbrev basePrime
    (P : Ideal (𝓞 L)) :
    Ideal (𝓞 K)
instance

basePrime_isPrime

L60 ↗
HilbertRamification.Dedekind.basePrime_isPrime
Documentation

The contracted base prime is prime.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
instance basePrime_isPrime
    (P : Ideal (𝓞 L)) [P.IsPrime] :
    (basePrime (K := K) P).IsPrime
instance

basePrime_liesOver

L66 ↗
HilbertRamification.Dedekind.basePrime_liesOver
Documentation

The top prime lies over its contraction to the base ring of integers.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · full declaration
instance basePrime_liesOver
    (P : Ideal (𝓞 L)) :
    P.LiesOver (basePrime (K := K) P) where
  over := rfl
theorem

basePrime_ne_bot

L73 ↗
HilbertRamification.Dedekind.basePrime_ne_bot
Documentation

Prime-decomposition statement: for a finite prime P of O_L, its contraction to O_K is nonzero.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
theorem basePrime_ne_bot
    (P : Ideal (𝓞 L)) [P.IsMaximal] :
    basePrime (K := K) P ≠ ⊥
abbrev

decompositionFieldPrime

L80 ↗
HilbertRamification.Dedekind.decompositionFieldPrime
Documentation

The prime-decomposition tower identity: P_Z = P ∩ O_{Z_P} for the decomposition field.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
abbrev decompositionFieldPrime
    (P : Ideal (𝓞 L)) :
    Ideal (𝓞 (decompositionField (K := K) (L := L) G P))
instance

decompositionFieldPrime_isPrime

L86 ↗
HilbertRamification.Dedekind.decompositionFieldPrime_isPrime
Documentation

The contracted decomposition-field prime is prime.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
instance decompositionFieldPrime_isPrime
    (P : Ideal (𝓞 L)) [P.IsPrime] :
    (decompositionFieldPrime (K := K) (L := L) G P).IsPrime
instance

decompositionFieldPrime_liesOver

L92 ↗
HilbertRamification.Dedekind.decompositionFieldPrime_liesOver
Documentation

The top prime lies over its contraction to the decomposition field.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · full declaration
instance decompositionFieldPrime_liesOver
    (P : Ideal (𝓞 L)) :
    P.LiesOver (decompositionFieldPrime (K := K) (L := L) G P) where
  over := rfl
instance

decompositionFieldPrime_liesOver_basePrime

L98 ↗
HilbertRamification.Dedekind.decompositionFieldPrime_liesOver_basePrime
Documentation

The decomposition-field contraction lies over the base contraction.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
instance decompositionFieldPrime_liesOver_basePrime
    (P : Ideal (𝓞 L)) :
    (decompositionFieldPrime (K := K) (L := L) G P).LiesOver
      (basePrime (K := K) P)
theorem

decompositionFieldPrime_ne_bot

L109 ↗
HilbertRamification.Dedekind.decompositionFieldPrime_ne_bot
Documentation

The prime-decomposition tower identity: the contracted decomposition-field prime P_Z is nonzero for a finite prime P of O_L.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
theorem decompositionFieldPrime_ne_bot
    (P : Ideal (𝓞 L)) [P.IsMaximal] :
    decompositionFieldPrime (K := K) (L := L) G P ≠ ⊥
abbrev

inertiaFieldPrime

L118 ↗
HilbertRamification.Dedekind.inertiaFieldPrime
Documentation

A prime-decomposition consequence: P_T = P ∩ O_{T_P} for the inertia field.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
abbrev inertiaFieldPrime
    (P : Ideal (𝓞 L)) :
    Ideal (𝓞 (inertiaField (K := K) (L := L) G P))
instance

inertiaFieldPrime_isPrime

L124 ↗
HilbertRamification.Dedekind.inertiaFieldPrime_isPrime
Documentation

The contracted inertia-field prime is prime.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
instance inertiaFieldPrime_isPrime
    (P : Ideal (𝓞 L)) [P.IsPrime] :
    (inertiaFieldPrime (K := K) (L := L) G P).IsPrime
instance

inertiaFieldPrime_liesOver

L130 ↗
HilbertRamification.Dedekind.inertiaFieldPrime_liesOver
Documentation

The top prime lies over its contraction to the inertia field.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · full declaration
instance inertiaFieldPrime_liesOver
    (P : Ideal (𝓞 L)) :
    P.LiesOver (inertiaFieldPrime (K := K) (L := L) G P) where
  over := rfl
instance

inertiaField_algebra_decompositionField

L138 ↗
HilbertRamification.Dedekind.inertiaField_algebra_decompositionField
Documentation

The inertia field has the same underlying field whether viewed over K or over the decomposition field; this instance keeps ring-of-integers extensions in the tower explicit.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
instance inertiaField_algebra_decompositionField
    (P : Ideal (𝓞 L)) :
    Algebra (decompositionField (K := K) (L := L) G P)
      (inertiaField (K := K) (L := L) G P)
instance

ringOfIntegers_isScalarTower_decomposition_inertia

L149 ↗
HilbertRamification.Dedekind.ringOfIntegers_isScalarTower_decomposition_inertia
Documentation

The ring-of-integers tower from the decomposition field through the inertia field to L is scalar-compatible.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
instance ringOfIntegers_isScalarTower_decomposition_inertia
    (P : Ideal (𝓞 L)) :
    IsScalarTower
      (𝓞 (decompositionField (K := K) (L := L) G P))
      (𝓞 (inertiaField (K := K) (L := L) G P))
      (𝓞 L)
instance

inertiaFieldPrime_liesOver_decompositionFieldPrime

L164 ↗
HilbertRamification.Dedekind.inertiaFieldPrime_liesOver_decompositionFieldPrime
Documentation

The inertia-field contraction lies over the decomposition-field contraction.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
instance inertiaFieldPrime_liesOver_decompositionFieldPrime
    (P : Ideal (𝓞 L)) :
    (inertiaFieldPrime (K := K) (L := L) G P).LiesOver
      (decompositionFieldPrime (K := K) (L := L) G P)
instance

inertiaFieldPrime_liesOver_basePrime

L173 ↗
HilbertRamification.Dedekind.inertiaFieldPrime_liesOver_basePrime
Documentation

The inertia-field contraction lies over the base contraction.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
instance inertiaFieldPrime_liesOver_basePrime
    (P : Ideal (𝓞 L)) :
    (inertiaFieldPrime (K := K) (L := L) G P).LiesOver
      (basePrime (K := K) P)
theorem

inertiaFieldPrime_ne_bot

L184 ↗
HilbertRamification.Dedekind.inertiaFieldPrime_ne_bot
Documentation

A prime-decomposition consequence: the contracted inertia-field prime P_T is nonzero for a finite prime P of O_L.

Source context 9 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open Algebra NumberField
open scoped Pointwise
attribute [local instance] Ideal.Quotient.field
variable {K L : Type*}
variable [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
variable (G : Type*) [Group G] [MulSemiringAction G L] [SMulCommClass G K L]
Lean source · statement
theorem inertiaFieldPrime_ne_bot
    (P : Ideal (𝓞 L)) [P.IsMaximal] :
    inertiaFieldPrime (K := K) (L := L) G P ≠ ⊥

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.