Lean4
/-- Let `t := g ^ d / f ^ e`, then `A_{(fg)} = A_{(f)}[1/t]`. -/
theorem isLocalization_mul (hd : d ≠ 0) :
letI := (awayMap 𝒜 hg hx).toAlgebra
IsLocalization.Away (isLocalizationElem hf hg) (Away 𝒜 x) :=
by
letI := (awayMap 𝒜 hg hx).toAlgebra
constructor
· rintro ⟨r, n, rfl⟩
rw [map_pow, RingHom.algebraMap_toAlgebra]
let z : Away 𝒜 x :=
Away.mk 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) (d + e) (g ^ e * f ^ (2 * e + d)) <|
by
convert SetLike.mul_mem_graded (SetLike.pow_mem_graded e hg) (SetLike.pow_mem_graded (2 * e + d) hf) using 2
ring
refine (isUnit_iff_exists_inv.mpr ⟨z, ?_⟩).pow _
ext
simp only [val_mul, val_one, awayMap_mk, Away.val_mk, z, Localization.mk_mul]
rw [← Localization.mk_one, Localization.mk_eq_mk_iff, Localization.r_iff_exists]
use 1
simp only [OneMemClass.coe_one, one_mul, Submonoid.coe_mul, mul_one, hx]
ring
· intro z
obtain ⟨n, s, hs, rfl⟩ := Away.mk_surjective 𝒜 (hx ▸ SetLike.mul_mem_graded hf hg) z
rcases d with - | d
· contradiction
let t : Away 𝒜 f :=
Away.mk 𝒜 hf (n * (e + 1)) (s * g ^ (n * d)) <| by
convert SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg) using 2; simp; ring
refine ⟨⟨t, ⟨_, ⟨n, rfl⟩⟩⟩, ?_⟩
ext
simp only [RingHom.algebraMap_toAlgebra, map_pow, awayMap_mk, val_mul, val_mk, val_pow, Localization.mk_pow,
Localization.mk_mul, t]
rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
exact ⟨1, by simp; ring⟩
· intro a b e
obtain ⟨n, a, ha, rfl⟩ := Away.mk_surjective 𝒜 hf a
obtain ⟨m, b, hb, rfl⟩ := Away.mk_surjective 𝒜 hf b
replace e := congr_arg val e
simp only [RingHom.algebraMap_toAlgebra, awayMap_mk, val_mk, Localization.mk_eq_mk_iff,
Localization.r_iff_exists] at e
obtain ⟨⟨_, k, rfl⟩, hc⟩ := e
refine ⟨⟨_, k + m + n, rfl⟩, ?_⟩
ext
simp only [val_mul, val_pow, val_mk, Localization.mk_pow, Localization.mk_eq_mk_iff, Localization.r_iff_exists,
Submonoid.coe_mul, Localization.mk_mul, SubmonoidClass.coe_pow, Subtype.exists, exists_prop]
refine ⟨_, ⟨k, rfl⟩, ?_⟩
rcases d with - | d
· contradiction
subst hx
convert congr(f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * $hc) using 1 <;> ring
