NYLL
Module

CompositumUnramified.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.CompositumUnramified
7 declarations indexed from sourceView source ↗

Module documentation

Unramifiedness in a compositum

This file contains reusable criteria for proving that a prime in a number field compositum is unramified from the inertia groups of its two factors.

Imports5
Imported by9

Declarations

theorem

inertiaGroup_eq_bot_of_restrictNormal_of_sup_eq_top

L35 ↗
HilbertRamification.Dedekind.inertiaGroup_eq_bot_of_restrictNormal_of_sup_eq_top
Documentation

If two normal intermediate fields generate a number-field extension and the inertia of a prime restricts trivially to both, then the original inertia group is trivial. The base field is arbitrary; in particular this applies to the Kummer composita used in the global existence theorem.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem inertiaGroup_eq_bot_of_restrictNormal_of_sup_eq_top
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    (A B : IntermediateField K M) [Normal K A] [Normal K B]
    (Q : Ideal (𝓞 M))
    (hsup : A ⊔ B = ⊤)
    (hIA :
      inertiaGroup (Q.under (𝓞 A)) Gal(A/K) = ⊥)
    (hIB :
      inertiaGroup (Q.under (𝓞 B)) Gal(B/K) = ⊥) :
    inertiaGroup Q Gal(M/K) = ⊥
theorem

inertiaGroup_eq_bot_of_finset_adjoin_eq_top

L125 ↗
HilbertRamification.Dedekind.inertiaGroup_eq_bot_of_finset_adjoin_eq_top
Documentation

If a finite family of normal simple intermediate fields generates a finite Galois number-field extension and the inertia at a prime restricts trivially to every member of the family, then the inertia of the full extension is trivial. This is the finite-radical form of the compositum argument used for the full S-unit Kummer extension.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem inertiaGroup_eq_bot_of_finset_adjoin_eq_top
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    (T : Finset M)
    (Q : Ideal (𝓞 M))
    (hnormal :
      ∀ x : M, x ∈ T →
        Normal K (IntermediateField.adjoin K {x}))
    (hI :
      ∀ (x : M) (_ : x ∈ T),
        inertiaGroup
            (Q.under
              (𝓞 (IntermediateField.adjoin K {x})))
            Gal((IntermediateField.adjoin K {x})/K) =
          ⊥)
    (hadjoin :
      IntermediateField.adjoin K (T : Set M) = ⊤) :
    inertiaGroup Q Gal(M/K) = ⊥
theorem

inertiaGroup_eq_bot_of_ramificationIdx_eq_one

L227 ↗
HilbertRamification.Dedekind.inertiaGroup_eq_bot_of_ramificationIdx_eq_one
Documentation

For a finite Galois extension of number fields, ramification index one at a prime forces the corresponding inertia group to be trivial. The residue extension is separable because the residue field of a number field is finite.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem inertiaGroup_eq_bot_of_ramificationIdx_eq_one
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    (p : Ideal (𝓞 K)) (P : Ideal (𝓞 M))
    [p.IsPrime] [P.IsPrime] [P.IsMaximal] [P.LiesOver p]
    (hp0 : p ≠ ⊥)
    (he : P.ramificationIdx (𝓞 K) = 1) :
    inertiaGroup P Gal(M/K) = ⊥
theorem

inertiaGroup_eq_bot_of_isUnramifiedAt

L253 ↗
HilbertRamification.Dedekind.inertiaGroup_eq_bot_of_isUnramifiedAt
Documentation

Algebraic unramifiedness at a prime of a finite Galois number-field extension forces the corresponding inertia group to be trivial.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem inertiaGroup_eq_bot_of_isUnramifiedAt
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    (P : Ideal (𝓞 M)) [P.IsPrime] [P.IsMaximal]
    (hunram : Algebra.IsUnramifiedAt (𝓞 K) P) :
    inertiaGroup P Gal(M/K) = ⊥
theorem

isUnramifiedAt_of_inertiaGroup_eq_bot

L276 ↗
HilbertRamification.Dedekind.isUnramifiedAt_of_inertiaGroup_eq_bot
Documentation

Trivial inertia at a prime of a finite Galois number-field extension gives algebraic unramifiedness at that prime.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem isUnramifiedAt_of_inertiaGroup_eq_bot
    {K M : Type*}
    [Field K] [NumberField K]
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    (P : Ideal (𝓞 M)) [P.IsPrime] [P.IsMaximal]
    (hI : inertiaGroup P Gal(M/K) = ⊥) :
    Algebra.IsUnramifiedAt (𝓞 K) P
theorem

inertiaGroup_eq_bot_of_ramificationIdx_eq_one_int

L311 ↗
HilbertRamification.Dedekind.inertiaGroup_eq_bot_of_ramificationIdx_eq_one_int
Documentation

In the rational-base case, ramification index one forces the corresponding inertia group to be trivial.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem inertiaGroup_eq_bot_of_ramificationIdx_eq_one_int
    {K : Type*} [Field K] [NumberField K] [IsGalois ℚ K]
    (p : Ideal ℤ) (P : Ideal (𝓞 K))
    [p.IsPrime] [P.IsPrime] [P.IsMaximal] [P.LiesOver p]
    (hp0 : p ≠ ⊥)
    (he : P.ramificationIdx ℤ = 1) :
    inertiaGroup P Gal(K/ℚ) = ⊥
theorem

isUnramifiedAt_int_of_inertiaGroup_eq_bot

L332 ↗
HilbertRamification.Dedekind.isUnramifiedAt_int_of_inertiaGroup_eq_bot
Documentation

Trivial rational inertia gives unramifiedness at the chosen finite prime.

Source context 5 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
Lean source · statement
theorem isUnramifiedAt_int_of_inertiaGroup_eq_bot
    {K : Type*} [Field K] [NumberField K] [IsGalois ℚ K]
    (P : Ideal (𝓞 K)) [P.IsPrime] [P.IsMaximal]
    (hI : inertiaGroup P Gal(K/ℚ) = ⊥) :
    Algebra.IsUnramifiedAt ℤ P

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