NYLL
Module

NormalizationPrimeField.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeField
13 declarations indexed from sourceView source ↗

Module documentation

The actual normalization-prime localization in the ambient Galois field

The shared integral-closure fraction supplier and the existing canonical prime-localization lift construct the literal map into the original field. The native coefficient equations prove injectivity, its base square, and compatibility with each original inertia element. All scalar actions are those of the existing owners; no action on the localization is introduced.

Imports12
Imported by7

Declarations

def

primeLocalizationFieldMap

L38 ↗
EtaleFundamentalGroups.StrictHenselian.primeLocalizationFieldMap
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
def primeLocalizationFieldMap
    (B : Type u) (F : Type v) [CommRing B] [IsDomain B]
    [Field F] [Algebra B F] [IsFractionRing B F]
    (Q : Ideal B) [Q.IsPrime] : Localization.AtPrime Q →+* F
theorem

primeLocalizationFieldMap_comp

L46 ↗
EtaleFundamentalGroups.StrictHenselian.primeLocalizationFieldMap_comp
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem primeLocalizationFieldMap_comp
    (B : Type u) (F : Type v) [CommRing B] [IsDomain B]
    [Field F] [Algebra B F] [IsFractionRing B F]
    (Q : Ideal B) [Q.IsPrime] :
    (primeLocalizationFieldMap B F Q).comp (algebraMap B (Localization.AtPrime Q)) =
      algebraMap B F
theorem

primeLocalizationFieldMap_injective

L58 ↗
EtaleFundamentalGroups.StrictHenselian.primeLocalizationFieldMap_injective
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem primeLocalizationFieldMap_injective
    (B : Type u) (F : Type v) [CommRing B] [IsDomain B]
    [Field F] [Algebra B F] [IsFractionRing B F]
    (Q : Ideal B) [Q.IsPrime] :
    Function.Injective (primeLocalizationFieldMap B F Q)
theorem

integralClosure_subtype_comp

L69 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosure_subtype_comp
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem integralClosure_subtype_comp
    (A : Type u) (L : Type v) [CommRing A] [Field L] [Algebra A L] :
    (integralClosure A L).toSubring.subtype.comp (algebraMap A (integralClosure A L)) =
      algebraMap A L
def

actionInertiaLocalizationRingHom

L74 ↗
EtaleFundamentalGroups.StrictHenselian.actionInertiaLocalizationRingHom
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
def actionInertiaLocalizationRingHom
    (G : Type u) (B : Type v) [Group G] [CommRing B] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (σ : G) (hσ : σ ∈ Q.inertia G) :
    Localization.AtPrime Q →+* Localization.AtPrime Q
theorem

actionInertiaLocalizationRingHom_comp

L81 ↗
EtaleFundamentalGroups.StrictHenselian.actionInertiaLocalizationRingHom_comp
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem actionInertiaLocalizationRingHom_comp
    (G : Type u) (B : Type v) [Group G] [CommRing B] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (σ : G) (hσ : σ ∈ Q.inertia G) :
    (actionInertiaLocalizationRingHom G B Q σ hσ).comp
        (algebraMap B (Localization.AtPrime Q)) =
      (algebraMap B (Localization.AtPrime Q)).comp (MulSemiringAction.toRingHom G B σ)
theorem

primeLocalization_comp_eq_of_coefficients

L92 ↗
EtaleFundamentalGroups.StrictHenselian.primeLocalization_comp_eq_of_coefficients
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem primeLocalization_comp_eq_of_coefficients
    (B : Type u) (F : Type v) [CommRing B] [CommRing F]
    (Q : Ideal B) [Q.IsPrime]
    (i : B →+* F) (j : Localization.AtPrime Q →+* F)
    (τ : F →+* F) (s : B →+* B)
    (e : Localization.AtPrime Q →+* Localization.AtPrime Q)
    (hj : j.comp (algebraMap B (Localization.AtPrime Q)) = i)
    (he : e.comp (algebraMap B (Localization.AtPrime Q)) =
      (algebraMap B (Localization.AtPrime Q)).comp s)
    (hτ : τ.comp i = i.comp s) :
    τ.comp j = j.comp e
def

integralClosurePrimeToAmbientField

L126 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeToAmbientField
Documentation

The prescribed prime-localization map into the original ambient field. Its fraction-field input is supplied by the actual algebraic normalization.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Algebraic
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [Algebra.IsAlgebraic K L]
Lean source · statement
def integralClosurePrimeToAmbientField
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] : Localization.AtPrime Q →+* L
theorem

integralClosurePrimeToAmbientField_comp_coefficient

L133 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeToAmbientField_comp_coefficient
Documentation

The ambient map extends the literal integral-closure inclusion.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Algebraic
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [Algebra.IsAlgebraic K L]
Lean source · statement
theorem integralClosurePrimeToAmbientField_comp_coefficient
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    (integralClosurePrimeToAmbientField A K L Q).comp
        (algebraMap (integralClosure A L) (Localization.AtPrime Q)) =
      (integralClosure A L).toSubring.subtype
theorem

integralClosurePrimeToAmbientField_injective

L143 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeToAmbientField_injective
Documentation

The literal normalization-prime map into the ambient field is injective.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Algebraic
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [Algebra.IsAlgebraic K L]
Lean source · statement
theorem integralClosurePrimeToAmbientField_injective
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    Function.Injective (integralClosurePrimeToAmbientField A K L Q)
theorem

integralClosurePrimeToAmbientField_comp_baseMap

L151 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeToAmbientField_comp_baseMap
Documentation

The original base map is preserved by the actual ambient-field map.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Algebraic
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [Algebra.IsAlgebraic K L]
Lean source · statement
theorem integralClosurePrimeToAmbientField_comp_baseMap
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    (integralClosurePrimeToAmbientField A K L Q).comp (integralClosurePrimeBaseMap A L Q) =
      algebraMap A L
theorem

normalizationInertia_comp_coefficient

L173 ↗
EtaleFundamentalGroups.StrictHenselian.normalizationInertia_comp_coefficient
Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Galois
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L]
attribute [local instance] normalizationInertiaImageAction
omit [IsDomain A] in
Lean source · statement
theorem normalizationInertia_comp_coefficient
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (σ : Gal(L/K)) (hσ : σ ∈ Q.inertia Gal(L/K)) :
    (normalizationPrimeInertiaRingEquiv A K L Q σ hσ).toRingHom.comp
        (algebraMap (integralClosure A L) (Localization.AtPrime Q)) =
      (algebraMap (integralClosure A L) (Localization.AtPrime Q)).comp
        (MulSemiringAction.toRingHom Gal(L/K) (integralClosure A L) σ)
theorem

integralClosurePrimeToAmbientField_comp_inertia

L184 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeToAmbientField_comp_inertia
Documentation

The actual inclusion into the ambient field intertwines each original inertia element with its native automorphism of the literal prime localization.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Galois
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
  [IsScalarTower A K L] [IsGalois K L]
attribute [local instance] normalizationInertiaImageAction
Lean source · statement
theorem integralClosurePrimeToAmbientField_comp_inertia
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (σ : Gal(L/K)) (hσ : σ ∈ Q.inertia Gal(L/K)) :
    σ.toRingHom.comp (integralClosurePrimeToAmbientField A K L Q) =
      (integralClosurePrimeToAmbientField A K L Q).comp
        (normalizationPrimeInertiaRingEquiv A K L Q σ hσ).toRingHom

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