Module

Localization.lean

Nyll.EtaleFundamentalGroups.Inertia.Normalization.Localization

2 declarations indexed from sourceView source ↗

Module documentation

Normalization inertia and localization

Localizing a normalization at a prime below Q does not change its inertia subgroup. This is the comparison needed to state the final one-point theorem using the original normalization prime, while applying the existing height-one cardinality theorem to the localized normalization.

Only the canonical generic action on integral closures is used. In particular, this file introduces no global action, algebra, or scalar-tower instances and needs no finiteness, Galois, regularity, or height hypotheses.

Imports1

Nyll.EtaleFundamentalGroups.Inertia.Localized.Basic

Imported by6

theorem

normalizationInertia_eq_localizedNormalizationInertia_of_under_le

L37 ↗

EtaleFundamentalGroups.normalizationInertia_eq_localizedNormalizationInertia_of_under_le

Documentation

Inertia at a normalization prime is unchanged after localizing the base at any larger prime. The contraction of Q need only be contained in the localization prime; it need not equal it.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]

Lean source · statement

theorem normalizationInertia_eq_localizedNormalizationInertia_of_under_le
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (hQP : Q.under A ≤ P) :
    Q.toAddSubgroup.inertia Gal(L/K) =
      localizedNormalizationInertia (K := K) (L := L) P Q

theorem

normalizationInertia_eq_localizedNormalizationInertia

L124 ↗

EtaleFundamentalGroups.normalizationInertia_eq_localizedNormalizationInertia