English
Under a property respecting isomorphisms, comparing a localization away and a pullback via IsLocalization.Away.map yields equivalent truth values of P.
Русский
При свойстве, сохраняющем изоморфизмы, сопоставление локализации Away.map и IsLocalization.Away.map дает равные значения истиности P.
LaTeX
$$$P(\text{ Localization.awayMap } f r) \iff P( \text{ IsLocalization.Away.map } R' S' f r).$$$
Lean4
theorem isLocalization_away_iff (hP : RingHom.RespectsIso @P) {R S : Type u} (R' S' : Type u) [CommRing R] [CommRing S]
[CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] (f : R →+* S) (r : R) [IsLocalization.Away r R']
[IsLocalization.Away (f r) S'] : P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r) :=
by
let e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) _ _).toRingEquiv
let e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) _ _).toRingEquiv
refine (hP.cancel_left_isIso e₁.toCommRingCatIso.hom (CommRingCat.ofHom _)).symm.trans ?_
refine (hP.cancel_right_isIso (CommRingCat.ofHom _) e₂.toCommRingCatIso.hom).symm.trans ?_
rw [← eq_iff_iff]
congr 1
-- Porting note: Here, the proof used to have a huge `simp` involving `[anonymous]`, which didn't
-- work out anymore. The issue seemed to be that it couldn't handle a term in which Ring
-- homomorphisms were repeatedly casted to the bundled category and back. Here we resolve the
-- problem by converting the goal to a more straightforward form.
let e :=
(e₂ : Localization.Away (f r) →+* S').comp
(((IsLocalization.map (Localization.Away (f r)) f
(by rintro x ⟨n, rfl⟩; use n; simp : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r)))) :
Localization.Away r →+* Localization.Away (f r)).comp
(e₁ : R' →+* Localization.Away r))
suffices e = IsLocalization.Away.map R' S' f r by convert this
apply IsLocalization.ringHom_ext (Submonoid.powers r) _
ext1 x
dsimp [e, e₁, e₂, IsLocalization.Away.map]
simp only [IsLocalization.map_eq, id_apply, RingHomCompTriple.comp_apply]
