English
The canonical map toBasicOpen is an injective ring homomorphism.
Русский
Канонический отображение toBasicOpen инъективно.
LaTeX
$$$toBasicOpen(R,f)$ is injective.$$
Lean4
theorem toBasicOpen_injective (f : R) : Function.Injective (toBasicOpen R f) :=
by
intro s t h_eq
obtain ⟨a, ⟨b, hb⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers f) s
obtain ⟨c, ⟨d, hd⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers f) t
simp only [toBasicOpen_mk'] at h_eq
rw [IsLocalization.eq]
-- We know that the fractions `a/b` and `c/d` are equal as sections of the structure sheaf on
-- `basicOpen f`. We need to show that they agree as elements in the localization of `R` at `f`.
-- This amounts showing that `r * (d * a) = r * (b * c)`, for some power `r = f ^ n` of `f`.
-- We define `I` as the ideal of *all* elements `r` satisfying the above equation.
let I : Ideal R :=
{ carrier := {r : R | r * (d * a) = r * (b * c)}
zero_mem' := by simp only [Set.mem_setOf_eq, zero_mul]
add_mem' := fun {r₁ r₂} hr₁ hr₂ => by dsimp at hr₁ hr₂ ⊢; simp only [add_mul, hr₁, hr₂]
smul_mem' := fun {r₁ r₂} hr₂ => by dsimp at hr₂ ⊢; simp only [mul_assoc, hr₂] }
-- Our claim now reduces to showing that `f` is contained in the radical of `I`
suffices f ∈ I.radical by
obtain ⟨n, hn⟩ := this
exact ⟨⟨f ^ n, n, rfl⟩, hn⟩
rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.mem_vanishingIdeal]
intro p hfp
contrapose hfp
rw [PrimeSpectrum.mem_zeroLocus, Set.not_subset]
have := congr_fun (congr_arg Subtype.val h_eq) ⟨p, hfp⟩
dsimp at this
rw [IsLocalization.eq (S := Localization.AtPrime p.asIdeal)] at this
obtain ⟨r, hr⟩ := this
exact
⟨r.1, hr, r.2⟩
/-
Auxiliary lemma for surjectivity of `toBasicOpen`.
Every section can locally be represented on basic opens `basicOpen g` as a fraction `f/g`
-/
