NYLL
Module

NormalizationPrimeEmbedding.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeEmbedding
6 declarations indexed from sourceView source ↗

Module documentation

Embedding the actual geometric stalk in a normalization prime localization

The base map is the literal composite through the integral closure. Its injection follows from the original embedding into the ambient field and native prime-localization injectivity. Contraction to the closed point makes it local. The previously constructed stalk map is therefore injective.

Algebraicity and faithfulness over the base are ordinary consequences of the original fraction-field data, not hypotheses about the stalk comparison. The fraction-field scalar construction is confined to the strict-target supplier; the geometric proof uses only the original A-algebra structure on L.

Imports13
Imported by14

Declarations

def

integralClosurePrimeBaseMap

L42 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeBaseMap
Documentation

The original base map to the literal normalization prime localization.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
Lean source · statement
def integralClosurePrimeBaseMap
    (A : Type u) (L : Type v) [CommRing A] [Field L] [Algebra A L]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    A →+* Localization.AtPrime Q
theorem

integralClosurePrimeBaseMap_injective

L51 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeBaseMap_injective
Documentation

The literal base map is injective whenever the original field action is faithful. No injection of a geometric stalk is assumed.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
Lean source · statement
theorem integralClosurePrimeBaseMap_injective
    (A : Type u) (L : Type v) [CommRing A] [Field L] [Algebra A L]
    [FaithfulSMul A L] (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    Function.Injective (integralClosurePrimeBaseMap A L Q)
theorem

integralClosurePrimeBaseMap_isLocalHom

L64 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosurePrimeBaseMap_isLocalHom
Documentation

Contraction of the original normalization prime to the closed point makes the literal localization map local.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
Lean source · statement
theorem integralClosurePrimeBaseMap_isLocalHom
    (A : Type u) (L : Type v) [CommRing A] [IsLocalRing A] [Field L] [Algebra A L]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (hQ : Q.under A = IsLocalRing.maximalIdeal A) :
    IsLocalHom (integralClosurePrimeBaseMap A L Q)
theorem

integralClosure_maximalPrime_under

L82 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosure_maximalPrime_under
Documentation

A maximal normalization prime lies over the closed point of the local base, by integrality of the actual integral closure.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
Lean source · statement
theorem integralClosure_maximalPrime_under
    (A : Type u) (L : Type v) [CommRing A] [IsLocalRing A] [Field L] [Algebra A L]
    (Q : Ideal (integralClosure A L)) [Q.IsMaximal] :
    Q.under A = IsLocalRing.maximalIdeal A
theorem

integralClosure_primeLocalization_strictHenselian_of_algebraic

L91 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosure_primeLocalization_strictHenselian_of_algebraic
Documentation

The strict-target supplier can be used with algebraicity over the base itself. The only fraction-field action is the existing native lift.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
Lean source · statement
theorem integralClosure_primeLocalization_strictHenselian_of_algebraic
    (A : Type u) (L : Type v) [CommRing A] [IsDomain A] [Field L] [Algebra A L]
    [FaithfulSMul A L] [Algebra.IsAlgebraic A L] [IsSepClosed L]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    HenselianLocalRing (Localization.AtPrime Q) ∧
      IsSepClosed (IsLocalRing.ResidueField (Localization.AtPrime Q))
theorem

geometricStalkToIntegralClosurePrime_injective

L107 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkToIntegralClosurePrime_injective
Documentation

The actual geometric-stalk map into the literal normalization prime localization is injective. Its locality and base injection are derived from the original prime contraction and the actual normalization inclusions.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
universe u v
Lean source · full declaration
theorem geometricStalkToIntegralClosurePrime_injective
    (A L : Type u) [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [IsLocalRing A]
    [Field L] [Algebra A L] [FaithfulSMul A L] [Algebra.IsAlgebraic A L] [IsSepClosed L]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (hQ : Q.under A = IsLocalRing.maximalIdeal A) :
    let : HenselianLocalRing (Localization.AtPrime Q) :=
      (integralClosure_primeLocalization_strictHenselian_of_algebraic A L Q).1
    let : IsSepClosed (IsLocalRing.ResidueField (Localization.AtPrime Q)) :=
      (integralClosure_primeLocalization_strictHenselian_of_algebraic A L Q).2
    Function.Injective (geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q)) := by
  intro actualHenselian actualSepClosed
  have : IsLocalHom (integralClosurePrimeBaseMap A L Q) :=
    integralClosurePrimeBaseMap_isLocalHom A L Q hQ
  exact geometricStalkToHenselian_injective (integralClosurePrimeBaseMap A L Q)
    (integralClosurePrimeBaseMap_injective A L Q)

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