Localizations of commutative rings at the complement of a prime ideal #
Main definitions #
IsLocalization.AtPrime (P : Ideal R) [IsPrime P] (S : Type*)expresses thatSis a localization at (the complement of) a prime idealP, as an abbreviation ofIsLocalization P.prime_compl S
Main results #
IsLocalization.AtPrime.isLocalRing: 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
@[reducible, inline]
abbrev
IsLocalization.AtPrime
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
:
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
@[reducible, inline]
abbrev
Localization.AtPrime
{R : Type u_1}
[CommSemiring R]
(P : Ideal R)
[hp : P.IsPrime]
:
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
theorem
IsLocalization.AtPrime.Nontrivial
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
theorem
IsLocalization.AtPrime.isLocalRing
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
@[deprecated IsLocalization.AtPrime.isLocalRing (since := "2024-11-09")]
theorem
IsLocalization.AtPrime.localRing
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(P : Ideal R)
[hp : P.IsPrime]
[IsLocalization.AtPrime S P]
:
Alias of IsLocalization.AtPrime.isLocalRing.
instance
Localization.AtPrime.isLocalRing
{R : Type u_1}
[CommSemiring R]
(P : Ideal R)
[hp : P.IsPrime]
:
The localization of R at the complement of a prime ideal is a local ring.
def
IsLocalization.AtPrime.orderIsoOfPrime
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
:
The prime ideals in the localization of a commutative ring at a prime ideal I are in order-preserving bijection with the prime ideals contained in I.
Equations
- One or more equations did not get rendered due to their size.
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 : I.IsPrime]
[IsLocalization.AtPrime S I]
(x : R)
:
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 : I.IsPrime]
[IsLocalization.AtPrime S I]
(x : R)
(h : IsLocalRing S := ⋯)
:
theorem
IsLocalization.AtPrime.comap_maximalIdeal
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
[hI : I.IsPrime]
[IsLocalization.AtPrime S I]
(h : IsLocalRing S := ⋯)
:
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 : I.IsPrime]
[IsLocalization.AtPrime S I]
(x : R)
(y : ↥I.primeCompl)
:
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 : I.IsPrime]
[IsLocalization.AtPrime S I]
(x : R)
(y : ↥I.primeCompl)
(h : IsLocalRing S := ⋯)
:
theorem
Localization.AtPrime.comap_maximalIdeal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
:
Ideal.comap (algebraMap R (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization I.primeCompl)) = I
The unique maximal ideal of the localization at I.primeCompl lies over the ideal I.
theorem
Localization.AtPrime.map_eq_maximalIdeal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
:
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.isLocalRing
theorem
Localization.le_comap_primeCompl_iff
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
{I : Ideal R}
[hI : I.IsPrime]
{J : Ideal P}
[J.IsPrime]
{f : R →+* P}
:
noncomputable def
Localization.localRingHom
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f 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 ⋯
theorem
Localization.localRingHom_to_map
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
(x : R)
:
(localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)
theorem
Localization.localRingHom_mk'
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
(x : R)
(y : ↥I.primeCompl)
:
(localRingHom I J f hIJ) (IsLocalization.mk' (Localization.AtPrime I) x y) = IsLocalization.mk' (Localization.AtPrime J) (f x) ⟨f ↑y, ⋯⟩
instance
Localization.isLocalHom_localRingHom
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[hJ : J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
:
IsLocalHom (localRingHom I J f hIJ)
@[deprecated Localization.isLocalHom_localRingHom (since := "2024-10-10")]
theorem
Localization.isLocalRingHom_localRingHom
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[hJ : J.IsPrime]
(f : R →+* P)
(hIJ : I = Ideal.comap f J)
:
IsLocalHom (localRingHom I J f hIJ)
Alias of Localization.isLocalHom_localRingHom.
theorem
Localization.localRingHom_unique
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
(J : Ideal P)
[J.IsPrime]
(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 P (Localization.AtPrime J)) (f x))
:
@[simp]
theorem
Localization.localRingHom_id
{R : Type u_1}
[CommSemiring R]
(I : Ideal R)
[hI : I.IsPrime]
:
theorem
Localization.localRingHom_comp
{R : Type u_1}
[CommSemiring R]
{P : Type u_3}
[CommSemiring P]
(I : Ideal R)
[hI : I.IsPrime]
{S : Type u_4}
[CommSemiring S]
(J : Ideal S)
[hJ : J.IsPrime]
(K : Ideal P)
[hK : K.IsPrime]
(f : R →+* S)
(hIJ : I = Ideal.comap f J)
(g : S →+* P)
(hJK : J = Ideal.comap g K)
:
noncomputable instance
Localization.AtPrime.instAlgebraOfLiesOver
{A : Type u_4}
{B : Type u_5}
[CommRing A]
[CommRing B]
[Algebra A B]
(p : Ideal A)
[p.IsPrime]
(P : Ideal B)
[P.IsPrime]
[P.LiesOver p]
:
Equations
- Localization.AtPrime.instAlgebraOfLiesOver p P = (Localization.localRingHom p P (algebraMap A B) ⋯).toAlgebra
@[reducible, inline]
noncomputable abbrev
Localization.AtPrime.mapPiEvalRingHom
{ι : Type u_4}
{R : ι → Type u_5}
[(i : ι) → CommSemiring (R i)]
{i : ι}
(I : Ideal (R i))
[I.IsPrime]
:
Localization.localRingHom specialized to a projection homomorphism from a product ring.
Equations
- Localization.AtPrime.mapPiEvalRingHom I = Localization.localRingHom (Ideal.comap (Pi.evalRingHom R i) I) I (Pi.evalRingHom R i) ⋯
theorem
Localization.AtPrime.mapPiEvalRingHom_bijective
{ι : Type u_4}
{R : ι → Type u_5}
[(i : ι) → CommSemiring (R i)]
{i : ι}
(I : Ideal (R i))
[I.IsPrime]
:
theorem
Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap
{ι : Type u_4}
{R : ι → Type u_5}
[(i : ι) → CommSemiring (R i)]
{i : ι}
(I : Ideal (R i))
[I.IsPrime]
:
(mapPiEvalRingHom I).comp (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) = (algebraMap (R i) (Localization.AtPrime I)).comp (Pi.evalRingHom R i)
theorem
Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply
{ι : Type u_4}
{R : ι → Type u_5}
[(i : ι) → CommSemiring (R i)]
{i : ι}
(I : Ideal (R i))
[I.IsPrime]
{r : (i : ι) → R i}
:
(mapPiEvalRingHom I) ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) r) = (algebraMap (R i) (Localization.AtPrime I)) (r i)