NYLL
Module

NormalizationPrimeStalkFraction.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrimeStalkFraction
15 declarations indexed from sourceView source ↗

Module documentation

The actual strict-stalk fraction field inside the original ambient field

The constructed stalk embedding and the prescribed normalization-localization map form an injective ring map into L. The native fraction-ring lift extends that actual map. Native localization extensionality then transports the already proved inertia fixedness to the fraction ring. The geometric construction uses the reduced A/L inputs; the original Galois inputs supply those properties, and the two prescribed ambient maps agree literally. No reverse fixed-image equality or field comparison is assumed.

Imports14
Imported by6

Declarations

def

injectiveFractionLift

L44 ↗
EtaleFundamentalGroups.StrictHenselian.injectiveFractionLift
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
def injectiveFractionLift
    {R : Type u} {F : Type v} [CommRing R] [Field F]
    (f : R →+* F) (hf : Function.Injective f) : FractionRing R →+* F
theorem

injectiveFractionLift_injective

L50 ↗
EtaleFundamentalGroups.StrictHenselian.injectiveFractionLift_injective
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem injectiveFractionLift_injective
    {R : Type u} {F : Type v} [CommRing R] [Field F]
    (f : R →+* F) (hf : Function.Injective f) :
    Function.Injective (injectiveFractionLift f hf)
theorem

injectiveFractionLift_comp

L57 ↗
EtaleFundamentalGroups.StrictHenselian.injectiveFractionLift_comp
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem injectiveFractionLift_comp
    {R : Type u} {F : Type v} [CommRing R] [Field F]
    (f : R →+* F) (hf : Function.Injective f) :
    (injectiveFractionLift f hf).comp (algebraMap R (FractionRing R)) = f
theorem

injectiveFractionLift_comp_endomorphism

L66 ↗
EtaleFundamentalGroups.StrictHenselian.injectiveFractionLift_comp_endomorphism
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem injectiveFractionLift_comp_endomorphism
    {R : Type u} {F : Type v} [CommRing R] [Field F]
    (f : R →+* F) (hf : Function.Injective f)
    (τ : F →+* F) (hτ : τ.comp f = f) :
    τ.comp (injectiveFractionLift f hf) = injectiveFractionLift f hf
def

normalizationPrimeAmbientMap

L81 ↗
EtaleFundamentalGroups.StrictHenselian.normalizationPrimeAmbientMap
Source context 5 commands

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

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

normalizationPrimeAmbientMap_injective

L92 ↗
EtaleFundamentalGroups.StrictHenselian.normalizationPrimeAmbientMap_injective
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem normalizationPrimeAmbientMap_injective
    (A : Type u) (L : Type v) [CommRing A] [IsDomain A] [Field L]
    [Algebra A L] [FaithfulSMul A L] [Algebra.IsAlgebraic A L]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    Function.Injective (normalizationPrimeAmbientMap A L Q)
theorem

normalizationPrimeAmbientMap_eq

L107 ↗
EtaleFundamentalGroups.StrictHenselian.normalizationPrimeAmbientMap_eq
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
Lean source · statement
theorem normalizationPrimeAmbientMap_eq
    (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]
    [FaithfulSMul A L] [Algebra.IsAlgebraic A L]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    normalizationPrimeAmbientMap A L Q = integralClosurePrimeToAmbientField A K L Q
def

normalizationStalkAmbientMap

L125 ↗
EtaleFundamentalGroups.StrictHenselian.normalizationStalkAmbientMap
Source context 8 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Geometric
variable (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]
omit [IsIntegrallyClosed A] [IsLocalRing A] in
Lean source · full declaration
def normalizationStalkAmbientMap :
    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
    geometricStalk (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue (Localization.AtPrime Q)).comp (integralClosurePrimeBaseMap A L Q))))
      →+* L := by
  intro actualHenselian actualSepClosed
  exact (normalizationPrimeAmbientMap A L Q).comp
    (geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q))
theorem

normalizationStalkAmbientMap_injective

L137 ↗
EtaleFundamentalGroups.StrictHenselian.normalizationStalkAmbientMap_injective
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Geometric
variable (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]
Lean source · full declaration
theorem normalizationStalkAmbientMap_injective
    (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 (normalizationStalkAmbientMap A L Q) := by
  intro actualHenselian actualSepClosed
  exact (normalizationPrimeAmbientMap_injective A L Q).comp
    (geometricStalkToIntegralClosurePrime_injective A L Q hQ)
def

geometricStalkFractionToNormalizationField

L159 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionToNormalizationField
Documentation

The actual fraction ring of the geometric stalk embeds in the original ambient field, through the already constructed normalization-prime embedding.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section MaximalGeometric
variable (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.IsMaximal]
Lean source · full declaration
def geometricStalkFractionToNormalizationField :
    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
    FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue (Localization.AtPrime Q)).comp (integralClosurePrimeBaseMap A L Q)))))
      →+* L := by
  intro actualHenselian actualSepClosed
  exact injectiveFractionLift (normalizationStalkAmbientMap A L Q)
    (normalizationStalkAmbientMap_injective A L Q (integralClosure_maximalPrime_under A L Q))
theorem

geometricStalkFractionToNormalizationField_injective

L173 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionToNormalizationField_injective
Documentation

The constructed fraction-ring map is injective, by the native field-map injectivity theorem applied to the actual injective stalk map.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section MaximalGeometric
variable (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.IsMaximal]
Lean source · full declaration
theorem geometricStalkFractionToNormalizationField_injective :
    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 (geometricStalkFractionToNormalizationField A L Q) := by
  intro actualHenselian actualSepClosed
  exact injectiveFractionLift_injective (normalizationStalkAmbientMap A L Q)
    (normalizationStalkAmbientMap_injective A L Q (integralClosure_maximalPrime_under A L Q))
theorem

geometricStalkFractionToNormalizationField_comp_endomorphism

L183 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionToNormalizationField_comp_endomorphism
Source context 7 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section MaximalGeometric
variable (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.IsMaximal]
Lean source · full declaration
theorem geometricStalkFractionToNormalizationField_comp_endomorphism
    (τ : L →+* L) :
    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
    τ.comp (normalizationStalkAmbientMap A L Q) = normalizationStalkAmbientMap A L Q →
      τ.comp (geometricStalkFractionToNormalizationField A L Q) =
        geometricStalkFractionToNormalizationField A L Q := by
  intro actualHenselian actualSepClosed hτ
  exact injectiveFractionLift_comp_endomorphism (normalizationStalkAmbientMap A L Q)
    (normalizationStalkAmbientMap_injective A L Q (integralClosure_maximalPrime_under A L Q)) τ hτ
theorem

normalizationStalkAmbientMap_comp_inertia

L208 ↗
EtaleFundamentalGroups.StrictHenselian.normalizationStalkAmbientMap_comp_inertia
Source context 9 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Galois
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]
attribute [local instance] normalizationInertiaImageAction
omit [IsIntegrallyClosed A] in
Lean source · full declaration
theorem normalizationStalkAmbientMap_comp_inertia
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    (σ : Gal(L/K)) (hσ : σ ∈ Q.inertia Gal(L/K)) :
    let : Algebra.IsAlgebraic A L :=
      (IsFractionRing.comap_isAlgebraic_iff (A := A) (K := K) (C := L)).mpr inferInstance
    let : FaithfulSMul A L :=
      (Module.isTorsionFree_iff_faithfulSMul (R := A) (A := L)).mp
        (Module.IsTorsionFree.trans_faithfulSMul A K L)
    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
    σ.toRingHom.comp (normalizationStalkAmbientMap A L Q) =
      normalizationStalkAmbientMap A L Q := by
  intro actualAlgebraic actualFaithful actualHenselian actualSepClosed
  change σ.toRingHom.comp ((normalizationPrimeAmbientMap A L Q).comp
      (geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q))) =
    (normalizationPrimeAmbientMap A L Q).comp
      (geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q))
  rw [normalizationPrimeAmbientMap_eq A K L Q]
  rw [← RingHom.comp_assoc,
    integralClosurePrimeToAmbientField_comp_inertia A K L Q σ hσ,
    RingHom.comp_assoc, normalizationPrimeInertia_comp_geometricStalkMap A K L Q σ hσ]
theorem

geometricStalkFractionToNormalizationField_comp_stalk

L235 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionToNormalizationField_comp_stalk
Documentation

The actual geometric-stalk fraction-field map extends the literal stalk map into the original ambient field. Both maps are the existing constructed maps, and the equality is their original localization computation.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Galois
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]
attribute [local instance] normalizationInertiaImageAction
Lean source · full declaration
theorem geometricStalkFractionToNormalizationField_comp_stalk
    (Q : Ideal (integralClosure A L)) [Q.IsMaximal] :
    let : Algebra.IsAlgebraic A L :=
      (IsFractionRing.comap_isAlgebraic_iff (A := A) (K := K) (C := L)).mpr inferInstance
    let : FaithfulSMul A L :=
      (Module.isTorsionFree_iff_faithfulSMul (R := A) (A := L)).mp
        (Module.IsTorsionFree.trans_faithfulSMul A K L)
    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
    (geometricStalkFractionToNormalizationField A L Q).comp
        (algebraMap
          (geometricStalk (Spec.map (CommRingCat.ofHom
            ((IsLocalRing.residue (Localization.AtPrime Q)).comp
              (integralClosurePrimeBaseMap A L Q)))))
          (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom
            ((IsLocalRing.residue (Localization.AtPrime Q)).comp
              (integralClosurePrimeBaseMap A L Q))))))) =
      (integralClosurePrimeToAmbientField A K L Q).comp
        (geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q)) := by
  intro actualAlgebraic actualFaithful actualHenselian actualSepClosed
  exact (injectiveFractionLift_comp (normalizationStalkAmbientMap A L Q)
    (normalizationStalkAmbientMap_injective A L Q
      (integralClosure_maximalPrime_under A L Q))).trans
        (congrArg
          (fun j : Localization.AtPrime Q →+* L =>
            j.comp (geometricStalkToHenselian (integralClosurePrimeBaseMap A L Q)))
          (normalizationPrimeAmbientMap_eq A K L Q))
theorem

geometricStalkFractionToNormalizationField_comp_inertia

L268 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionToNormalizationField_comp_inertia
Documentation

Every original inertia element fixes the constructed image of the actual geometric-stalk fraction field in L. This is the forward fixed-field inclusion; the reverse inclusion is not a premise or conclusion here.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups.StrictHenselian
open EtaleFundamentalGroups.Inertia
universe u v w
section Galois
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]
attribute [local instance] normalizationInertiaImageAction
Lean source · full declaration
theorem geometricStalkFractionToNormalizationField_comp_inertia
    (Q : Ideal (integralClosure A L)) [Q.IsMaximal]
    (σ : Gal(L/K)) (hσ : σ ∈ Q.inertia Gal(L/K)) :
    let : Algebra.IsAlgebraic A L :=
      (IsFractionRing.comap_isAlgebraic_iff (A := A) (K := K) (C := L)).mpr inferInstance
    let : FaithfulSMul A L :=
      (Module.isTorsionFree_iff_faithfulSMul (R := A) (A := L)).mp
        (Module.IsTorsionFree.trans_faithfulSMul A K L)
    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
    σ.toRingHom.comp (geometricStalkFractionToNormalizationField A L Q) =
      geometricStalkFractionToNormalizationField A L Q := by
  intro actualAlgebraic actualFaithful actualHenselian actualSepClosed
  exact geometricStalkFractionToNormalizationField_comp_endomorphism A L Q σ.toRingHom
    (normalizationStalkAmbientMap_comp_inertia A K L Q σ hσ)

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