NYLL
Module

NormalizationPrimeOrdinaryHenselization.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeOrdinaryHenselization
9 declarations indexed from sourceView source ↗

Module documentation

The actual ordinary henselization inside the original normalization

The original fraction-field and Galois data supply the Henselian property of the literal normalization-prime localization. The ordinary universal map then embeds the constructed henselization into that localization and into the original ambient field. The existing decomposition-group action fixes this embedding by ordinary uniqueness, without acting trivially on the localization residue field.

Imports9
Imported by3

Declarations

def

ordinaryHenselizationToNormalizationPrime

L48 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationPrime
Documentation

The actual ordinary universal map into the literal normalization-prime localization, using only the original fraction-field and prime data.

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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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 ordinaryHenselizationToNormalizationPrime :
    ordinaryHenselization A →+* Localization.AtPrime Q
theorem

ordinaryHenselizationToNormalizationPrime_comp_map

L63 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationPrime_comp_map
Documentation

The original map from A factors through the constructed ordinary henselization and its actual map into the literal localization.

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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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 ordinaryHenselizationToNormalizationPrime_comp_map :
    (ordinaryHenselizationToNormalizationPrime A K L Q hQ).comp
      (ordinaryHenselizationMap A) = integralClosurePrimeBaseMap A L Q
theorem

ordinaryHenselizationToNormalizationPrime_injective

L79 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationPrime_injective
Documentation

Over the original normal local domain, the actual ordinary universal map into the localization is 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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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 ordinaryHenselizationToNormalizationPrime_injective [IsIntegrallyClosed A] :
    Function.Injective (ordinaryHenselizationToNormalizationPrime A K L Q hQ)
def

ordinaryHenselizationToNormalizationField

L95 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationField
Documentation

The ordinary henselization maps into the original ambient field through the prescribed normalization-localization inclusion.

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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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 ordinaryHenselizationToNormalizationField : ordinaryHenselization A →+* L
theorem

ordinaryHenselizationToNormalizationField_comp_map

L99 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationField_comp_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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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 ordinaryHenselizationToNormalizationField_comp_map :
    (ordinaryHenselizationToNormalizationField A K L Q hQ).comp
      (ordinaryHenselizationMap A) = algebraMap A L
theorem

ordinaryHenselizationToNormalizationField_injective

L112 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationField_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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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 ordinaryHenselizationToNormalizationField_injective [IsIntegrallyClosed A] :
    Function.Injective (ordinaryHenselizationToNormalizationField A K L Q hQ)
theorem

ordinaryHenselizationToNormalizationPrime_comp_decomposition

L119 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationPrime_comp_decomposition
Documentation

Every original decomposition-group element fixes the actual image of the ordinary henselization in the literal localization.

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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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 ordinaryHenselizationToNormalizationPrime_comp_decomposition
    (σ : MulAction.stabilizer Gal(L/K) Q) :
    (SchemeTheory.stabilizerLocalizationRingEquiv
      (integralClosure A L) Gal(L/K) Q σ).toRingHom.comp
        (ordinaryHenselizationToNormalizationPrime A K L Q hQ) =
      ordinaryHenselizationToNormalizationPrime A K L Q hQ
theorem

integralClosurePrimeToAmbientField_comp_decomposition

L152 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeToAmbientField_comp_decomposition
Documentation

The original ambient-field action and the existing literal localization action agree on all fractions, by their equality on integral coefficients.

Source context 8 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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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)
omit [IsLocalRing A] [IsSepClosed L] in
Lean source · statement
theorem integralClosurePrimeToAmbientField_comp_decomposition
    (σ : MulAction.stabilizer Gal(L/K) Q) :
    (σ : Gal(L/K)).toRingHom.comp (integralClosurePrimeToAmbientField A K L Q) =
      (integralClosurePrimeToAmbientField A K L Q).comp
        (SchemeTheory.stabilizerLocalizationRingEquiv
          (integralClosure A L) Gal(L/K) Q σ).toRingHom
theorem

ordinaryHenselizationToNormalizationField_comp_decomposition

L179 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationField_comp_decomposition
Documentation

The original decomposition group fixes the actual ordinary-henselization embedding in 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 normalizationInertiaCoefficientCommClass
variable (A : Type u) (K : Type v) (L : Type u)
  [CommRing A] [IsDomain 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 ordinaryHenselizationToNormalizationField_comp_decomposition
    (σ : MulAction.stabilizer Gal(L/K) Q) :
    (σ : Gal(L/K)).toRingHom.comp (ordinaryHenselizationToNormalizationField A K L Q hQ) =
      ordinaryHenselizationToNormalizationField A K L Q hQ

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