NYLL
Module

ActualFiniteNormalizationLocalTower.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationLocalTower
2 declarations indexed from sourceView source ↗

Module documentation

Local maps in finite normalization towers

Constructs the local ring map at nested finite normalization primes and establishes its injectivity under the DVR and Galois hypotheses.

Imports4
Imported by6

Declarations

def

actualFiniteNormalizationTowerLocalRingMap

L33 ↗
EtaleFundamentalGroups.Inertia.actualFiniteNormalizationTowerLocalRingMap
Documentation

The literal local ring map at two nested actual finite primes.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
  (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsPrime]
Lean source · full declaration
def actualFiniteNormalizationTowerLocalRingMap
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
    letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q F
    Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q E) →+*
      Localization.AtPrime (finiteAbsoluteNormalizationPrime A K L Q F) := by
  letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q E
  letI := finiteAbsoluteNormalizationPrime_isPrime A K L Q F
  exact Localization.localRingHom
    (finiteAbsoluteNormalizationPrime A K L Q E)
    (finiteAbsoluteNormalizationPrime A K L Q F)
    (actualFiniteNormalizationTowerRingMap A K L E F h)
    (actualFiniteNormalizationPrime_tower A K L Q E F h)
theorem

actualFiniteNormalizationTowerLocalRingMap_injective

L48 ↗
EtaleFundamentalGroups.Inertia.actualFiniteNormalizationTowerLocalRingMap_injective
Documentation

The actual map of finite local normalizations is injective.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
  (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsPrime]
Lean source · statement
theorem actualFiniteNormalizationTowerLocalRingMap_injective
    [IsDomain A] [IsDiscreteValuationRing A] [IsFractionRing A K] [IsGalois K L]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    Function.Injective (actualFiniteNormalizationTowerLocalRingMap A K L Q E F h).toFun

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