Localizations of commutative rings at the complement of a prime ideal #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
is_localization.at_prime (I : ideal R) [is_prime I] (S : Type*)expresses thatSis a localization at (the complement of) a prime idealI, as an abbreviation ofis_localization I.prime_compl S
Main results #
is_localization.at_prime.local_ring: a theorem (not an instance) stating a localization at the complement of a prime ideal is a local ring
Implementation notes #
See src/ring_theory/localization/basic.lean for a design overview.
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
The complement of a prime ideal I ⊆ R is a submonoid of R.
Instances for ideal.prime_compl
- is_localization.localization_localization_at_prime_is_localization
- valuation_subring.of_prime_localization
- algebraic_geometry.structure_sheaf.as_ideal.is_localization.at_prime
- algebraic_geometry.structure_sheaf.is_localization.to_stalk
- algebraic_geometry.structure_sheaf.is_localized_module_to_pushforward_stalk_alg_hom
theorem
ideal.prime_compl_le_non_zero_divisors
{R : Type u_1}
[comm_semiring R]
(I : ideal R)
[hp : I.is_prime]
[no_zero_divisors R] :
@[protected, reducible]
def
is_localization.at_prime
{R : Type u_1}
[comm_semiring R]
(S : Type u_2)
[comm_semiring S]
[algebra R S]
(I : ideal R)
[hp : I.is_prime] :
Prop
Given a prime ideal P, the typeclass is_localization.at_prime S P states that S is
isomorphic to the localization of R at the complement of P.
@[protected, reducible]
def
localization.at_prime
{R : Type u_1}
[comm_semiring R]
(I : ideal R)
[hp : I.is_prime] :
Type u_1
Given a prime ideal P, localization.at_prime S P is a localization of
R at the complement of P, as a quotient type.
theorem
is_localization.at_prime.nontrivial
{R : Type u_1}
[comm_semiring R]
(S : Type u_2)
[comm_semiring S]
[algebra R S]
(I : ideal R)
[hp : I.is_prime]
[is_localization.at_prime S I] :
theorem
is_localization.at_prime.local_ring
{R : Type u_1}
[comm_semiring R]
(S : Type u_2)
[comm_semiring S]
[algebra R S]
(I : ideal R)
[hp : I.is_prime]
[is_localization.at_prime S I] :
@[protected, instance]
def
localization.at_prime.local_ring
{R : Type u_1}
[comm_semiring R]
(I : ideal R)
[hp : I.is_prime] :
The localization of R at the complement of a prime ideal is a local ring.
theorem
is_localization.at_prime.is_unit_to_map_iff
{R : Type u_1}
[comm_semiring R]
(S : Type u_2)
[comm_semiring S]
[algebra R S]
(I : ideal R)
[hI : I.is_prime]
[is_localization.at_prime S I]
(x : R) :
is_unit (⇑(algebra_map R S) x) ↔ x ∈ I.prime_compl
theorem
is_localization.at_prime.to_map_mem_maximal_iff
{R : Type u_1}
[comm_semiring R]
(S : Type u_2)
[comm_semiring S]
[algebra R S]
(I : ideal R)
[hI : I.is_prime]
[is_localization.at_prime S I]
(x : R)
(h : local_ring S := _) :
⇑(algebra_map R S) x ∈ local_ring.maximal_ideal S ↔ x ∈ I
theorem
is_localization.at_prime.comap_maximal_ideal
{R : Type u_1}
[comm_semiring R]
(S : Type u_2)
[comm_semiring S]
[algebra R S]
(I : ideal R)
[hI : I.is_prime]
[is_localization.at_prime S I]
(h : local_ring S := _) :
ideal.comap (algebra_map R S) (local_ring.maximal_ideal S) = I
theorem
is_localization.at_prime.is_unit_mk'_iff
{R : Type u_1}
[comm_semiring R]
(S : Type u_2)
[comm_semiring S]
[algebra R S]
(I : ideal R)
[hI : I.is_prime]
[is_localization.at_prime S I]
(x : R)
(y : ↥(I.prime_compl)) :
is_unit (is_localization.mk' S x y) ↔ x ∈ I.prime_compl
theorem
is_localization.at_prime.mk'_mem_maximal_iff
{R : Type u_1}
[comm_semiring R]
(S : Type u_2)
[comm_semiring S]
[algebra R S]
(I : ideal R)
[hI : I.is_prime]
[is_localization.at_prime S I]
(x : R)
(y : ↥(I.prime_compl))
(h : local_ring S := _) :
is_localization.mk' S x y ∈ local_ring.maximal_ideal S ↔ x ∈ I
theorem
localization.at_prime.comap_maximal_ideal
{R : Type u_1}
[comm_semiring R]
{I : ideal R}
[hI : I.is_prime] :
The unique maximal ideal of the localization at I.prime_compl lies over the ideal I.
theorem
localization.at_prime.map_eq_maximal_ideal
{R : Type u_1}
[comm_semiring R]
{I : ideal R}
[hI : I.is_prime] :
The image of I in the localization at I.prime_compl is a maximal ideal, and in particular
it is the unique maximal ideal given by the local ring structure at_prime.local_ring
theorem
localization.le_comap_prime_compl_iff
{R : Type u_1}
[comm_semiring R]
{P : Type u_3}
[comm_semiring P]
{I : ideal R}
[hI : I.is_prime]
{J : ideal P}
[hJ : J.is_prime]
{f : R →+* P} :
I.prime_compl ≤ submonoid.comap f J.prime_compl ↔ ideal.comap f J ≤ I
noncomputable
def
localization.local_ring_hom
{R : Type u_1}
[comm_semiring R]
{P : Type u_3}
[comm_semiring P]
(I : ideal R)
[hI : I.is_prime]
(J : ideal P)
[hJ : J.is_prime]
(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.local_ring_hom I J f hIJ = is_localization.map (localization.at_prime J) f _
Instances for localization.local_ring_hom
theorem
localization.local_ring_hom_to_map
{R : Type u_1}
[comm_semiring R]
{P : Type u_3}
[comm_semiring P]
(I : ideal R)
[hI : I.is_prime]
(J : ideal P)
[hJ : J.is_prime]
(f : R →+* P)
(hIJ : I = ideal.comap f J)
(x : R) :
⇑(localization.local_ring_hom I J f hIJ) (⇑(algebra_map R (localization.at_prime I)) x) = ⇑(algebra_map P (localization.at_prime J)) (⇑f x)
theorem
localization.local_ring_hom_mk'
{R : Type u_1}
[comm_semiring R]
{P : Type u_3}
[comm_semiring P]
(I : ideal R)
[hI : I.is_prime]
(J : ideal P)
[hJ : J.is_prime]
(f : R →+* P)
(hIJ : I = ideal.comap f J)
(x : R)
(y : ↥(I.prime_compl)) :
⇑(localization.local_ring_hom I J f hIJ) (is_localization.mk' (localization.at_prime I) x y) = is_localization.mk' (localization.at_prime J) (⇑f x) ⟨⇑f ↑y, _⟩
@[protected, instance]
def
localization.is_local_ring_hom_local_ring_hom
{R : Type u_1}
[comm_semiring R]
{P : Type u_3}
[comm_semiring P]
(I : ideal R)
[hI : I.is_prime]
(J : ideal P)
[hJ : J.is_prime]
(f : R →+* P)
(hIJ : I = ideal.comap f J) :
is_local_ring_hom (localization.local_ring_hom I J f hIJ)
theorem
localization.local_ring_hom_unique
{R : Type u_1}
[comm_semiring R]
{P : Type u_3}
[comm_semiring P]
(I : ideal R)
[hI : I.is_prime]
(J : ideal P)
[hJ : J.is_prime]
(f : R →+* P)
(hIJ : I = ideal.comap f J)
{j : localization.at_prime I →+* localization.at_prime J}
(hj : ∀ (x : R), ⇑j (⇑(algebra_map R (localization.at_prime I)) x) = ⇑(algebra_map P (localization.at_prime J)) (⇑f x)) :
localization.local_ring_hom I J f hIJ = j
@[simp]
theorem
localization.local_ring_hom_id
{R : Type u_1}
[comm_semiring R]
(I : ideal R)
[hI : I.is_prime] :
localization.local_ring_hom I I (ring_hom.id R) _ = ring_hom.id (localization.at_prime I)
@[simp]
theorem
localization.local_ring_hom_comp
{R : Type u_1}
[comm_semiring R]
{P : Type u_3}
[comm_semiring P]
(I : ideal R)
[hI : I.is_prime]
{S : Type u_2}
[comm_semiring S]
(J : ideal S)
[hJ : J.is_prime]
(K : ideal P)
[hK : K.is_prime]
(f : R →+* S)
(hIJ : I = ideal.comap f J)
(g : S →+* P)
(hJK : J = ideal.comap g K) :
localization.local_ring_hom I K (g.comp f) _ = (localization.local_ring_hom J K g hJK).comp (localization.local_ring_hom I J f hIJ)