English
If s is locally a fraction on U, then comapFun f U V hUV s is locally a fraction on V; the proof is by transferring the local data along comap.
Русский
Если s локально дробь на U, то comapFun f U V hUV s локально дробь на V; доказательство переносит локальные данные через comap.
LaTeX
$$∀ p, (isLocallyFraction R).pred s → (isLocallyFraction S).pred (comapFun f U V hUV s)$$
Lean4
theorem comapFunIsLocallyFraction (f : R →+* S) (U : Opens (PrimeSpectrum.Top R)) (V : Opens (PrimeSpectrum.Top S))
(hUV : V.1 ⊆ PrimeSpectrum.comap f ⁻¹' U.1) (s : ∀ x : U, Localizations R x)
(hs : (isLocallyFraction R).toPrelocalPredicate.pred s) :
(isLocallyFraction S).toPrelocalPredicate.pred (comapFun f U V hUV s) :=
by
rintro
⟨p, hpV⟩
-- Since `s` is locally fraction, we can find a neighborhood `W` of `PrimeSpectrum.comap f p`
-- in `U`, such that `s = a / b` on `W`, for some ring elements `a, b : R`.
rcases hs ⟨PrimeSpectrum.comap f p, hUV hpV⟩ with
⟨W, m, iWU, a, b, h_frac⟩
-- We claim that we can write our new section as the fraction `f a / f b` on the neighborhood
-- `(comap f) ⁻¹ W ⊓ V` of `p`.
refine ⟨Opens.comap (PrimeSpectrum.comap f) W ⊓ V, ⟨m, hpV⟩, Opens.infLERight _ _, f a, f b, ?_⟩
rintro ⟨q, ⟨hqW, hqV⟩⟩
specialize h_frac ⟨PrimeSpectrum.comap f q, hqW⟩
refine ⟨h_frac.1, ?_⟩
dsimp only [comapFun]
erw [← Localization.localRingHom_to_map (PrimeSpectrum.comap f q).asIdeal _ _ rfl, ← RingHom.map_mul, h_frac.2,
Localization.localRingHom_to_map]
rfl
