NYLL
Module

NumberFieldPrimes.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.NumberFieldPrimes
15 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: number-field prime ideals in the fixed fields

This file proves the ramification and inertia invariant statements for the contracted primes P_Z and P_T appearing in the decomposition and inertia fixed-field tower.

Imports4
Imported by4

Declarations

theorem

dedekindTower_decompositionFieldPrime_primesOver_ncard_eq_one

L38 ↗
HilbertRamification.Dedekind.dedekindTower_decompositionFieldPrime_primesOver_ncard_eq_one
Documentation

The prime-decomposition tower identity: P is the only prime of O_L above P_Z.

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 dedekindTower_decompositionFieldPrime_primesOver_ncard_eq_one
    (P : Ideal (𝓞 L)) [P.IsPrime]
    [Finite G] [IsGaloisGroup G K L] :
    ((decompositionFieldPrime (K := K) (L := L) G P).primesOver (𝓞 L)).ncard =
      1
theorem

dedekindTower_decompositionFieldPrime_product_eq_base_product

L68 ↗
HilbertRamification.Dedekind.dedekindTower_decompositionFieldPrime_product_eq_base_product
Documentation

The prime-decomposition tower identity: over the decomposition field, the local product e(P/P_Z) * f(P/P_Z) equals the original product e(P/p) * f(P/p). This is the exact e' f' = e f product comparison in the prime-decomposition proof.

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 dedekindTower_decompositionFieldPrime_product_eq_base_product
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L] :
    Ideal.ramificationIdx' (decompositionFieldPrime (K := K) (L := L) G P) P *
        P.inertiaDeg
          (𝓞 (decompositionField (K := K) (L := L) G P)) =
      Ideal.ramificationIdx' (basePrime (K := K) P) P *
        P.inertiaDeg (𝓞 K)
theorem

dedekindTower_decompositionFieldPrime_tower_invariants

L127 ↗
HilbertRamification.Dedekind.dedekindTower_decompositionFieldPrime_tower_invariants
Documentation

The prime-decomposition tower identity: for the decomposition field prime P_Z, the top extension has the original ramification index and inertia degree, while P_Z/p has both invariants equal to 1.

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 dedekindTower_decompositionFieldPrime_tower_invariants
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L] :
    Ideal.ramificationIdx' (basePrime (K := K) P) (decompositionFieldPrime (K := K) (L := L) G
      P) = 1 ∧
      (decompositionFieldPrime (K := K) (L := L) G P).inertiaDeg
          (𝓞 K) = 1 ∧
      Ideal.ramificationIdx' (decompositionFieldPrime (K := K) (L := L) G P) P =
        Ideal.ramificationIdx' (basePrime (K := K) P) P ∧
      P.inertiaDeg (𝓞 (decompositionField (K := K) (L := L) G P)) =
        P.inertiaDeg (𝓞 K)
theorem

dedekindRamification_inertiaFieldPrime_primesOver_ncard_eq_one

L175 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldPrime_primesOver_ncard_eq_one
Documentation

A prime-decomposition consequence: P is the only prime of O_L above P_T.

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 dedekindRamification_inertiaFieldPrime_primesOver_ncard_eq_one
    (P : Ideal (𝓞 L)) [P.IsPrime]
    [Finite G] [IsGaloisGroup G K L] :
    ((inertiaFieldPrime (K := K) (L := L) G P).primesOver (𝓞 L)).ncard =
      1
theorem

dedekindRamification_inertiaFieldPrime_product_eq_base_ramificationIdx

L205 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldPrime_product_eq_base_ramificationIdx
Documentation

A prime-decomposition consequence: over the inertia field, the local product e(P/P_T) * f(P/P_T) equals the original ramification index e(P/p) when the residue extension is separable.

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 dedekindRamification_inertiaFieldPrime_product_eq_base_ramificationIdx
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    Ideal.ramificationIdx' (inertiaFieldPrime (K := K) (L := L) G P) P *
        P.inertiaDeg
          (𝓞 (inertiaField (K := K) (L := L) G P)) =
      Ideal.ramificationIdx' (basePrime (K := K) P) P
theorem

dedekindRamification_inertiaFieldPrime_residue_isSeparable

L263 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldPrime_residue_isSeparable
Documentation

A prime-decomposition consequence: the residue extension for P/P_T is separable whenever the original residue extension kappa(P)/kappa(p) is separable.

Source context 10 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]
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem dedekindRamification_inertiaFieldPrime_residue_isSeparable
    (P : Ideal (𝓞 L)) [P.IsMaximal]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    Algebra.IsSeparable
      ((𝓞 (inertiaField (K := K) (L := L) G P)) ⧸
        inertiaFieldPrime (K := K) (L := L) G P)
      ((𝓞 L) ⧸ P)
theorem

dedekindRamification_inertiaFieldPrime_inertiaDeg_eq_one

L312 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldPrime_inertiaDeg_eq_one
Documentation

A prime-decomposition consequence: P/P_T has residue degree one.

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 dedekindRamification_inertiaFieldPrime_inertiaDeg_eq_one
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    P.inertiaDeg (𝓞 (inertiaField (K := K) (L := L) G P)) = 1
theorem

dedekindRamification_inertiaFieldPrime_top_invariants

L368 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldPrime_top_invariants
Documentation

Ramification over the inertia field: over the inertia field, P has ramification index e and residue degree 1.

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 dedekindRamification_inertiaFieldPrime_top_invariants
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    Ideal.ramificationIdx' (inertiaFieldPrime (K := K) (L := L) G P) P =
        Ideal.ramificationIdx' (basePrime (K := K) P) P ∧
      P.inertiaDeg (𝓞 (inertiaField (K := K) (L := L) G P)) = 1
theorem

dedekindRamification_inertiaFieldPrime_middle_invariants

L387 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldPrime_middle_invariants
Documentation

Ramification between the decomposition and inertia fields: between the decomposition field and inertia field, P_T/P_Z has ramification index 1 and residue degree f.

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 dedekindRamification_inertiaFieldPrime_middle_invariants
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    Ideal.ramificationIdx' (decompositionFieldPrime (K := K) (L := L) G P) (inertiaFieldPrime (K
      := K) (L := L) G P) = 1 ∧
      (inertiaFieldPrime (K := K) (L := L) G P).inertiaDeg
          (𝓞 (decompositionField (K := K) (L := L) G P)) =
        P.inertiaDeg (𝓞 K)
theorem

dedekindRamification_inertiaField_finrank_eq_base_ramificationIdx

L450 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaField_finrank_eq_base_ramificationIdx
Documentation

A prime-decomposition consequence: [L : T_P] = e.

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 dedekindRamification_inertiaField_finrank_eq_base_ramificationIdx
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    Module.finrank (inertiaField (K := K) (L := L) G P) L =
      P.ramificationIdx (𝓞 K)
theorem

dedekindRamification_inertiaFieldOverDecompositionField_finrank_eq_base_inertiaDeg

L470 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldOverDecompositionField_finrank_eq_base_inertiaDeg
Documentation

A prime-decomposition consequence: [T_P : Z_P] = f.

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 dedekindRamification_inertiaFieldOverDecompositionField_finrank_eq_base_inertiaDeg
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    Module.finrank (decompositionField (K := K) (L := L) G P)
        (inertiaFieldOverDecompositionField (K := K) (L := L) G P) =
      P.inertiaDeg (𝓞 K)
theorem

dedekindRamification_inertiaField_degree_cardinalities

L493 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaField_degree_cardinalities
Documentation

Degree and cardinality relations in the fixed-field tower: #I_P = [L:T_P] = e and #(G_P/I_P) = [T_P:Z_P] = f.

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 dedekindRamification_inertiaField_degree_cardinalities
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    Nat.card (inertiaGroup P G) =
        P.ramificationIdx (𝓞 K) ∧
      Module.finrank (inertiaField (K := K) (L := L) G P) L =
        P.ramificationIdx (𝓞 K) ∧
      Nat.card
          (decompositionGroup P G ⧸
            (inertiaGroup P G).subgroupOf (decompositionGroup P G)) =
        P.inertiaDeg (𝓞 K) ∧
      Module.finrank (decompositionField (K := K) (L := L) G P)
          (inertiaFieldOverDecompositionField (K := K) (L := L) G P) =
        P.inertiaDeg (𝓞 K)
theorem

dedekindRamification_inertiaFieldPrime_tower_invariants

L526 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaFieldPrime_tower_invariants
Documentation

Ramification and residue degrees in the ideal-level fixed-field tower: Z_P -> T_P -> L has ramification indices 1, e and residue degrees f, 1.

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 dedekindRamification_inertiaFieldPrime_tower_invariants
    (P : Ideal (𝓞 L)) [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    Ideal.ramificationIdx' (inertiaFieldPrime (K := K) (L := L) G P) P =
        Ideal.ramificationIdx' (basePrime (K := K) P) P ∧
      P.inertiaDeg (𝓞 (inertiaField (K := K) (L := L) G P)) = 1 ∧
      Ideal.ramificationIdx' (decompositionFieldPrime (K := K) (L := L) G P) (inertiaFieldPrime
        (K := K) (L := L) G P) = 1 ∧
      (inertiaFieldPrime (K := K) (L := L) G P).inertiaDeg
          (𝓞 (decompositionField (K := K) (L := L) G P)) =
        P.inertiaDeg (𝓞 K)
theorem

inertiaGroup_eq_bot_iff_isUnramifiedAt

L548 ↗
HilbertRamification.Dedekind.inertiaGroup_eq_bot_iff_isUnramifiedAt
Documentation

A trivial-inertia special case: under the separable residue hypothesis, I_P = 1 if and only if P is unramified over O_K.

Source context 10 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]
omit [SMulCommClass G K L] in
Lean source · statement
theorem inertiaGroup_eq_bot_iff_isUnramifiedAt
    {P : Ideal (𝓞 L)} [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    inertiaGroup P G = ⊥ ↔ Algebra.IsUnramifiedAt (𝓞 K) P
theorem

dedekindRamification_inertiaField_eq_top_iff_isUnramifiedAt

L569 ↗
HilbertRamification.Dedekind.dedekindRamification_inertiaField_eq_top_iff_isUnramifiedAt
Documentation

A trivial-inertia special case: under the separable residue hypothesis, T_P = L if and only if P is unramified over O_K.

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 dedekindRamification_inertiaField_eq_top_iff_isUnramifiedAt
    {P : Ideal (𝓞 L)} [P.IsPrime] [P.IsMaximal]
    [Finite G] [IsGaloisGroup G K L]
    [Algebra.IsSeparable ((𝓞 K) ⧸ basePrime (K := K) P) ((𝓞 L) ⧸ P)] :
    inertiaField (K := K) (L := L) G P = ⊤ ↔
      Algebra.IsUnramifiedAt (𝓞 K) P

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