Module

CyclicCoordinates.lean

Nyll.EtaleFundamentalGroups.Inertia.Localized.CyclicCoordinates

3 declarations indexed from sourceView source ↗

Module documentation

Cyclic coordinates for localized normalization inertia

At a height-one prime with characteristic-zero residue field, the localized normalization inertia group is cyclic. This file turns that source theorem into a noncomputably chosen additive coordinate system indexed by the actual group cardinality.

Imports2

Imported by2

theorem

localizationAtPrime_smulCommClass

L32 ↗

EtaleFundamentalGroups.localizationAtPrime_smulCommClass

Source context 9 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] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
omit [IsDomain A] [Algebra A L] [IsScalarTower A K L] in

Lean source · full declaration

theorem localizationAtPrime_smulCommClass
    (P : Ideal A) [P.IsPrime] :
    letI := localizationAtPrimeToFractionFieldAlgebra (K := K) P
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI := localizationAtPrimeToFractionFieldToExtension_isScalarTower
      (K := K) (L := L) P
    SMulCommClass Gal(L/K) (Localization.AtPrime P) L := by
  let V := Localization.AtPrime P
  let : Algebra V K :=
    localizationAtPrimeToFractionFieldAlgebra (K := K) P
  let : Algebra V L :=
    localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  let : IsScalarTower V K L :=
    localizationAtPrimeToFractionFieldToExtension_isScalarTower
      (K := K) (L := L) P
  refine ⟨fun σ v x ↦ ?_⟩
  change σ (algebraMap V L v * x) = algebraMap V L v * σ x
  rw [map_mul, IsScalarTower.algebraMap_apply V K L, AlgEquiv.commutes]

theorem

localizedNormalizationInertia_isCyclic

L54 ↗

EtaleFundamentalGroups.localizedNormalizationInertia_isCyclic

Source context 10 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] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [IsRegularRing A]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem localizedNormalizationInertia_isCyclic
    (P : Ideal A) [P.IsPrime] (hP : P.height = 1)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P]
    [CharZero (A ⧸ P)] :
    IsCyclic (localizedNormalizationInertia (K := K) (L := L) P Q)

def

localizedNormalizationInertiaAddEquivZMod

L149 ↗

EtaleFundamentalGroups.localizedNormalizationInertiaAddEquivZMod

Documentation

Noncomputably chosen additive cyclic coordinates on the localized normalization inertia group. The coordinate modulus is the actual group cardinality.

Source context 10 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] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [IsRegularRing A]
variable [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def localizedNormalizationInertiaAddEquivZMod
    (P : Ideal A) [P.IsPrime] (hP : P.height = 1)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver P]
    [CharZero (A ⧸ P)] :
    Additive (localizedNormalizationInertia (K := K) (L := L) P Q) ≃+
      ZMod (Nat.card
        (localizedNormalizationInertia (K := K) (L := L) P Q))

Module documentation

Cyclic coordinates for localized normalization inertia

Declarations

localizationAtPrime_smulCommClass

localizedNormalizationInertia_isCyclic

localizedNormalizationInertiaAddEquivZMod