Module

NormalizationPrimeOrdinaryFixedField.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeOrdinaryFixedField

4 declarations indexed from sourceView source ↗

Module documentation

The actual ordinary fraction image is the original decomposition fixed field

The actual fraction-ring image contains the original base fraction field: write a base-field element as a quotient of original base-ring elements and use the proved coefficient square. Hence the image is an actual intermediate field of the original extension. Its proved fixing subgroup is the original decomposition subgroup, so the native infinite Galois correspondence identifies that same image with the decomposition fixed field.

Imports6

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeOrdinaryDecomposition
Nyll.SchemeTheory.RingTheory.Ramification.FiniteLevelInertiaImage
Mathlib.Algebra.Field.Subfield.Basic
Mathlib.FieldTheory.IntermediateField.Basic
Mathlib.FieldTheory.Galois.Infinite
Mathlib.RingTheory.Localization.FractionRing

Imported by1

Nyll.EtaleFundamentalGroups.StrictHenselian.All

def

ordinaryHenselizationFractionImage

L45 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionImage

Documentation

The range of the actual ordinary fraction map as an intermediate field of the original L/K. Containment of K is proved from original fractions.

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 ordinaryHenselizationFractionImage : IntermediateField K L

theorem

ordinaryHenselizationFractionImage_coe

L71 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionImage_coe

Documentation

The intermediate-field carrier is literally the actual fraction-map range.

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 ordinaryHenselizationFractionImage_coe :
    (ordinaryHenselizationFractionImage A K L Q hQ : Set L) =
      Set.range (ordinaryHenselizationFractionToNormalizationField A K L Q hQ)

theorem

ordinaryHenselizationFractionToNormalizationField_range_eq_fixedField

L77 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_range_eq_fixedField

Documentation

The image of the actual ordinary henselization fraction field is exactly the field fixed by the original normalization-prime decomposition subgroup.

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_eq_fixedField :
    Set.range (ordinaryHenselizationFractionToNormalizationField A K L Q hQ) =
      (IntermediateField.fixedField (MulAction.stabilizer Gal(L/K) Q) : Set L)

theorem

ordinaryHenselizationFractionToNormalizationField_ringRange_eq_fixedField

L90 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_ringRange_eq_fixedField

Documentation

Bundled subring form of the literal actual-image equality.

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_ringRange_eq_fixedField :
    (ordinaryHenselizationFractionToNormalizationField A K L Q hQ).range =
      (IntermediateField.fixedField (MulAction.stabilizer Gal(L/K) Q)).toSubalgebra.toSubring

Module documentation

The actual ordinary fraction image is the original decomposition fixed field

Declarations

ordinaryHenselizationFractionImage

ordinaryHenselizationFractionImage_coe

ordinaryHenselizationFractionToNormalizationField_range_eq_fixedField

ordinaryHenselizationFractionToNormalizationField_ringRange_eq_fixedField