Module

AtMappedPrimeEquiv.lean

Nyll.SchemeTheory.RingTheory.Localization.AtMappedPrimeEquiv

3 declarations indexed from sourceView source ↗

Module documentation

Localizing a ring equivalence at a prime

An algebra equivalence carries the complement of a prime ideal onto the complement of its image. Hence it induces an algebra equivalence between the corresponding local rings. The explicit formula on elements from the base ring is retained for later transport of distinguished root parameters.

Imports1

Mathlib.RingTheory.Localization.AtPrime.Basic

Imported by3

theorem

localizationAtMappedPrime_map_primeCompl

L30 ↗

EtaleFundamentalGroups.localizationAtMappedPrime_map_primeCompl

Documentation

An algebra equivalence maps the complement of a prime onto the complement of the image prime.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uR uS
variable {A : Type uA} {R : Type uR} {S : Type uS}
variable [CommRing A] [CommRing R] [CommRing S]
variable [Algebra A R] [Algebra A S]

Lean source · statement

theorem localizationAtMappedPrime_map_primeCompl
    (e : R ≃ₐ[A] S) (P : Ideal R) [P.IsPrime] :
    Submonoid.map e P.primeCompl =
      (P.map e.toRingEquiv).primeCompl

def

localizationAtMappedPrimeAlgEquiv

L52 ↗

EtaleFundamentalGroups.localizationAtMappedPrimeAlgEquiv

Documentation

An algebra equivalence induces an algebra equivalence of the local rings at a prime and its image.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uR uS
variable {A : Type uA} {R : Type uR} {S : Type uS}
variable [CommRing A] [CommRing R] [CommRing S]
variable [Algebra A R] [Algebra A S]

Lean source · statement

def localizationAtMappedPrimeAlgEquiv
    (e : R ≃ₐ[A] S) (P : Ideal R) [P.IsPrime] :
    Localization.AtPrime P ≃ₐ[A]
      Localization.AtPrime (P.map e.toRingEquiv)

theorem

localizationAtMappedPrimeAlgEquiv_algebraMap

L65 ↗

EtaleFundamentalGroups.localizationAtMappedPrimeAlgEquiv_algebraMap

Documentation

On elements coming from the original ring, the localized equivalence is the original equivalence followed by the target localization map.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uR uS
variable {A : Type uA} {R : Type uR} {S : Type uS}
variable [CommRing A] [CommRing R] [CommRing S]
variable [Algebra A R] [Algebra A S]

Lean source · statement

theorem localizationAtMappedPrimeAlgEquiv_algebraMap
    (e : R ≃ₐ[A] S) (P : Ideal R) [P.IsPrime] (x : R) :
    localizationAtMappedPrimeAlgEquiv e P
        (algebraMap R (Localization.AtPrime P) x) =
      algebraMap S
        (Localization.AtPrime (P.map e.toRingEquiv)) (e x)

Module documentation

Localizing a ring equivalence at a prime

Declarations

localizationAtMappedPrime_map_primeCompl

localizationAtMappedPrimeAlgEquiv

localizationAtMappedPrimeAlgEquiv_algebraMap