Localizations of commutative rings at the complement of a prime ideal #

Main definitions #

IsLocalization.AtPrime (P : Ideal R) [IsPrime P] (S : Type*) expresses that S is a localization at (the complement of) a prime ideal P, as an abbreviation of IsLocalization P.prime_compl S

Main results #

IsLocalization.AtPrime.localRing: a theorem (not an instance) stating a localization at the complement of a prime ideal is a local ring

Implementation notes #

See RingTheory.Localization.Basic for a design overview.

Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

source

def Ideal.primeCompl {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : Ideal.IsPrime P] :

Submonoid R

The complement of a prime ideal P ⊆ R is a submonoid of R.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Ideal.primeCompl_le_nonZeroDivisors {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : Ideal.IsPrime P] [NoZeroDivisors R] :

Ideal.primeCompl P ≤ nonZeroDivisors R

source

@[inline, reducible]

abbrev IsLocalization.AtPrime {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : Ideal.IsPrime P] :

Prop

Given a prime ideal P, the typeclass IsLocalization.AtPrime S P states that S is isomorphic to the localization of R at the complement of P.

Equations

IsLocalization.AtPrime S P = IsLocalization (Ideal.primeCompl P) S

Instances For

source

@[inline, reducible]

abbrev Localization.AtPrime {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : Ideal.IsPrime P] :

Type u_1

Given a prime ideal P, Localization.AtPrime P is a localization of R at the complement of P, as a quotient type.

Equations

Localization.AtPrime P = Localization (Ideal.primeCompl P)

Instances For

source

theorem IsLocalization.AtPrime.Nontrivial {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : Ideal.IsPrime P] [IsLocalization.AtPrime S P] :

Nontrivial S

source

theorem IsLocalization.AtPrime.localRing {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (P : Ideal R) [hp : Ideal.IsPrime P] [IsLocalization.AtPrime S P] :

LocalRing S

source

instance Localization.AtPrime.localRing {R : Type u_1} [CommSemiring R] (P : Ideal R) [hp : Ideal.IsPrime P] :

LocalRing (Localization (Ideal.primeCompl P))

The localization of R at the complement of a prime ideal is a local ring.

Equations

@Localization.AtPrime.localRing = @Localization.AtPrime.localRing.proof_1

source

instance IsLocalization.isDomain_of_local_atPrime {A : Type u_4} [CommRing A] [IsDomain A] {P : Ideal A} :

∀ (x : Ideal.IsPrime P), IsDomain (Localization.AtPrime P)

The localization of an integral domain at the complement of a prime ideal is an integral domain.

Equations

@IsLocalization.isDomain_of_local_atPrime = @IsLocalization.isDomain_of_local_atPrime.proof_1

source

theorem IsLocalization.AtPrime.isUnit_to_map_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : Ideal.IsPrime I] [IsLocalization.AtPrime S I] (x : R) :

IsUnit (↑(algebraMap R S) x) ↔ x ∈ Ideal.primeCompl I

source

theorem IsLocalization.AtPrime.to_map_mem_maximal_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : Ideal.IsPrime I] [IsLocalization.AtPrime S I] (x : R) (h : optParam (LocalRing S) (_ : LocalRing S)) :

↑(algebraMap R S) x ∈ LocalRing.maximalIdeal S ↔ x ∈ I

source

theorem IsLocalization.AtPrime.comap_maximalIdeal {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : Ideal.IsPrime I] [IsLocalization.AtPrime S I] (h : optParam (LocalRing S) (_ : LocalRing S)) :

Ideal.comap (algebraMap R S) (LocalRing.maximalIdeal S) = I

source

theorem IsLocalization.AtPrime.isUnit_mk'_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : Ideal.IsPrime I] [IsLocalization.AtPrime S I] (x : R) (y : { x // x ∈ Ideal.primeCompl I }) :

IsUnit (IsLocalization.mk' S x y) ↔ x ∈ Ideal.primeCompl I

source

theorem IsLocalization.AtPrime.mk'_mem_maximal_iff {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I : Ideal R) [hI : Ideal.IsPrime I] [IsLocalization.AtPrime S I] (x : R) (y : { x // x ∈ Ideal.primeCompl I }) (h : optParam (LocalRing S) (_ : LocalRing S)) :

IsLocalization.mk' S x y ∈ LocalRing.maximalIdeal S ↔ x ∈ I

source

theorem Localization.AtPrime.comap_maximalIdeal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : Ideal.IsPrime I] :

Ideal.comap (algebraMap R (Localization.AtPrime I)) (LocalRing.maximalIdeal (Localization (Ideal.primeCompl I))) = I

The unique maximal ideal of the localization at I.primeCompl lies over the ideal I.

source

theorem Localization.AtPrime.map_eq_maximalIdeal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : Ideal.IsPrime I] :

Ideal.map (algebraMap R (Localization.AtPrime I)) I = LocalRing.maximalIdeal (Localization (Ideal.primeCompl I))

The image of I in the localization at I.primeCompl is a maximal ideal, and in particular it is the unique maximal ideal given by the local ring structure AtPrime.localRing

source

theorem Localization.le_comap_primeCompl_iff {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] {I : Ideal R} [hI : Ideal.IsPrime I] {J : Ideal P} [hJ : Ideal.IsPrime J] {f : R →+* P} :

Ideal.primeCompl I ≤ Submonoid.comap f (Ideal.primeCompl J) ↔ Ideal.comap f J ≤ I

source

noncomputable def Localization.localRingHom {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : Ideal.IsPrime I] (J : Ideal P) [Ideal.IsPrime J] (f : R →+* P) (hIJ : I = Ideal.comap f J) :

Localization.AtPrime I →+* Localization.AtPrime J

For a ring hom f : R →+* S and a prime ideal J in S, the induced ring hom from the localization of R at J.comap f to the localization of S at J.

To make this definition more flexible, we allow any ideal I of R as input, together with a proof that I = J.comap f. This can be useful when I is not definitionally equal to J.comap f.

Equations

Localization.localRingHom I J f hIJ = IsLocalization.map (Localization.AtPrime J) f (_ : Ideal.primeCompl I ≤ Submonoid.comap f (Ideal.primeCompl J))

Instances For

source

theorem Localization.localRingHom_to_map {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : Ideal.IsPrime I] (J : Ideal P) [Ideal.IsPrime J] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) :

↑(Localization.localRingHom I J f hIJ) (↑(algebraMap R (Localization.AtPrime I)) x) = ↑(algebraMap ((fun x => P) x) (Localization.AtPrime J)) (↑f x)

source

theorem Localization.localRingHom_mk' {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : Ideal.IsPrime I] (J : Ideal P) [Ideal.IsPrime J] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) (y : { x // x ∈ Ideal.primeCompl I }) :

↑(Localization.localRingHom I J f hIJ) (IsLocalization.mk' (Localization.AtPrime I) x y) = IsLocalization.mk' (Localization.AtPrime J) (↑f x) { val := ↑f ↑y, property := (_ : ↑y ∈ Submonoid.comap f (Ideal.primeCompl J)) }

source

instance Localization.isLocalRingHom_localRingHom {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : Ideal.IsPrime I] (J : Ideal P) [hJ : Ideal.IsPrime J] (f : R →+* P) (hIJ : I = Ideal.comap f J) :

IsLocalRingHom (Localization.localRingHom I J f hIJ)

Equations

@Localization.isLocalRingHom_localRingHom = @Localization.isLocalRingHom_localRingHom.proof_1

source

theorem Localization.localRingHom_unique {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : Ideal.IsPrime I] (J : Ideal P) [Ideal.IsPrime J] (f : R →+* P) (hIJ : I = Ideal.comap f J) {j : Localization.AtPrime I →+* Localization.AtPrime J} (hj : ∀ (x : R), ↑j (↑(algebraMap R (Localization.AtPrime I)) x) = ↑(algebraMap ((fun x => P) x) (Localization.AtPrime J)) (↑f x)) :

Localization.localRingHom I J f hIJ = j

source

@[simp]

theorem Localization.localRingHom_id {R : Type u_1} [CommSemiring R] (I : Ideal R) [hI : Ideal.IsPrime I] :

Localization.localRingHom I I (RingHom.id R) (_ : I = Ideal.comap (RingHom.id R) I) = RingHom.id (Localization.AtPrime I)

source

theorem Localization.localRingHom_comp {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (I : Ideal R) [hI : Ideal.IsPrime I] {S : Type u_4} [CommSemiring S] (J : Ideal S) [hJ : Ideal.IsPrime J] (K : Ideal P) [hK : Ideal.IsPrime K] (f : R →+* S) (hIJ : I = Ideal.comap f J) (g : S →+* P) (hJK : J = Ideal.comap g K) :

Localization.localRingHom I K (RingHom.comp g f) (_ : I = Ideal.comap (RingHom.comp g f) K) = RingHom.comp (Localization.localRingHom J K g hJK) (Localization.localRingHom I J f hIJ)