NYLL
Module

NormalizationPrimeOrdinaryFraction.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeOrdinaryFraction
5 declarations indexed from sourceView source ↗

Module documentation

The ordinary henselization fraction field in the original ambient field

The native fraction-ring lift extends the actual injective ordinary-stalk map. Localization extensionality extends the proved decomposition-group fixedness to this actual fraction-field embedding.

Imports4
Imported by3

Declarations

def

ordinaryHenselizationFractionToNormalizationField

L40 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField
Documentation

The actual fraction-ring map extending the original ordinary-stalk embedding into the original ambient field.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v
attribute [local instance] normalizationInertiaImageAction
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
  (Q : Ideal (integralClosure A L)) [Q.IsPrime]
  (hQ : Q.under A = IsLocalRing.maximalIdeal A)
Lean source · statement
def ordinaryHenselizationFractionToNormalizationField :
    FractionRing (ordinaryHenselization A) →+* L
theorem

ordinaryHenselizationFractionToNormalizationField_comp_stalk

L49 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_comp_stalk
Documentation

The fraction-ring map extends the literal ordinary-stalk map.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v
attribute [local instance] normalizationInertiaImageAction
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
  (Q : Ideal (integralClosure A L)) [Q.IsPrime]
  (hQ : Q.under A = IsLocalRing.maximalIdeal A)
Lean source · statement
theorem ordinaryHenselizationFractionToNormalizationField_comp_stalk :
    (ordinaryHenselizationFractionToNormalizationField A K L Q hQ).comp
      (algebraMap (ordinaryHenselization A) (FractionRing (ordinaryHenselization A))) =
      ordinaryHenselizationToNormalizationField A K L Q hQ
theorem

ordinaryHenselizationFractionToNormalizationField_injective

L62 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_injective
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v
attribute [local instance] normalizationInertiaImageAction
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
  (Q : Ideal (integralClosure A L)) [Q.IsPrime]
  (hQ : Q.under A = IsLocalRing.maximalIdeal A)
Lean source · statement
theorem ordinaryHenselizationFractionToNormalizationField_injective :
    Function.Injective (ordinaryHenselizationFractionToNormalizationField A K L Q hQ)
theorem

ordinaryHenselizationFractionToNormalizationField_comp_decomposition

L71 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_comp_decomposition
Documentation

The original decomposition group fixes the actual fraction-field embedding of the ordinary henselization.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v
attribute [local instance] normalizationInertiaImageAction
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
  (Q : Ideal (integralClosure A L)) [Q.IsPrime]
  (hQ : Q.under A = IsLocalRing.maximalIdeal A)
Lean source · statement
theorem ordinaryHenselizationFractionToNormalizationField_comp_decomposition
    (σ : MulAction.stabilizer Gal(L/K) Q) :
    (σ : Gal(L/K)).toRingHom.comp
        (ordinaryHenselizationFractionToNormalizationField A K L Q hQ) =
      ordinaryHenselizationFractionToNormalizationField A K L Q hQ
theorem

ordinaryHenselizationFractionToNormalizationField_range_subset_fixedField

L92 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_range_subset_fixedField
Documentation

The image of the actual ordinary fraction field lies in the original decomposition fixed field. The reverse inclusion remains separate.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v
attribute [local instance] normalizationInertiaImageAction
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L]
  (Q : Ideal (integralClosure A L)) [Q.IsPrime]
  (hQ : Q.under A = IsLocalRing.maximalIdeal A)
Lean source · statement
theorem ordinaryHenselizationFractionToNormalizationField_range_subset_fixedField :
    Set.range (ordinaryHenselizationFractionToNormalizationField A K L Q hQ) ⊆
      (IntermediateField.fixedField (MulAction.stabilizer Gal(L/K) Q) : Set L)

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