NYLL
Module

FinitePlaceInertiaFixedUnramified.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceInertiaFixedUnramified
7 declarations indexed from sourceView source ↗

Module documentation

Finite Galois fields fixed by absolute inertia are unramified

Normality makes the image of the finite global field in the local separable closure independent of its embedding. The actual decomposition comparison therefore makes inertia fix every generator of its chosen finite localization. The finite local inertia criterion and completion-to-ideal theorem then give unramifiedness at every global finite prime.

Only the two canonical base-to-separable-closure instances from the embedding leaf are reactivated. The three local proof instances (characteristic zero and two field-algebra torsion-freeness proofs) resolve otherwise ambiguous synthesis at IsAlgClosed.lift; no new data instance or alternative scalar tower is used.

Imports4
Imported by3

Declarations

theorem

fieldAlgebraTorsionFree

L33 ↗
ClassFieldTower.Martinet.Shafarevich.fieldAlgebraTorsionFree
Source context 5 commands

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

open NumberField IsDedekindDomain
open scoped NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations LocalClassFieldTheory LocalFieldTheory
Lean source · statement
theorem fieldAlgebraTorsionFree
    (K L : Type*) [Field K] [Field L] [Algebra K L] : Module.IsTorsionFree K L
def

finiteFieldSeparableEmbedding

L41 ↗
ClassFieldTower.Martinet.Shafarevich.finiteFieldSeparableEmbedding
Source context 5 commands

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

open NumberField IsDedekindDomain
open scoped NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations LocalClassFieldTheory LocalFieldTheory
Lean source · statement
def finiteFieldSeparableEmbedding
    (K L : Type) [Field K] [CharZero K] [Field L] [Algebra K L]
    [FiniteDimensional K L] : L →ₐ[K] SeparableClosure K
theorem

normal_algHom_range_eq

L49 ↗
ClassFieldTower.Martinet.Shafarevich.normal_algHom_range_eq
Source context 5 commands

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

open NumberField IsDedekindDomain
open scoped NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations LocalClassFieldTheory LocalFieldTheory
Lean source · statement
theorem normal_algHom_range_eq
    {K E A : Type*} [Field K] [Field E] [Field A] [Algebra K E] [Algebra K A]
    [FiniteDimensional K E] [Normal K E] (f g : E →ₐ[K] A) : f.range = g.range
theorem

normal_algHom_fixed_image

L57 ↗
ClassFieldTower.Martinet.Shafarevich.normal_algHom_fixed_image
Source context 5 commands

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

open NumberField IsDedekindDomain
open scoped NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations LocalClassFieldTheory LocalFieldTheory
Lean source · statement
theorem normal_algHom_fixed_image
    {K E A : Type*} [Field K] [Field E] [Field A] [Algebra K E] [Algebra K A]
    [FiniteDimensional K E] [Normal K E] (f g : E →ₐ[K] A)
    (u : A → A) (hu : ∀ x : E, u (g x) = g x) (x : E) : u (f x) = f x
theorem

chosenFinitePlaceIsUnramified_of_absoluteInertiaFixes

L80 ↗
ClassFieldTower.Martinet.Shafarevich.chosenFinitePlaceIsUnramified_of_absoluteInertiaFixes
Documentation

Absolute inertia fixing a finite normal global field forces its actual chosen local extension to be unramified.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations LocalClassFieldTheory LocalFieldTheory
attribute [local instance] finitePlaceSeparableEmbeddingBaseAlgebra
  finitePlaceSeparableEmbeddingBaseTower
variable (F : Type) [Field F] [NumberField F]
variable (M : IntermediateField F (AlgebraicClosure F))
  [FiniteDimensional F M] [IsGalois F M]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "Loc" => ChosenFinitePlaceLocalizedCompletion (K := F) (L := M) v
local notation "wM" => chosenFinitePlaceExtension (L := M) v
Lean source · statement
theorem chosenFinitePlaceIsUnramified_of_absoluteInertiaFixes
    (hM : ∀ tau : finitePlaceAbsoluteInertiaSubgroup F v,
      ∀ x : M, (tau.1.1 : Gal(AlgebraicClosure F/F)) (x : AlgebraicClosure F) = x) :
    ChosenFinitePlaceIsUnramified (K := F) (L := M) v
instance

finitePlaceInertiaFixedNumberField

L118 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceInertiaFixedNumberField
Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations LocalClassFieldTheory LocalFieldTheory
attribute [local instance] finitePlaceSeparableEmbeddingBaseAlgebra
  finitePlaceSeparableEmbeddingBaseTower
variable (F : Type) [Field F] [NumberField F]
variable (M : IntermediateField F (AlgebraicClosure F))
  [FiniteDimensional F M] [IsGalois F M]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "Loc" => ChosenFinitePlaceLocalizedCompletion (K := F) (L := M) v
local notation "wM" => chosenFinitePlaceExtension (L := M) v
Lean source · statement
instance finitePlaceInertiaFixedNumberField : NumberField M
theorem

finitePlacesUnramified_of_absoluteInertiaFixes

L123 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlacesUnramified_of_absoluteInertiaFixes
Documentation

If every selected absolute inertia fixes the finite Galois field, every finite prime of that field is unramified over the base.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations LocalClassFieldTheory LocalFieldTheory
attribute [local instance] finitePlaceSeparableEmbeddingBaseAlgebra
  finitePlaceSeparableEmbeddingBaseTower
variable (F : Type) [Field F] [NumberField F]
variable (M : IntermediateField F (AlgebraicClosure F))
  [FiniteDimensional F M] [IsGalois F M]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "Loc" => ChosenFinitePlaceLocalizedCompletion (K := F) (L := M) v
local notation "wM" => chosenFinitePlaceExtension (L := M) v
local instance finitePlaceInertiaFixedNumberField : NumberField M :=
  NumberField.of_module_finite F M
Lean source · statement
theorem finitePlacesUnramified_of_absoluteInertiaFixes
    (hM : ∀ v : HeightOneSpectrum (𝓞 F),
      ∀ tau : finitePlaceAbsoluteInertiaSubgroup F v,
      ∀ x : M, (tau.1.1 : Gal(AlgebraicClosure F/F)) (x : AlgebraicClosure F) = x)
    (P : HeightOneSpectrum (𝓞 M)) : Algebra.IsUnramifiedAt (𝓞 F) P.asIdeal

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