Module

ActualFiniteDecompositionRestriction.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteDecompositionRestriction

4 declarations indexed from sourceView source ↗

Module documentation

Actual original-to-finite decomposition restriction

The existing original coefficient decomposition morphism fixes the upper prime. Its literal normalization inclusion square then fixes the contracted finite prime. These proved facts construct the actual finite restriction.

Imports8

Imported by7

theorem

originalNormalizationDecomposition_comap

L39 ↗

EtaleFundamentalGroups.Inertia.originalNormalizationDecomposition_comap

Documentation

The existing original decomposition morphism fixes the literal upper prime under its already identified coefficient ring map.

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] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]

Lean source · statement

theorem originalNormalizationDecomposition_comap
    (Q : Ideal (normalizationCommAlgCat A L).carrier)
    (σ : (normalizationDecompositionGroup A K L Q).carrier) :
    Q = Q.comap (normalizationGaloisRingHom A K L σ.val)

theorem

originalDecomposition_finiteNormalization_stable

L52 ↗

EtaleFundamentalGroups.Inertia.originalDecomposition_finiteNormalization_stable

Documentation

The literal coefficient square contracts original decomposition stability to the actual finite normalization prime.

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] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]

Lean source · statement

theorem originalDecomposition_finiteNormalization_stable
    (Q : Ideal (normalizationCommAlgCat A L).carrier)
    (E : FiniteGaloisIntermediateField K L)
    (σ : (normalizationDecompositionGroup A K L Q).carrier) :
    (finiteAbsoluteNormalizationPrime A K L Q E).map
        (actualFiniteNormalizationRestrictionRingHom A K L E σ.val) =
      finiteAbsoluteNormalizationPrime A K L Q E

def

actualFiniteDecompositionCoefficientMap

L69 ↗

EtaleFundamentalGroups.Inertia.actualFiniteDecompositionCoefficientMap

Documentation

The prescribed finite coefficient map on the original decomposition group.

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] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]

Lean source · full declaration

def actualFiniteDecompositionCoefficientMap
    (Q : Ideal (normalizationCommAlgCat A L).carrier)
    (E : FiniteGaloisIntermediateField K L) :
    GrpCat.Hom (normalizationDecompositionGroup A K L Q)
      (commAlgAutomorphismGroup A (finiteAbsoluteNormalizationAlgebra A K L E)) where
  hom' := (actualFiniteNormalizationRestriction A K L E).hom'.comp
    (normalizationDecompositionInclusion A K L Q)

def