Localizations of commutative rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We characterize the localization of a commutative ring R at a submonoid M up to
isomorphism; that is, a commutative ring S is the localization of R at M iff we can find a
ring homomorphism f : R →+* S satisfying 3 properties:
- For all
y ∈ M,f yis a unit; - For all
z : S, there exists(x, y) : R × Msuch thatz * f y = f x; - For all
x, y : R,f x = f yiff there existsc ∈ Msuch thatx * c = y * c.
In the following, let R, P be commutative rings, S, Q be R- and P-algebras
and M, T be submonoids of R and P respectively, e.g.:
variables (R S P Q : Type*) [comm_ring R] [comm_ring S] [comm_ring P] [comm_ring Q]
variables [algebra R S] [algebra P Q] (M : submonoid R) (T : submonoid P)
Main definitions #
is_localization (M : submonoid R) (S : Type*)is a typeclass expressing thatSis a localization ofRatM, i.e. the canonical mapalgebra_map R S : R →+* Sis a localization map (satisfying the above properties).is_localization.mk' Sis a surjection sending(x, y) : R × Mtof x * (f y)⁻¹is_localization.liftis the ring homomorphism fromSinduced by a homomorphism fromRwhich maps elements ofMto invertible elements of the codomain.is_localization.map S Qis the ring homomorphism fromStoQwhich maps elements ofMto elements ofTis_localization.ring_equiv_of_ring_equiv: ifRandPare isomorphic by an isomorphism sendingMtoT, thenSandQare isomorphicis_localization.alg_equiv: ifQis another localization ofRatM, thenSandQare isomorphic asR-algebras
Main results #
localization M S, a construction of the localization as a quotient type, defined ingroup_theory.monoid_localization, hascomm_ring,algebra Randis_localization Minstances ifRis a ring.localization.away,localization.at_primeandfraction_ringare abbreviations forlocalizations and have their correspondingis_localizationinstances
Implementation notes #
In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally rewrite one
structure with an isomorphic one; one way around this is to isolate a predicate characterizing
a structure up to isomorphism, and reason about things that satisfy the predicate.
A previous version of this file used a fully bundled type of ring localization maps,
then used a type synonym f.codomain for f : localization_map M S to instantiate the
R-algebra structure on S. This results in defining ad-hoc copies for everything already
defined on S. By making is_localization a predicate on the algebra_map R S,
we can ensure the localization map commutes nicely with other algebra_maps.
To prove most lemmas about a localization map algebra_map R S in this file we invoke the
corresponding proof for the underlying comm_monoid localization map
is_localization.to_localization_map M S, which can be found in group_theory.monoid_localization
and the namespace submonoid.localization_map.
To reason about the localization as a quotient type, use mk_eq_of_mk' and associated lemmas.
These show the quotient map mk : R → M → localization M equals the surjection
localization_map.mk' induced by the map algebra_map : R →+* localization M.
The lemma mk_eq_of_mk' hence gives you access to the results in the rest of the file,
which are about the localization_map.mk' induced by any localization map.
The proof that "a comm_ring K which is the localization of an integral domain R at R \ {0}
is a field" is a def rather than an instance, so if you want to reason about a field of
fractions K, assume [field K] instead of just [comm_ring K].
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
@[class]
structure
is_localization
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S] :
Prop
- map_units : ∀ (y : ↥M), is_unit (⇑(algebra_map R S) ↑y)
- surj : ∀ (z : S), ∃ (x : R × ↥M), z * ⇑(algebra_map R S) ↑(x.snd) = ⇑(algebra_map R S) x.fst
- eq_iff_exists : ∀ {x y : R}, ⇑(algebra_map R S) x = ⇑(algebra_map R S) y ↔ ∃ (c : ↥M), ↑c * x = ↑c * y
The typeclass is_localization (M : submodule R) S where S is an R-algebra
expresses that S is isomorphic to the localization of R at M.
Instances of this typeclass
theorem
is_localization.of_le
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(N : submonoid R)
(h₁ : M ≤ N)
(h₂ : ∀ (r : R), r ∈ N → is_unit (⇑(algebra_map R S) r)) :
is_localization N S
def
is_localization.to_localization_with_zero_map
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S] :
is_localization.to_localization_with_zero_map M S shows S is the monoid localization of
R at M.
Equations
- is_localization.to_localization_with_zero_map M S = {to_localization_map := {to_monoid_hom := {to_fun := ⇑(algebra_map R S), map_one' := _, map_mul' := _}, map_units' := _, surj' := _, eq_iff_exists' := _}, map_zero' := _}
@[simp]
theorem
is_localization.to_localization_with_zero_map_to_localization_map_to_monoid_hom_apply
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(ᾰ : R) :
@[reducible]
def
is_localization.to_localization_map
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S] :
M.localization_map S
is_localization.to_localization_map M S shows S is the monoid localization of R at M.
@[simp]
theorem
is_localization.to_localization_map_to_map
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S] :
(is_localization.to_localization_map M S).to_map = ↑↑(algebra_map R S)
theorem
is_localization.to_localization_map_to_map_apply
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R) :
⇑((is_localization.to_localization_map M S).to_map) x = ⇑(algebra_map R S) x
noncomputable
def
is_localization.sec
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(z : S) :
Given a localization map f : M →* N, a section function sending z : N to some
(x, y) : M × S such that f x * (f y)⁻¹ = z.
Equations
@[simp]
theorem
is_localization.to_localization_map_sec
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S] :
theorem
is_localization.sec_spec
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(z : S) :
z * ⇑(algebra_map R S) ↑((is_localization.sec M z).snd) = ⇑(algebra_map R S) (is_localization.sec M z).fst
Given z : S, is_localization.sec M z is defined to be a pair (x, y) : R × M such
that z * f y = f x (so this lemma is true by definition).
theorem
is_localization.sec_spec'
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(z : S) :
⇑(algebra_map R S) (is_localization.sec M z).fst = ⇑(algebra_map R S) ↑((is_localization.sec M z).snd) * z
Given z : S, is_localization.sec M z is defined to be a pair (x, y) : R × M such
that z * f y = f x, so this lemma is just an application of S's commutativity.
theorem
is_localization.map_right_cancel
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x y : R}
{c : ↥M}
(h : ⇑(algebra_map R S) (↑c * x) = ⇑(algebra_map R S) (↑c * y)) :
⇑(algebra_map R S) x = ⇑(algebra_map R S) y
theorem
is_localization.map_left_cancel
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x y : R}
{c : ↥M}
(h : ⇑(algebra_map R S) (x * ↑c) = ⇑(algebra_map R S) (y * ↑c)) :
⇑(algebra_map R S) x = ⇑(algebra_map R S) y
theorem
is_localization.eq_zero_of_fst_eq_zero
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{z : S}
{x : R}
{y : ↥M}
(h : z * ⇑(algebra_map R S) ↑y = ⇑(algebra_map R S) x)
(hx : x = 0) :
z = 0
theorem
is_localization.map_eq_zero_iff
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(r : R) :
noncomputable
def
is_localization.mk'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
S
is_localization.mk' S is the surjection sending (x, y) : R × M to
f x * (f y)⁻¹.
Equations
- is_localization.mk' S x y = (is_localization.to_localization_map M S).mk' x y
@[simp]
theorem
is_localization.mk'_sec
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(z : S) :
is_localization.mk' S (is_localization.sec M z).fst (is_localization.sec M z).snd = z
theorem
is_localization.mk'_mul
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x₁ x₂ : R)
(y₁ y₂ : ↥M) :
is_localization.mk' S (x₁ * x₂) (y₁ * y₂) = is_localization.mk' S x₁ y₁ * is_localization.mk' S x₂ y₂
theorem
is_localization.mk'_one
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R) :
is_localization.mk' S x 1 = ⇑(algebra_map R S) x
@[simp]
theorem
is_localization.mk'_spec
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
is_localization.mk' S x y * ⇑(algebra_map R S) ↑y = ⇑(algebra_map R S) x
@[simp]
theorem
is_localization.mk'_spec'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
⇑(algebra_map R S) ↑y * is_localization.mk' S x y = ⇑(algebra_map R S) x
@[simp]
theorem
is_localization.mk'_spec_mk
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x y : R)
(hy : y ∈ M) :
is_localization.mk' S x ⟨y, hy⟩ * ⇑(algebra_map R S) y = ⇑(algebra_map R S) x
@[simp]
theorem
is_localization.mk'_spec'_mk
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x y : R)
(hy : y ∈ M) :
⇑(algebra_map R S) y * is_localization.mk' S x ⟨y, hy⟩ = ⇑(algebra_map R S) x
theorem
is_localization.eq_mk'_iff_mul_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x : R}
{y : ↥M}
{z : S} :
z = is_localization.mk' S x y ↔ z * ⇑(algebra_map R S) ↑y = ⇑(algebra_map R S) x
theorem
is_localization.mk'_eq_iff_eq_mul
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x : R}
{y : ↥M}
{z : S} :
is_localization.mk' S x y = z ↔ ⇑(algebra_map R S) x = z * ⇑(algebra_map R S) ↑y
theorem
is_localization.mk'_add_eq_iff_add_mul_eq_mul
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x : R}
{y : ↥M}
{z₁ z₂ : S} :
is_localization.mk' S x y + z₁ = z₂ ↔ ⇑(algebra_map R S) x + z₁ * ⇑(algebra_map R S) ↑y = z₂ * ⇑(algebra_map R S) ↑y
theorem
is_localization.mk'_surjective
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(z : S) :
∃ (x : R) (y : ↥M), is_localization.mk' S x y = z
noncomputable
def
is_localization.fintype'
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
[fintype R] :
fintype S
The localization of a fintype is a fintype. Cannot be an instance.
Equations
- is_localization.fintype' M S = have this : Π (a : Prop), decidable a, from classical.prop_decidable, fintype.of_surjective (function.uncurry (is_localization.mk' S)) _
def
is_localization.unique_of_zero_mem
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(h : 0 ∈ M) :
unique S
Localizing at a submonoid with 0 inside it leads to the trivial ring.
Equations
theorem
is_localization.mk'_eq_iff_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x₁ x₂ : R}
{y₁ y₂ : ↥M} :
is_localization.mk' S x₁ y₁ = is_localization.mk' S x₂ y₂ ↔ ⇑(algebra_map R S) (↑y₂ * x₁) = ⇑(algebra_map R S) (↑y₁ * x₂)
theorem
is_localization.mk'_eq_iff_eq'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x₁ x₂ : R}
{y₁ y₂ : ↥M} :
is_localization.mk' S x₁ y₁ = is_localization.mk' S x₂ y₂ ↔ ⇑(algebra_map R S) (x₁ * ↑y₂) = ⇑(algebra_map R S) (x₂ * ↑y₁)
theorem
is_localization.mk'_mem_iff
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x : R}
{y : ↥M}
{I : ideal S} :
is_localization.mk' S x y ∈ I ↔ ⇑(algebra_map R S) x ∈ I
@[protected]
theorem
is_localization.eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{a₁ b₁ : R}
{a₂ b₂ : ↥M} :
theorem
is_localization.mk'_eq_zero_iff
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(s : ↥M) :
@[simp]
theorem
is_localization.mk'_zero
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(s : ↥M) :
is_localization.mk' S 0 s = 0
theorem
is_localization.ne_zero_of_mk'_ne_zero
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x : R}
{y : ↥M}
(hxy : is_localization.mk' S x y ≠ 0) :
x ≠ 0
theorem
is_localization.eq_iff_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
[algebra R P]
[is_localization M P]
{x y : R} :
⇑(algebra_map R S) x = ⇑(algebra_map R S) y ↔ ⇑(algebra_map R P) x = ⇑(algebra_map R P) y
theorem
is_localization.mk'_eq_iff_mk'_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
[algebra R P]
[is_localization M P]
{x₁ x₂ : R}
{y₁ y₂ : ↥M} :
is_localization.mk' S x₁ y₁ = is_localization.mk' S x₂ y₂ ↔ is_localization.mk' P x₁ y₁ = is_localization.mk' P x₂ y₂
theorem
is_localization.mk'_eq_of_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{a₁ b₁ : R}
{a₂ b₂ : ↥M}
(H : ↑a₂ * b₁ = ↑b₂ * a₁) :
is_localization.mk' S a₁ a₂ = is_localization.mk' S b₁ b₂
theorem
is_localization.mk'_eq_of_eq'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{a₁ b₁ : R}
{a₂ b₂ : ↥M}
(H : b₁ * ↑a₂ = a₁ * ↑b₂) :
is_localization.mk' S a₁ a₂ = is_localization.mk' S b₁ b₂
@[simp]
theorem
is_localization.mk'_self
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x : R}
(hx : x ∈ M) :
is_localization.mk' S x ⟨x, hx⟩ = 1
@[simp]
theorem
is_localization.mk'_self'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x : ↥M} :
is_localization.mk' S ↑x x = 1
theorem
is_localization.mk'_self''
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
{x : ↥M} :
is_localization.mk' S x.val x = 1
theorem
is_localization.mul_mk'_eq_mk'_of_mul
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x y : R)
(z : ↥M) :
⇑(algebra_map R S) x * is_localization.mk' S y z = is_localization.mk' S (x * y) z
theorem
is_localization.mk'_eq_mul_mk'_one
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
is_localization.mk' S x y = ⇑(algebra_map R S) x * is_localization.mk' S 1 y
@[simp]
theorem
is_localization.mk'_mul_cancel_left
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
is_localization.mk' S (↑y * x) y = ⇑(algebra_map R S) x
theorem
is_localization.mk'_mul_cancel_right
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
is_localization.mk' S (x * ↑y) y = ⇑(algebra_map R S) x
@[simp]
theorem
is_localization.mk'_mul_mk'_eq_one
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x y : ↥M) :
is_localization.mk' S ↑x y * is_localization.mk' S ↑y x = 1
theorem
is_localization.mk'_mul_mk'_eq_one'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M)
(h : x ∈ M) :
is_localization.mk' S x y * is_localization.mk' S ↑y ⟨x, h⟩ = 1
theorem
is_localization.is_unit_comp
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
(j : S →+* P)
(y : ↥M) :
is_unit (⇑(j.comp (algebra_map R S)) ↑y)
theorem
is_localization.eq_of_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y))
{x y : R}
(h : ⇑(algebra_map R S) x = ⇑(algebra_map R S) y) :
Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of comm_semirings
g : R →+* P such that g(M) ⊆ units P, f x = f y → g x = g y for all x y : R.
theorem
is_localization.mk'_add
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x₁ x₂ : R)
(y₁ y₂ : ↥M) :
is_localization.mk' S (x₁ * ↑y₂ + x₂ * ↑y₁) (y₁ * y₂) = is_localization.mk' S x₁ y₁ + is_localization.mk' S x₂ y₂
theorem
is_localization.mul_add_inv_left
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{P : Type u_3}
[comm_semiring P]
{g : R →+* P}
(h : ∀ (y : ↥M), is_unit (⇑g ↑y))
(y : ↥M)
(w z₁ z₂ : P) :
theorem
is_localization.lift_spec_mul_add
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y))
(z : S)
(w w' v : P) :
noncomputable
def
is_localization.lift
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y)) :
S →+* P
Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of comm_semirings
g : R →+* P such that g y is invertible for all y : M, the homomorphism induced from
S to P sending z : S to g x * (g y)⁻¹, where (x, y) : R × M are such that
z = f x * (f y)⁻¹.
Equations
- is_localization.lift hg = {to_fun := ((is_localization.to_localization_with_zero_map M S).lift g.to_monoid_with_zero_hom hg).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
theorem
is_localization.lift_mk'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y))
(x : R)
(y : ↥M) :
⇑(is_localization.lift hg) (is_localization.mk' S x y) = ⇑g x * ↑(⇑(is_unit.lift_right (g.to_monoid_hom.restrict M) hg) y)⁻¹
Given a localization map f : R →+* S for a submonoid M ⊆ R and a map of comm_semirings
g : R →* P such that g y is invertible for all y : M, the homomorphism induced from
S to P maps f x * (f y)⁻¹ to g x * (g y)⁻¹ for all x : R, y ∈ M.
theorem
is_localization.lift_mk'_spec
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y))
(x : R)
(v : P)
(y : ↥M) :
⇑(is_localization.lift hg) (is_localization.mk' S x y) = v ↔ ⇑g x = ⇑g ↑y * v
@[simp]
theorem
is_localization.lift_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y))
(x : R) :
⇑(is_localization.lift hg) (⇑(algebra_map R S) x) = ⇑g x
theorem
is_localization.lift_eq_iff
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y))
{x y : R × ↥M} :
@[simp]
theorem
is_localization.lift_comp
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y)) :
(is_localization.lift hg).comp (algebra_map R S) = g
@[simp]
theorem
is_localization.lift_of_comp
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
(j : S →+* P) :
theorem
is_localization.monoid_hom_ext
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
⦃j k : S →* P⦄
(h : j.comp ↑(algebra_map R S) = k.comp ↑(algebra_map R S)) :
j = k
theorem
is_localization.ring_hom_ext
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
⦃j k : S →+* P⦄
(h : j.comp (algebra_map R S) = k.comp (algebra_map R S)) :
j = k
theorem
is_localization.alg_hom_subsingleton
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
[algebra R P] :
subsingleton (S →ₐ[R] P)
@[protected]
theorem
is_localization.ext
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
(j k : S → P)
(hj1 : j 1 = 1)
(hk1 : k 1 = 1)
(hjm : ∀ (a b : S), j (a * b) = j a * j b)
(hkm : ∀ (a b : S), k (a * b) = k a * k b)
(h : ∀ (a : R), j (⇑(algebra_map R S) a) = k (⇑(algebra_map R S) a)) :
j = k
To show j and k agree on the whole localization, it suffices to show they agree
on the image of the base ring, if they preserve 1 and *.
theorem
is_localization.lift_unique
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y))
{j : S →+* P}
(hj : ∀ (x : R), ⇑j (⇑(algebra_map R S) x) = ⇑g x) :
is_localization.lift hg = j
@[simp]
theorem
is_localization.lift_id
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : S) :
⇑(is_localization.lift _) x = x
theorem
is_localization.lift_surjective_iff
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y)) :
theorem
is_localization.lift_injective_iff
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
(hg : ∀ (y : ↥M), is_unit (⇑g ↑y)) :
function.injective ⇑(is_localization.lift hg) ↔ ∀ (x y : R), ⇑(algebra_map R S) x = ⇑(algebra_map R S) y ↔ ⇑g x = ⇑g y
noncomputable
def
is_localization.map
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{T : submonoid P}
(Q : Type u_4)
[comm_semiring Q]
[algebra P Q]
[is_localization T Q]
(g : R →+* P)
(hy : M ≤ submonoid.comap g T) :
S →+* Q
Map a homomorphism g : R →+* P to S →+* Q, where S and Q are
localizations of R and P at M and T respectively,
such that g(M) ⊆ T.
We send z : S to algebra_map P Q (g x) * (algebra_map P Q (g y))⁻¹, where
(x, y) : R × M are such that z = f x * (f y)⁻¹.
Equations
- is_localization.map Q g hy = is_localization.lift _
theorem
is_localization.map_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
(hy : M ≤ submonoid.comap g T)
[algebra P Q]
[is_localization T Q]
(x : R) :
⇑(is_localization.map Q g hy) (⇑(algebra_map R S) x) = ⇑(algebra_map P Q) (⇑g x)
@[simp]
theorem
is_localization.map_comp
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
(hy : M ≤ submonoid.comap g T)
[algebra P Q]
[is_localization T Q] :
(is_localization.map Q g hy).comp (algebra_map R S) = (algebra_map P Q).comp g
theorem
is_localization.map_mk'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
(hy : M ≤ submonoid.comap g T)
[algebra P Q]
[is_localization T Q]
(x : R)
(y : ↥M) :
⇑(is_localization.map Q g hy) (is_localization.mk' S x y) = is_localization.mk' Q (⇑g x) ⟨⇑g ↑y, _⟩
@[simp]
theorem
is_localization.map_id
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(z : S)
(h : M ≤ submonoid.comap (ring_hom.id R) M := _) :
⇑(is_localization.map S (ring_hom.id R) h) z = z
theorem
is_localization.map_unique
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
(hy : M ≤ submonoid.comap g T)
[algebra P Q]
[is_localization T Q]
(j : S →+* Q)
(hj : ∀ (x : R), ⇑j (⇑(algebra_map R S) x) = ⇑(algebra_map P Q) (⇑g x)) :
is_localization.map Q g hy = j
theorem
is_localization.map_comp_map
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
(hy : M ≤ submonoid.comap g T)
[algebra P Q]
[is_localization T Q]
{A : Type u_5}
[comm_semiring A]
{U : submonoid A}
{W : Type u_6}
[comm_semiring W]
[algebra A W]
[is_localization U W]
{l : P →+* A}
(hl : T ≤ submonoid.comap l U) :
(is_localization.map W l hl).comp (is_localization.map Q g hy) = is_localization.map W (l.comp g) _
If comm_semiring homs g : R →+* P, l : P →+* A induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by l ∘ g.
theorem
is_localization.map_map
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
(hy : M ≤ submonoid.comap g T)
[algebra P Q]
[is_localization T Q]
{A : Type u_5}
[comm_semiring A]
{U : submonoid A}
{W : Type u_6}
[comm_semiring W]
[algebra A W]
[is_localization U W]
{l : P →+* A}
(hl : T ≤ submonoid.comap l U)
(x : S) :
⇑(is_localization.map W l hl) (⇑(is_localization.map Q g hy) x) = ⇑(is_localization.map W (l.comp g) _) x
If comm_semiring homs g : R →+* P, l : P →+* A induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by l ∘ g.
theorem
is_localization.map_smul
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{g : R →+* P}
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
(hy : M ≤ submonoid.comap g T)
[algebra P Q]
[is_localization T Q]
(x : S)
(z : R) :
⇑(is_localization.map Q g hy) (z • x) = ⇑g z • ⇑(is_localization.map Q g hy) x
@[simp]
theorem
is_localization.ring_equiv_of_ring_equiv_apply
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{T : submonoid P}
(Q : Type u_4)
[comm_semiring Q]
[algebra P Q]
[is_localization T Q]
(h : R ≃+* P)
(H : submonoid.map h.to_monoid_hom M = T)
(ᾰ : S) :
⇑(is_localization.ring_equiv_of_ring_equiv S Q h H) ᾰ = ⇑(is_localization.map Q ↑h _) ᾰ
@[simp]
theorem
is_localization.ring_equiv_of_ring_equiv_symm_apply
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{T : submonoid P}
(Q : Type u_4)
[comm_semiring Q]
[algebra P Q]
[is_localization T Q]
(h : R ≃+* P)
(H : submonoid.map h.to_monoid_hom M = T)
(ᾰ : Q) :
⇑((is_localization.ring_equiv_of_ring_equiv S Q h H).symm) ᾰ = ⇑(is_localization.map S ↑(h.symm) _) ᾰ
noncomputable
def
is_localization.ring_equiv_of_ring_equiv
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(S : Type u_2)
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{T : submonoid P}
(Q : Type u_4)
[comm_semiring Q]
[algebra P Q]
[is_localization T Q]
(h : R ≃+* P)
(H : submonoid.map h.to_monoid_hom M = T) :
S ≃+* Q
If S, Q are localizations of R and P at submonoids M, T respectively, an
isomorphism j : R ≃+* P such that j(M) = T induces an isomorphism of localizations
S ≃+* Q.
Equations
- is_localization.ring_equiv_of_ring_equiv S Q h H = have H' : submonoid.map h.symm.to_monoid_hom T = M, from _, {to_fun := ⇑(is_localization.map Q ↑h _), inv_fun := ⇑(is_localization.map S ↑(h.symm) _), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
theorem
is_localization.ring_equiv_of_ring_equiv_eq_map
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
[algebra P Q]
[is_localization T Q]
{j : R ≃+* P}
(H : submonoid.map j.to_monoid_hom M = T) :
↑(is_localization.ring_equiv_of_ring_equiv S Q j H) = is_localization.map Q ↑j _
@[simp]
theorem
is_localization.ring_equiv_of_ring_equiv_eq
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
[algebra P Q]
[is_localization T Q]
{j : R ≃+* P}
(H : submonoid.map j.to_monoid_hom M = T)
(x : R) :
⇑(is_localization.ring_equiv_of_ring_equiv S Q j H) (⇑(algebra_map R S) x) = ⇑(algebra_map P Q) (⇑j x)
theorem
is_localization.ring_equiv_of_ring_equiv_mk'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
{T : submonoid P}
{Q : Type u_4}
[comm_semiring Q]
[algebra P Q]
[is_localization T Q]
{j : R ≃+* P}
(H : submonoid.map j.to_monoid_hom M = T)
(x : R)
(y : ↥M) :
⇑(is_localization.ring_equiv_of_ring_equiv S Q j H) (is_localization.mk' S x y) = is_localization.mk' Q (⇑j x) ⟨⇑j ↑y, _⟩
noncomputable
def
is_localization.alg_equiv
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(Q : Type u_4)
[comm_semiring Q]
[algebra R Q]
[is_localization M Q] :
If S, Q are localizations of R at the submonoid M respectively,
there is an isomorphism of localizations S ≃ₐ[R] Q.
Equations
- is_localization.alg_equiv M S Q = {to_fun := (is_localization.ring_equiv_of_ring_equiv S Q (ring_equiv.refl R) _).to_fun, inv_fun := (is_localization.ring_equiv_of_ring_equiv S Q (ring_equiv.refl R) _).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
is_localization.alg_equiv_apply
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(Q : Type u_4)
[comm_semiring Q]
[algebra R Q]
[is_localization M Q]
(ᾰ : S) :
⇑(is_localization.alg_equiv M S Q) ᾰ = (is_localization.ring_equiv_of_ring_equiv S Q (ring_equiv.refl R) _).to_fun ᾰ
@[simp]
theorem
is_localization.alg_equiv_symm_apply
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(Q : Type u_4)
[comm_semiring Q]
[algebra R Q]
[is_localization M Q]
(ᾰ : Q) :
⇑((is_localization.alg_equiv M S Q).symm) ᾰ = (is_localization.ring_equiv_of_ring_equiv S Q (ring_equiv.refl R) _).inv_fun ᾰ
@[simp]
theorem
is_localization.alg_equiv_mk'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{Q : Type u_4}
[comm_semiring Q]
[algebra R Q]
[is_localization M Q]
(x : R)
(y : ↥M) :
⇑(is_localization.alg_equiv M S Q) (is_localization.mk' S x y) = is_localization.mk' Q x y
@[simp]
theorem
is_localization.alg_equiv_symm_mk'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
{Q : Type u_4}
[comm_semiring Q]
[algebra R Q]
[is_localization M Q]
(x : R)
(y : ↥M) :
⇑((is_localization.alg_equiv M S Q).symm) (is_localization.mk' Q x y) = is_localization.mk' S x y
theorem
is_localization.is_localization_of_alg_equiv
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[algebra R P]
[is_localization M S]
(h : S ≃ₐ[R] P) :
is_localization M P
theorem
is_localization.is_localization_iff_of_alg_equiv
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[algebra R P]
(h : S ≃ₐ[R] P) :
is_localization M S ↔ is_localization M P
theorem
is_localization.is_localization_iff_of_ring_equiv
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
{S : Type u_2}
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
(h : S ≃+* P) :
is_localization M S ↔ is_localization M P
theorem
is_localization.is_localization_of_base_ring_equiv
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
[is_localization M S]
(h : R ≃+* P) :
theorem
is_localization.is_localization_iff_of_base_ring_equiv
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
{P : Type u_3}
[comm_semiring P]
(h : R ≃+* P) :
is_localization M S ↔ is_localization (submonoid.map h.to_monoid_hom M) S
theorem
is_localization.non_zero_divisors_le_comap
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S] :
non_zero_divisors R ≤ submonoid.comap (algebra_map R S) (non_zero_divisors S)
theorem
is_localization.map_non_zero_divisors_le
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S] :
submonoid.map (algebra_map R S) (non_zero_divisors R) ≤ non_zero_divisors S
Constructing a localization at a given submonoid #
@[protected, instance]
def
localization.unique
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
[subsingleton R] :
unique (localization M)
Equations
- localization.unique = {to_inhabited := {default := 1}, uniq := _}
@[protected, irreducible]
Addition in a ring localization is defined as ⟨a, b⟩ + ⟨c, d⟩ = ⟨b * c + d * a, b * d⟩.
Should not be confused with add_localization.add, which is defined as
⟨a, b⟩ + ⟨c, d⟩ = ⟨a + c, b + d⟩.
@[protected, instance]
def
localization.has_add
{R : Type u_1}
[comm_semiring R]
{M : submonoid R} :
has_add (localization M)
Equations
theorem
localization.add_mk
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(a : R)
(b : ↥M)
(c : R)
(d : ↥M) :
localization.mk a b + localization.mk c d = localization.mk (↑b * c + ↑d * a) (b * d)
theorem
localization.add_mk_self
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(a : R)
(b : ↥M)
(c : R) :
localization.mk a b + localization.mk c b = localization.mk (a + c) b
@[protected, instance]
Equations
- localization.comm_semiring = {add := has_add.add localization.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul localization.has_smul, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul (localization.has_mul M), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast._default 1 has_add.add localization.comm_semiring._proof_15 0 localization.comm_semiring._proof_16 localization.comm_semiring._proof_17 has_smul.smul localization.comm_semiring._proof_18 localization.comm_semiring._proof_19, nat_cast_zero := _, nat_cast_succ := _, npow := localization.npow M, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[simp]
theorem
localization.mk_add_monoid_hom_apply
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(b : ↥M)
(a : R) :
⇑(localization.mk_add_monoid_hom b) a = localization.mk a b
def
localization.mk_add_monoid_hom
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(b : ↥M) :
R →+ localization M
For any given denominator b : M, the map a ↦ a / b is an add_monoid_hom from R to
localization M
Equations
- localization.mk_add_monoid_hom b = {to_fun := λ (a : R), localization.mk a b, map_zero' := _, map_add' := _}
theorem
localization.mk_sum
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{ι : Type u_2}
(f : ι → R)
(s : finset ι)
(b : ↥M) :
localization.mk (s.sum (λ (i : ι), f i)) b = s.sum (λ (i : ι), localization.mk (f i) b)
theorem
localization.mk_list_sum
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(l : list R)
(b : ↥M) :
localization.mk l.sum b = (list.map (λ (a : R), localization.mk a b) l).sum
theorem
localization.mk_multiset_sum
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(l : multiset R)
(b : ↥M) :
localization.mk l.sum b = (multiset.map (λ (a : R), localization.mk a b) l).sum
@[protected, instance]
def
localization.distrib_mul_action
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[monoid S]
[distrib_mul_action S R]
[is_scalar_tower S R R] :
Equations
- localization.distrib_mul_action = {to_mul_action := localization.mul_action _inst_7, smul_zero := _, smul_add := _}
@[protected, instance]
def
localization.mul_semiring_action
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[semiring S]
[mul_semiring_action S R]
[is_scalar_tower S R R] :
Equations
- localization.mul_semiring_action = {to_distrib_mul_action := localization.distrib_mul_action _inst_7, smul_one := _, smul_mul := _}
@[protected, instance]
def
localization.module
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[semiring S]
[module S R]
[is_scalar_tower S R R] :
module S (localization M)
Equations
- localization.module = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action localization.distrib_mul_action, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
@[protected, instance]
def
localization.algebra
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra S R] :
algebra S (localization M)
Equations
- localization.algebra = {to_has_smul := localization.has_smul localization.algebra._proof_1, to_ring_hom := {to_fun := ⇑((localization.monoid_of M).to_map), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}.comp (algebra_map S R), commutes' := _, smul_def' := _}
@[protected, instance]
def
localization.is_localization
{R : Type u_1}
[comm_semiring R]
{M : submonoid R} :
is_localization M (localization M)
@[simp]
theorem
localization.to_localization_map_eq_monoid_of
{R : Type u_1}
[comm_semiring R]
{M : submonoid R} :
theorem
localization.monoid_of_eq_algebra_map
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(x : R) :
⇑((localization.monoid_of M).to_map) x = ⇑(algebra_map R (localization M)) x
theorem
localization.mk_one_eq_algebra_map
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(x : R) :
localization.mk x 1 = ⇑(algebra_map R (localization M)) x
theorem
localization.mk_eq_mk'_apply
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(x : R)
(y : ↥M) :
localization.mk x y = is_localization.mk' (localization M) x y
@[simp]
theorem
localization.mk_algebra_map
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{A : Type u_2}
[comm_semiring A]
[algebra A R]
(m : A) :
localization.mk (⇑(algebra_map A R) m) 1 = ⇑(algebra_map A (localization M)) m
theorem
localization.mk_nat_cast
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
(m : ℕ) :
localization.mk ↑m 1 = ↑m
noncomputable
def
localization.alg_equiv
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S] :
localization M ≃ₐ[R] S
The localization of R at M as a quotient type is isomorphic to any other localization.
Equations
- localization.alg_equiv M S = is_localization.alg_equiv M (localization M) S
@[simp]
theorem
localization.alg_equiv_symm_apply
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(ᾰ : S) :
⇑((localization.alg_equiv M S).symm) ᾰ = ⇑(is_localization.map (localization M) ↑((ring_equiv.refl R).symm) _) ᾰ
@[simp]
theorem
localization.alg_equiv_apply
{R : Type u_1}
[comm_semiring R]
(M : submonoid R)
(S : Type u_2)
[comm_semiring S]
[algebra R S]
[is_localization M S]
(ᾰ : localization M) :
⇑(localization.alg_equiv M S) ᾰ = ⇑(is_localization.map S ↑(ring_equiv.refl R) _) ᾰ
noncomputable
def
is_localization.unique
(R : Type u_1)
(Rₘ : Type u_2)
[comm_semiring R]
[comm_semiring Rₘ]
(M : submonoid R)
[subsingleton R]
[algebra R Rₘ]
[is_localization M Rₘ] :
unique Rₘ
The localization of a singleton is a singleton. Cannot be an instance due to metavariables.
@[simp]
theorem
localization.alg_equiv_mk'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
⇑(localization.alg_equiv M S) (is_localization.mk' (localization M) x y) = is_localization.mk' S x y
@[simp]
theorem
localization.alg_equiv_symm_mk'
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
⇑((localization.alg_equiv M S).symm) (is_localization.mk' S x y) = is_localization.mk' (localization M) x y
theorem
localization.alg_equiv_mk
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
⇑(localization.alg_equiv M S) (localization.mk x y) = is_localization.mk' S x y
theorem
localization.alg_equiv_symm_mk
{R : Type u_1}
[comm_semiring R]
{M : submonoid R}
{S : Type u_2}
[comm_semiring S]
[algebra R S]
[is_localization M S]
(x : R)
(y : ↥M) :
⇑((localization.alg_equiv M S).symm) (is_localization.mk' S x y) = localization.mk x y
@[protected, irreducible]
Negation in a ring localization is defined as -⟨a, b⟩ = ⟨-a, b⟩.
@[protected, instance]
Equations
theorem
localization.neg_mk
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(a : R)
(b : ↥M) :
-localization.mk a b = localization.mk (-a) b
@[protected, instance]
Equations
- localization.comm_ring = {add := comm_semiring.add localization.comm_semiring, add_assoc := _, zero := comm_semiring.zero localization.comm_semiring, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul localization.comm_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg localization.has_neg, sub := λ (x y : localization M), x + -y, sub_eq_add_neg := _, zsmul := has_smul.smul localization.has_smul, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast._default comm_semiring.nat_cast comm_semiring.add localization.comm_ring._proof_13 comm_semiring.zero localization.comm_ring._proof_14 localization.comm_ring._proof_15 comm_semiring.nsmul localization.comm_ring._proof_16 localization.comm_ring._proof_17 comm_semiring.one localization.comm_ring._proof_18 localization.comm_ring._proof_19 has_neg.neg (λ (x y : localization M), x + -y) localization.comm_ring._proof_20 has_smul.smul localization.comm_ring._proof_21 localization.comm_ring._proof_22 localization.comm_ring._proof_23 localization.comm_ring._proof_24, nat_cast := comm_semiring.nat_cast localization.comm_semiring, one := comm_semiring.one localization.comm_semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_semiring.mul localization.comm_semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_semiring.npow localization.comm_semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
theorem
localization.sub_mk
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(a c : R)
(b d : ↥M) :
localization.mk a b - localization.mk c d = localization.mk (↑d * a - ↑b * c) (b * d)
theorem
localization.mk_int_cast
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(m : ℤ) :
localization.mk ↑m 1 = ↑m
theorem
is_localization.to_map_eq_zero_iff
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(S : Type u_2)
[comm_ring S]
[algebra R S]
[is_localization M S]
{x : R}
(hM : M ≤ non_zero_divisors R) :
⇑(algebra_map R S) x = 0 ↔ x = 0
@[protected]
theorem
is_localization.injective
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(S : Type u_2)
[comm_ring S]
[algebra R S]
[is_localization M S]
(hM : M ≤ non_zero_divisors R) :
@[protected]
theorem
is_localization.to_map_ne_zero_of_mem_non_zero_divisors
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(S : Type u_2)
[comm_ring S]
[algebra R S]
[is_localization M S]
[nontrivial R]
(hM : M ≤ non_zero_divisors R)
{x : R}
(hx : x ∈ non_zero_divisors R) :
⇑(algebra_map R S) x ≠ 0
theorem
is_localization.sec_snd_ne_zero
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
[nontrivial R]
(hM : M ≤ non_zero_divisors R)
(x : S) :
↑((is_localization.sec M x).snd) ≠ 0
theorem
is_localization.sec_fst_ne_zero
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
[nontrivial R]
[no_zero_divisors S]
(hM : M ≤ non_zero_divisors R)
{x : S}
(hx : x ≠ 0) :
(is_localization.sec M x).fst ≠ 0
theorem
is_localization.map_injective_of_injective
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
(S : Type u_2)
[comm_ring S]
[algebra R S]
{P : Type u_3}
[comm_ring P]
[is_localization M S]
(Q : Type u_5)
[comm_ring Q]
{g : R →+* P}
[algebra P Q]
(hg : function.injective ⇑g)
[is_localization (submonoid.map g M) Q] :
Injectivity of a map descends to the map induced on localizations.
@[reducible]
theorem
is_localization.no_zero_divisors_of_le_non_zero_divisors
{S : Type u_2}
[comm_ring S]
(A : Type u_6)
[comm_ring A]
[is_domain A]
[algebra A S]
{M : submonoid A}
[is_localization M S]
(hM : M ≤ non_zero_divisors A) :
A comm_ring S which is the localization of a ring R without zero divisors at a subset of
non-zero elements does not have zero divisors.
See note [reducible non-instances].
@[reducible]
theorem
is_localization.is_domain_of_le_non_zero_divisors
{S : Type u_2}
[comm_ring S]
(A : Type u_6)
[comm_ring A]
[is_domain A]
[algebra A S]
{M : submonoid A}
[is_localization M S]
(hM : M ≤ non_zero_divisors A) :
A comm_ring S which is the localization of an integral domain R at a subset of
non-zero elements is an integral domain.
See note [reducible non-instances].
@[reducible]
theorem
is_localization.is_domain_localization
{A : Type u_6}
[comm_ring A]
[is_domain A]
{M : submonoid A}
(hM : M ≤ non_zero_divisors A) :
The localization at of an integral domain to a set of non-zero elements is an integral domain. See note [reducible non-instances].
theorem
is_field.localization_map_bijective
{R : Type u_1}
{Rₘ : Type u_2}
[comm_ring R]
[comm_ring Rₘ]
{M : submonoid R}
(hM : 0 ∉ M)
(hR : is_field R)
[algebra R Rₘ]
[is_localization M Rₘ] :
function.bijective ⇑(algebra_map R Rₘ)
If R is a field, then localizing at a submonoid not containing 0 adds no new elements.
theorem
field.localization_map_bijective
{K : Type u_1}
{Kₘ : Type u_2}
[field K]
[comm_ring Kₘ]
{M : submonoid K}
(hM : 0 ∉ M)
[algebra K Kₘ]
[is_localization M Kₘ] :
function.bijective ⇑(algebra_map K Kₘ)
If R is a field, then localizing at a submonoid not containing 0 adds no new elements.
noncomputable
def
localization_algebra
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
(S : Type u_2)
[comm_ring S]
[algebra R S]
{Rₘ : Type u_4}
{Sₘ : Type u_5}
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ] :
algebra Rₘ Sₘ
Definition of the natural algebra induced by the localization of an algebra.
Given an algebra R → S, a submonoid R of M, and a localization Rₘ for M,
let Sₘ be the localization of S to the image of M under algebra_map R S.
Then this is the natural algebra structure on Rₘ → Sₘ, such that the entire square commutes,
where localization_map.map_comp gives the commutativity of the underlying maps.
This instance can be helpful if you define Sₘ := localization (algebra.algebra_map_submonoid S M),
however we will instead use the hypotheses [algebra Rₘ Sₘ] [is_scalar_tower R Rₘ Sₘ] in lemmas
since the algebra structure may arise in different ways.
Equations
- localization_algebra M S = (is_localization.map Sₘ (algebra_map R S) _).to_algebra
theorem
is_localization.map_units_map_submonoid
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(S : Type u_2)
[comm_ring S]
[algebra R S]
(Sₘ : Type u_5)
[comm_ring Sₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ]
[algebra R Sₘ]
[is_scalar_tower R S Sₘ]
(y : ↥M) :
is_unit (⇑(algebra_map R Sₘ) ↑y)
@[simp]
theorem
is_localization.algebra_map_mk'
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(S : Type u_2)
[comm_ring S]
[algebra R S]
(Rₘ : Type u_4)
(Sₘ : Type u_5)
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ]
[algebra Rₘ Sₘ]
[algebra R Sₘ]
[is_scalar_tower R Rₘ Sₘ]
[is_scalar_tower R S Sₘ]
(x : R)
(y : ↥M) :
⇑(algebra_map Rₘ Sₘ) (is_localization.mk' Rₘ x y) = is_localization.mk' Sₘ (⇑(algebra_map R S) x) ⟨⇑(algebra_map R S) ↑y, _⟩
theorem
is_localization.algebra_map_eq_map_map_submonoid
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
(S : Type u_2)
[comm_ring S]
[algebra R S]
(Rₘ : Type u_4)
(Sₘ : Type u_5)
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ]
[algebra Rₘ Sₘ]
[algebra R Sₘ]
[is_scalar_tower R Rₘ Sₘ]
[is_scalar_tower R S Sₘ] :
algebra_map Rₘ Sₘ = is_localization.map Sₘ (algebra_map R S) _
If the square below commutes, the bottom map is uniquely specified:
R → S
↓ ↓
Rₘ → Sₘ
theorem
is_localization.algebra_map_apply_eq_map_map_submonoid
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
(S : Type u_2)
[comm_ring S]
[algebra R S]
(Rₘ : Type u_4)
(Sₘ : Type u_5)
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ]
[algebra Rₘ Sₘ]
[algebra R Sₘ]
[is_scalar_tower R Rₘ Sₘ]
[is_scalar_tower R S Sₘ]
(x : Rₘ) :
⇑(algebra_map Rₘ Sₘ) x = ⇑(is_localization.map Sₘ (algebra_map R S) _) x
If the square below commutes, the bottom map is uniquely specified:
R → S
↓ ↓
Rₘ → Sₘ
theorem
is_localization.lift_algebra_map_eq_algebra_map
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
(S : Type u_2)
[comm_ring S]
[algebra R S]
(Rₘ : Type u_4)
(Sₘ : Type u_5)
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ]
[algebra Rₘ Sₘ]
[algebra R Sₘ]
[is_scalar_tower R Rₘ Sₘ]
[is_scalar_tower R S Sₘ] :
is_localization.lift _ = algebra_map Rₘ Sₘ
theorem
localization_algebra_injective
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
{S : Type u_2}
[comm_ring S]
[algebra R S]
(Rₘ : Type u_4)
(Sₘ : Type u_5)
[comm_ring Rₘ]
[comm_ring Sₘ]
[algebra R Rₘ]
[is_localization M Rₘ]
[algebra S Sₘ]
[is_localization (algebra.algebra_map_submonoid S M) Sₘ]
(hRS : function.injective ⇑(algebra_map R S)) :
function.injective ⇑(algebra_map Rₘ Sₘ)
Injectivity of the underlying algebra_map descends to the algebra induced by localization.