English
If P respects isomorphisms, then Locally P also respects isomorphisms.
Русский
Если P сохраняет изоморфизмы, то Locally P также сохраняет изоморфизмы.
LaTeX
$$$\operatorname{RespectsIso}(P) \Rightarrow \operatorname{RespectsIso}(\Locally P).$$$
Lean4
/-- If `P` respects isomorphism, so does `Locally P`. -/
theorem locally_respectsIso (hPi : RespectsIso P) : RespectsIso (Locally P)
where
left {R S T} _ _ _ f
e := fun ⟨s, hsone, hs⟩ ↦ by
refine ⟨e '' s, ?_, ?_⟩
· rw [← Ideal.map_span, hsone, Ideal.map_top]
· rintro - ⟨a, ha, rfl⟩
let e' : Localization.Away a ≃+* Localization.Away (e a) :=
IsLocalization.ringEquivOfRingEquiv _ _ e (Submonoid.map_powers e a)
have :
(algebraMap T (Localization.Away (e a))).comp e.toRingHom =
e'.toRingHom.comp (algebraMap S (Localization.Away a)) :=
by
ext x
simp [e']
rw [← RingHom.comp_assoc, this, RingHom.comp_assoc]
apply hPi.left
exact hs a ha
right {R S T} _ _ _ f
e := fun ⟨s, hsone, hs⟩ ↦ ⟨s, hsone, fun a ha ↦ (RingHom.comp_assoc _ _ _).symm ▸ hPi.right _ _ (hs a ha)⟩
