Module

Basic.lean

Nyll.EtaleFundamentalGroups.Inertia.Localized.Basic

2 declarations indexed from sourceView source ↗

Module documentation

Inertia at a localized normalization prime

This file defines the inertia subgroup at a normalization prime after localizing the base at a prime ideal. The construction uses only the canonical fraction-field maps and the generic action on an integral closure; it has no DVR, height, regularity, finiteness, or Galois-extension hypothesis.

Imports1

Nyll.EtaleFundamentalGroups.Normalization.Primes.Basic

Imported by5

theorem

localizationAtPrime_galois_smulCommClass

L34 ↗

EtaleFundamentalGroups.localizationAtPrime_galois_smulCommClass

Documentation

The canonical Galois action on L commutes with scalars from the prime localization of A. This is a named non-instance producer so consumers can reuse the same local instance without adding a global typeclass path.

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_galois_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]

def

localizedNormalizationInertia

L57 ↗

EtaleFundamentalGroups.localizedNormalizationInertia

Documentation

The inertia subgroup at the ideal transported to the normalization of the prime localization. Its action is the generic integral-closure action induced by the canonical action of Gal(L/K) on L; no DVR or height assumption is needed.

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] [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]

Lean source · statement

def localizedNormalizationInertia
    (P : Ideal A) [P.IsPrime]
    (Q : Ideal (integralClosure A L)) :
    Subgroup Gal(L/K)

Module documentation

Inertia at a localized normalization prime

Declarations

localizationAtPrime_galois_smulCommClass

localizedNormalizationInertia