More lemmas on localization away #
This file contains lemmas on localization away from an element requiring more imports.
noncomputable def
IsLocalization.Away.mulNumerator
{R : Type u_1}
[CommRing R]
(s : Set R)
{Rₜ : ↑s → Type u_2}
[(t : ↑s) → CommRing (Rₜ t)]
[(t : ↑s) → Algebra R (Rₜ t)]
[∀ (t : ↑s), IsLocalization.Away (↑t) (Rₜ t)]
(p : (t : ↑s) → Set (Rₜ t))
(x : (t : ↑s) × ↑(p t))
:
R
Given a set s in a ring R and for every t : s a set p t of fractions in
a localization of R at t, this is the function sending a pair (t, y), with
t : s and y : t a, to t multiplied with a numerator of y. The range
of this function spans the unit ideal, if s and every p t do.
Equations
- IsLocalization.Away.mulNumerator s p x = ↑x.fst * (IsLocalization.Away.sec ↑x.fst ↑x.snd).1
Instances For
theorem
IsLocalization.Away.span_range_mulNumerator_eq_top
{R : Type u_1}
[CommRing R]
{s : Set R}
(hsone : Ideal.span s = ⊤)
{Rₜ : ↑s → Type u_2}
[(t : ↑s) → CommRing (Rₜ t)]
[(t : ↑s) → Algebra R (Rₜ t)]
[∀ (t : ↑s), IsLocalization.Away (↑t) (Rₜ t)]
{p : (t : ↑s) → Set (Rₜ t)}
(htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤)
:
theorem
IsLocalization.Away.quotient_of_isIdempotentElem
{R : Type u_1}
[CommRing R]
{e : R}
(he : IsIdempotentElem e)
:
IsLocalization.Away e (R ⧸ Ideal.span {1 - e})