Module

ActualFiniteNormalizationTower.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteNormalizationTower

4 declarations indexed from sourceView source ↗

Module documentation

Inclusions of finite normalizations

Constructs injective ring maps between nested finite normalizations. Proves their ambient inclusion triangle and the contraction identity for chosen primes.

Imports4

Imported by10

def

actualFiniteNormalizationTowerRingMap

L32 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationTowerRingMap

Documentation

The literal map between the normalizations of two actual finite levels.

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]

Lean source · statement

def actualFiniteNormalizationTowerRingMap
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    finiteAbsoluteNormalizationAlgebra A K L E →+*
      finiteAbsoluteNormalizationAlgebra A K L F

theorem

actualFiniteNormalizationTowerRingMap_comp

L41 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationTowerRingMap_comp

Documentation

The actual finite normalization inclusions form their literal tower triangle.

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]

Lean source · statement

theorem actualFiniteNormalizationTowerRingMap_comp
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    (finiteAbsoluteNormalizationRingMap A K L F).comp
        (actualFiniteNormalizationTowerRingMap A K L E F h) =
      finiteAbsoluteNormalizationRingMap A K L E

theorem

actualFiniteNormalizationTowerRingMap_injective

L51 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationTowerRingMap_injective

Documentation

The actual finite tower inclusion 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]

Lean source · statement

theorem actualFiniteNormalizationTowerRingMap_injective
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    Function.Injective (actualFiniteNormalizationTowerRingMap A K L E F h).toFun

theorem

actualFiniteNormalizationPrime_tower

L59 ↗

EtaleFundamentalGroups.Inertia.actualFiniteNormalizationPrime_tower

Documentation

The chosen finite primes are the literal contractions along the tower.

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]

Lean source · statement

theorem actualFiniteNormalizationPrime_tower
    (Q : Ideal (normalizationCommAlgCat A L))
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    finiteAbsoluteNormalizationPrime A K L Q E =
      (finiteAbsoluteNormalizationPrime A K L Q F).comap
        (actualFiniteNormalizationTowerRingMap A K L E F h)

Module documentation

Inclusions of finite normalizations

Declarations

actualFiniteNormalizationTowerRingMap

actualFiniteNormalizationTowerRingMap_comp

actualFiniteNormalizationTowerRingMap_injective

actualFiniteNormalizationPrime_tower