NYLL
Module

FieldLocalization.lean

Nyll.SchemeTheory.RingTheory.Localization.Fraction.FieldLocalization
7 declarations indexed from sourceView source ↗

Module documentation

A prime localization inside a chosen fraction field

This file fixes the canonical algebra maps from a prime localization into an arbitrary chosen fraction field and then into a field extension. The latter map is defined by composition through the fraction field, so the two scalar towers are definitionally compatible and the localization lift is constructed only once.

Imports2
  • Mathlib.RingTheory.Localization.Integral
  • Mathlib.RingTheory.Localization.LocalizationLocalization
Imported by13

Declarations

theorem

integralClosure_isFractionRing_of_fractionField_algebraic

L30 ↗
EtaleFundamentalGroups.integralClosure_isFractionRing_of_fractionField_algebraic
Documentation

An algebraic extension of the displayed fraction field is the fraction field of the actual integral closure. This is the existing normalization supplier, now shared without changing its proof.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL
Lean source · statement
theorem integralClosure_isFractionRing_of_fractionField_algebraic
    (A : Type uA) (K : Type uK) (L : Type uL)
    [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] :
    IsFractionRing (integralClosure A L) L
abbrev

localizationAtPrimeToFractionFieldAlgebra

L50 ↗
EtaleFundamentalGroups.localizationAtPrimeToFractionFieldAlgebra
Documentation

The canonical map from the localization of A at P to a chosen fraction field of A.

Source context 6 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}
variable [CommRing A] [IsDomain A]
variable [Field K] [Algebra A K] [IsFractionRing A K]
Lean source · statement
abbrev localizationAtPrimeToFractionFieldAlgebra
    (P : Ideal A) [P.IsPrime] :
    Algebra (Localization.AtPrime P) K
theorem

localizationAtPrimeToFractionField_isScalarTower

L65 ↗
EtaleFundamentalGroups.localizationAtPrimeToFractionField_isScalarTower
Documentation

The fraction-field map from a prime localization extends the original map from A.

Source context 7 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}
variable [CommRing A] [IsDomain A]
variable [Field K] [Algebra A K] [IsFractionRing A K]
omit [IsDomain A] in
Lean source · full declaration
theorem localizationAtPrimeToFractionField_isScalarTower
    (P : Ideal A) [P.IsPrime] :
    letI := localizationAtPrimeToFractionFieldAlgebra (K := K) P
    IsScalarTower A (Localization.AtPrime P) K := by
  let := localizationAtPrimeToFractionFieldAlgebra (K := K) P
  exact IsScalarTower.of_algebraMap_eq' (IsLocalization.lift_comp _).symm
theorem

localizationAtPrimeToFractionField_isFractionRing

L74 ↗
EtaleFundamentalGroups.localizationAtPrimeToFractionField_isFractionRing
Documentation

A chosen fraction field of A is also a fraction field of every prime localization of A, for the canonical map above.

Source context 6 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}
variable [CommRing A] [IsDomain A]
variable [Field K] [Algebra A K] [IsFractionRing A K]
Lean source · full declaration
theorem localizationAtPrimeToFractionField_isFractionRing
    (P : Ideal A) [P.IsPrime] :
    letI := localizationAtPrimeToFractionFieldAlgebra (K := K) P
    IsFractionRing (Localization.AtPrime P) K := by
  let := localizationAtPrimeToFractionFieldAlgebra (K := K) P
  let : IsScalarTower A (Localization.AtPrime P) K :=
    localizationAtPrimeToFractionField_isScalarTower (K := K) P
  exact IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
    P.primeCompl (Localization.AtPrime P) K
abbrev

localizationAtPrimeToExtensionAlgebra

L88 ↗
EtaleFundamentalGroups.localizationAtPrimeToExtensionAlgebra
Documentation

The map from the localization of A at P to L, factored canonically through the chosen fraction field K.

Source context 7 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}
variable [CommRing A] [IsDomain A]
variable [Field K] [Algebra A K] [IsFractionRing A K]
variable {L : Type uL} [Field L] [Algebra K L]
Lean source · statement
abbrev localizationAtPrimeToExtensionAlgebra
    (P : Ideal A) [P.IsPrime] :
    Algebra (Localization.AtPrime P) L
theorem

localizationAtPrimeToFractionFieldToExtension_isScalarTower

L98 ↗
EtaleFundamentalGroups.localizationAtPrimeToFractionFieldToExtension_isScalarTower
Documentation

The prime-localization, fraction-field, and extension maps form a scalar tower by construction.

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}
variable [CommRing A] [IsDomain A]
variable [Field K] [Algebra A K] [IsFractionRing A K]
variable {L : Type uL} [Field L] [Algebra K L]
omit [IsDomain A] in
Lean source · full declaration
theorem localizationAtPrimeToFractionFieldToExtension_isScalarTower
    (P : Ideal A) [P.IsPrime] :
    letI := localizationAtPrimeToFractionFieldAlgebra (K := K) P
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    IsScalarTower (Localization.AtPrime P) K L := by
  let := localizationAtPrimeToFractionFieldAlgebra (K := K) P
  let := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  exact IsScalarTower.of_algebraMap_eq' rfl
theorem

localizationAtPrimeToExtension_isScalarTower

L112 ↗
EtaleFundamentalGroups.localizationAtPrimeToExtension_isScalarTower
Documentation

The canonical localization map is compatible with the original map A → L.

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}
variable [CommRing A] [IsDomain A]
variable [Field K] [Algebra A K] [IsFractionRing A K]
variable {L : Type uL} [Field L] [Algebra K L]
variable [Algebra A L] [IsScalarTower A K L]
omit [IsDomain A] in
Lean source · full declaration
theorem localizationAtPrimeToExtension_isScalarTower
    (P : Ideal A) [P.IsPrime] :
    letI := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
    IsScalarTower A (Localization.AtPrime P) L := by
  let := localizationAtPrimeToFractionFieldAlgebra (K := K) P
  let : IsScalarTower A (Localization.AtPrime P) K :=
    localizationAtPrimeToFractionField_isScalarTower (K := K) P
  let := localizationAtPrimeToExtensionAlgebra (K := K) (L := L) P
  refine IsScalarTower.of_algebraMap_eq fun x ↦ ?_
  change algebraMap A L x =
    algebraMap K L
      (algebraMap (Localization.AtPrime P) K
        (algebraMap A (Localization.AtPrime P) x))
  rw [← IsScalarTower.algebraMap_apply A (Localization.AtPrime P) K,
    ← IsScalarTower.algebraMap_apply A K L]

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