English
If a property P respects isomorphisms, then for any f, Locally P f follows from P on a cover and the compatibility with isomorphisms.
Русский
Если свойство P сохраняет изоморфизмы, то локально свойство P для f следует из выполнения P на покрытии и совместимости с изоморфизмами.
LaTeX
$$$\text{Locally}(P,f)\Rightarrow \text{Locally}(Q,f)$ при $Q$ переносимо через изоморфизм; точнее: если $P$ хранит изоморфизмы, то $Locally P f \Rightarrow Locally Q f$.$$
Lean4
/-- If `P` respects isomorphisms, to check `P` holds locally for `f : R →+* S`, it suffices
to check `P` holds on a standard open cover. -/
theorem locally_of_exists (hP : RespectsIso P) (f : R →+* S) {ι : Type*} (s : ι → S)
(hsone : Ideal.span (Set.range s) = ⊤) (Sₜ : ι → Type u) [∀ i, CommRing (Sₜ i)] [∀ i, Algebra S (Sₜ i)]
[∀ i, IsLocalization.Away (s i) (Sₜ i)] (hf : ∀ i, P ((algebraMap S (Sₜ i)).comp f)) : Locally P f :=
by
use Set.range s, hsone
rintro - ⟨i, rfl⟩
let e : Localization.Away (s i) ≃+* Sₜ i := (IsLocalization.algEquiv (Submonoid.powers (s i)) _ _).toRingEquiv
have : algebraMap S (Localization.Away (s i)) = e.symm.toRingHom.comp (algebraMap S (Sₜ i)) :=
RingHom.ext (fun x ↦ (AlgEquiv.commutes (IsLocalization.algEquiv _ _ _).symm _).symm)
rw [this, RingHom.comp_assoc]
exact hP.left _ _ (hf i)
