NYLL
Module

ActualFiniteDecompositionSurjectivity.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteDecompositionSurjectivity
3 declarations indexed from sourceView source ↗

Module documentation

Surjectivity onto actual finite decomposition

The proved finite field decomposition image supplies original decomposition lifts. The actual coefficient-automorphism surjection then identifies the target with the existing intrinsic finite-normalization stabilizer.

Imports5
Imported by3

Declarations

theorem

actualNormalizationDecomposition_exists_finiteNative_restriction

L34 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationDecomposition_exists_finiteNative_restriction
Documentation

The actual field decomposition image provides an original lift of every finite field decomposition element.

Source context 4 commands

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

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 actualNormalizationDecomposition_exists_finiteNative_restriction
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
    (E : FiniteGaloisIntermediateField K L)
    (τ : { g : (finiteGaloisGroupObject K L E).carrier //
      ((finiteNormalizationActionDiagram A K L E).lowerDecomposition
        (finiteAbsoluteNormalizationPrime A K L Q E)).carrier g }) :
    ∃ σ : (normalizationDecompositionGroup A K L Q).carrier,
      (finiteGaloisRestrictionGroupMap K L E).hom'.toFun σ.val = τ.val
theorem

finiteNormalizationDecomposition_exists_finiteNative_lift

L52 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationDecomposition_exists_finiteNative_lift
Documentation

The actual finite field action lifts every intrinsic finite coefficient decomposition element.

Source context 4 commands

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

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 finiteNormalizationDecomposition_exists_finiteNative_lift
    (Q : Ideal (integralClosure A L)) (E : FiniteGaloisIntermediateField K L)
    (τ : (commAlgIdealDecompositionGroup A (finiteAbsoluteNormalizationAlgebra A K L E)
      (finiteAbsoluteNormalizationPrime A K L Q E)).carrier) :
    ∃ g : { g : (finiteGaloisGroupObject K L E).carrier //
      ((finiteNormalizationActionDiagram A K L E).lowerDecomposition
        (finiteAbsoluteNormalizationPrime A K L Q E)).carrier g },
      (finiteNormalizationGaloisGroupMap A K L E).hom'.toFun g.val = τ.val
theorem

actualFiniteDecompositionRestriction_surjective

L70 ↗
EtaleFundamentalGroups.Inertia.actualFiniteDecompositionRestriction_surjective
Documentation

Original decomposition surjects onto the intrinsic decomposition group of every actual finite normalization contraction.

Source context 4 commands

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

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 actualFiniteDecompositionRestriction_surjective
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
    (E : FiniteGaloisIntermediateField K L) :
    Function.Surjective (actualFiniteDecompositionRestriction A K L Q E).hom'.toFun

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