Module

RamificationSupportCompositum.lean

Nyll.SawinTotallyRealTowers.RamificationSupportCompositum

3 declarations indexed from sourceView source ↗

Module documentation

Composita with prescribed finite ramification support

Inertia at a prime outside the permitted support is trivial on each factor. The restrictions to the factors jointly detect automorphisms of their compositum. This argument does not require an odd extension degree.

Imports3

Nyll.SawinTotallyRealTowers.RamificationSupportTransport
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.CompositumUnramified
Mathlib.FieldTheory.Galois.GaloisClosure

Imported by2

instance

finiteIntermediateFieldNumberField

L28 ↗

ClassFieldTower.Sawin.finiteIntermediateFieldNumberField

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

instance finiteIntermediateFieldNumberField
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K] [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega) [FiniteDimensional K E] : NumberField E

theorem

inertia_eq_bot_of_outside

L36 ↗

ClassFieldTower.Sawin.inertia_eq_bot_of_outside

Documentation

The support condition kills inertia in a normal intermediate field at every prime above a base prime outside the support.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin
private local instance finiteIntermediateFieldNumberField
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K] [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega) [FiniteDimensional K E] : NumberField E :=
  NumberField.of_module_finite K E

Lean source · statement

theorem inertia_eq_bot_of_outside
    {K : Type u} {M : Type v}
    [Field K] [NumberField K] [Field M] [NumberField M]
    [Algebra K M] [FiniteDimensional K M]
    (A : IntermediateField K M) [IsGalois K A]
    (T : Set (HeightOneSpectrum (𝓞 K)))
    (hA : IsUnramifiedAtFinitePlacesOutside K A T)
    (Q : HeightOneSpectrum (𝓞 M))
    (hQ : finitePlaceBelow (K := K) Q ∉ T) :
    HilbertRamification.Dedekind.inertiaGroup
      (Q.asIdeal.under (𝓞 A)) (A ≃ₐ[K] A) = ⊥

theorem

sup

L58 ↗

ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutside.sup

Documentation

Finite Galois composita preserve the permitted ramification support.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin
private local instance finiteIntermediateFieldNumberField
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K] [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega) [FiniteDimensional K E] : NumberField E :=
  NumberField.of_module_finite K E
namespace IsUnramifiedAtFinitePlacesOutside

Lean source · statement

theorem sup
    {K : Type u} {Omega : Type v}
    [Field K] [NumberField K] [Field Omega] [Algebra K Omega]
    (E₁ E₂ : IntermediateField K Omega)
    [FiniteDimensional K E₁] [FiniteDimensional K E₂]
    [IsGalois K E₁] [IsGalois K E₂]
    (T : Set (HeightOneSpectrum (𝓞 K)))
    (h₁ : IsUnramifiedAtFinitePlacesOutside K E₁ T)
    (h₂ : IsUnramifiedAtFinitePlacesOutside K E₂ T) :
    IsUnramifiedAtFinitePlacesOutside K ↥(E₁ ⊔ E₂) T

Module documentation

Composita with prescribed finite ramification support

Declarations

finiteIntermediateFieldNumberField

inertia_eq_bot_of_outside

sup