NYLL
Module

NormalizationPrimeOrdinaryDecomposition.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeOrdinaryDecomposition
4 declarations indexed from sourceView source ↗

Module documentation

The original decomposition group fixes exactly the ordinary fraction image

An ambient automorphism fixing the actual ordinary henselization preserves unit status of the original integral coefficients in the literal prime localization. This follows from the proved locality of the integral closure over the Henselian base. Hence it preserves the original prime itself. Together with ordinary uniqueness this identifies the original decomposition group as the fixing group of the actual embedded ordinary fraction field.

Imports7
Imported by3

Declarations

theorem

ordinaryHenselizationToNormalizationField_comp_eq_self_imp_decomposition

L46 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationField_comp_eq_self_imp_decomposition
Documentation

Fixing the actual ordinary henselization forces an original ambient automorphism to stabilize the original normalization prime.

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] [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_eq_self_imp_decomposition
    (σ : Gal(L/K))
    (hσ : σ.toRingHom.comp (ordinaryHenselizationToNormalizationField A K L Q hQ) =
      ordinaryHenselizationToNormalizationField A K L Q hQ) :
    σ ∈ MulAction.stabilizer Gal(L/K) Q
theorem

ordinaryHenselizationToNormalizationField_comp_eq_self_iff

L106 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationToNormalizationField_comp_eq_self_iff
Documentation

The original decomposition subgroup is detected by the actual ordinary henselization embedding, with the original base and ambient field retained.

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] [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_eq_self_iff
    (σ : Gal(L/K)) :
    σ.toRingHom.comp (ordinaryHenselizationToNormalizationField A K L Q hQ) =
        ordinaryHenselizationToNormalizationField A K L Q hQ ↔
      σ ∈ MulAction.stabilizer Gal(L/K) Q
theorem

ordinaryHenselizationFractionToNormalizationField_comp_eq_self_iff

L121 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_comp_eq_self_iff
Documentation

Fixing the actual ordinary fraction embedding is equivalent to belonging to the original decomposition subgroup.

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
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)
variable [IsIntegrallyClosed A]
Lean source · statement
theorem ordinaryHenselizationFractionToNormalizationField_comp_eq_self_iff
    (σ : Gal(L/K)) :
    σ.toRingHom.comp (ordinaryHenselizationFractionToNormalizationField A K L Q hQ) =
        ordinaryHenselizationFractionToNormalizationField A K L Q hQ ↔
      σ ∈ MulAction.stabilizer Gal(L/K) Q
theorem

ordinaryHenselizationFractionToNormalizationField_fixingSubgroup

L147 ↗
EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationFractionToNormalizationField_fixingSubgroup
Documentation

The original decomposition group is exactly the subgroup fixing the range of the actual ordinary-henselization fraction field.

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
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)
variable [IsIntegrallyClosed A]
Lean source · statement
theorem ordinaryHenselizationFractionToNormalizationField_fixingSubgroup :
    fixingSubgroup Gal(L/K)
        (Set.range (ordinaryHenselizationFractionToNormalizationField A K L Q hQ)) =
      MulAction.stabilizer Gal(L/K) Q

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