NYLL
Module

Basic.lean

Nyll.EtaleFundamentalGroups.Normalization.Localization.Basic
5 declarations indexed from sourceView source ↗

Module documentation

Normalization after localization at a prime

This file uses the canonical fraction-field factorization from FractionFieldLocalization to relate a prime localization to the normalization in a field extension. The normalization inclusion is obtained by base-changing integrality, after which we specialize mathlib's theorem that integral closure commutes with localization.

Imports3
Imported by5

Declarations

def

integralClosureLocalizationRingHom

L35 ↗
EtaleFundamentalGroups.integralClosureLocalizationRingHom
Documentation

The underlying inclusion of the original normalization into the normalization after localizing the base at P.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
Lean source · statement
def integralClosureLocalizationRingHom
    (P : Ideal A) [P.IsPrime]
    [Algebra (Localization.AtPrime P) L]
    [IsScalarTower A (Localization.AtPrime P) L] :
    integralClosure A L →+*
      integralClosure (Localization.AtPrime P) L
abbrev

integralClosureLocalizationAlgebra

L50 ↗
EtaleFundamentalGroups.integralClosureLocalizationAlgebra
Documentation

The canonical algebra structure induced by integralClosureLocalizationRingHom.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
Lean source · statement
abbrev integralClosureLocalizationAlgebra
    (P : Ideal A) [P.IsPrime]
    [Algebra (Localization.AtPrime P) L]
    [IsScalarTower A (Localization.AtPrime P) L] :
    Algebra (integralClosure A L)
      (integralClosure (Localization.AtPrime P) L)
def

integralClosureLocalizationAlgHom

L60 ↗
EtaleFundamentalGroups.integralClosureLocalizationAlgHom
Documentation

The canonical inclusion from the original normalization into the normalization after localizing the base at P.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
Lean source · full declaration
def integralClosureLocalizationAlgHom
    (P : Ideal A) [P.IsPrime]
    [Algebra (Localization.AtPrime P) L]
    [IsScalarTower A (Localization.AtPrime P) L] :
    letI := integralClosureLocalizationAlgebra (L := L) P
    integralClosure A L →ₐ[A]
      integralClosure (Localization.AtPrime P) L := by
  letI := integralClosureLocalizationAlgebra (L := L) P
  refine
    { toRingHom := integralClosureLocalizationRingHom (L := L) P
      commutes' := fun x ↦ Subtype.ext ?_ }
  rfl
theorem

isLocalization_integralClosure_localizationAtPrime

L76 ↗
EtaleFundamentalGroups.isLocalization_integralClosure_localizationAtPrime
Documentation

The normalization of the prime localization inside L is the localization of the original normalization at the image of Pᶜ.

Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
omit [IsDomain A] in
Lean source · full declaration
theorem isLocalization_integralClosure_localizationAtPrime
    (P : Ideal A) [P.IsPrime] :
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI := localizationAtPrimeToExtension_isScalarTower (K := K) (L := L) P
    letI := integralClosureLocalizationAlgebra (L := L) P
    IsLocalization
      (Algebra.algebraMapSubmonoid (integralClosure A L) P.primeCompl)
      (integralClosure (Localization.AtPrime P) L) := by
  let := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  let hALocL : IsScalarTower A (Localization.AtPrime P) L :=
    localizationAtPrimeToExtension_isScalarTower (K := K) (L := L) P
  let : IsScalarTower A (Localization.AtPrime P) L := hALocL
  let := integralClosureLocalizationAlgebra (L := L) P
  let hAB : IsScalarTower A (integralClosure A L)
      (integralClosure (Localization.AtPrime P) L) :=
    IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  let : IsScalarTower A (integralClosure A L)
      (integralClosure (Localization.AtPrime P) L) := hAB
  let hBL : IsScalarTower (integralClosure A L)
      (integralClosure (Localization.AtPrime P) L) L :=
    IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  let : IsScalarTower (integralClosure A L)
      (integralClosure (Localization.AtPrime P) L) L := hBL
  let : IsLocalization
      (Algebra.algebraMapSubmonoid L P.primeCompl) L :=
    IsLocalization.of_le_isUnit fun y hy ↦ by
      rcases hy with ⟨x, hx, rfl⟩
      change IsUnit (algebraMap A L x)
      rw [isUnit_iff_ne_zero, IsScalarTower.algebraMap_apply A K L,
        map_ne_zero_iff _ (algebraMap K L).injective,
        map_ne_zero_iff _ (IsFractionRing.injective A K)]
      exact fun h ↦ hx (h ▸ P.zero_mem)
  have hLocal : IsLocalization
      (Algebra.algebraMapSubmonoid (integralClosure A L) P.primeCompl)
      (integralClosure (Localization.AtPrime P) L) :=
    @IsLocalization.integralClosure
      A _ L _ _ (Localization.AtPrime P) L _ _ _ _ _ _ _ hALocL
      P.primeCompl _ _ (integralClosureLocalizationAlgebra (L := L) P) hBL hAB
  exact hLocal
theorem

moduleFinite_integralClosure_localizationAtPrime

L121 ↗
EtaleFundamentalGroups.moduleFinite_integralClosure_localizationAtPrime
Documentation

Finiteness of a normalization is preserved when the base is localized at a prime. The target normalization is identified with the corresponding localization of the original normalization, so no finiteness assumption on the localized ring is needed.

Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
variable {A : Type uA} {K : Type uK} {L : Type uL}
variable [CommRing A] [IsDomain A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
omit [IsDomain A] in
Lean source · full declaration
theorem moduleFinite_integralClosure_localizationAtPrime
    [Module.Finite A (integralClosure A L)]
    (P : Ideal A) [P.IsPrime] :
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    letI := localizationAtPrimeToExtension_isScalarTower
      (K := K) (L := L) P
    Module.Finite (Localization.AtPrime P)
      (integralClosure (Localization.AtPrime P) L) := by
  let := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  let : IsScalarTower A (Localization.AtPrime P) L :=
    localizationAtPrimeToExtension_isScalarTower (K := K) (L := L) P
  let := integralClosureLocalizationAlgebra (L := L) P
  let : IsLocalization
      (Algebra.algebraMapSubmonoid (integralClosure A L) P.primeCompl)
      (integralClosure (Localization.AtPrime P) L) :=
    isLocalization_integralClosure_localizationAtPrime
      (K := K) (L := L) P
  let : IsScalarTower A (integralClosure A L)
      (integralClosure (Localization.AtPrime P) L) :=
    IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  let : IsScalarTower A (Localization.AtPrime P)
      (integralClosure (Localization.AtPrime P) L) :=
    IsScalarTower.of_algebraMap_eq fun x ↦
      Subtype.ext <|
        IsScalarTower.algebraMap_apply A (Localization.AtPrime P) L x
  exact Module.Finite.of_isLocalization
    A (integralClosure A L) P.primeCompl

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