English
Under stronger assumptions including domain and divisor conditions, there exist a and n with properties expressing a reduced fraction representation of a given nonzero b in B.
Русский
При более сильных предположениях существование a и n дает представление b как дробь с сокращением.
LaTeX
$$$\exists a\in R,\exists n\in \mathbb{Z}, \neg x \nmid a \wedge selfZPow x B n \cdot algebraMap R B a = b$$$
Lean4
theorem exists_reduced_fraction' {b : B} (hb : b ≠ 0) (hx : Irreducible x) :
∃ (a : R) (n : ℤ), ¬x ∣ a ∧ selfZPow x B n * algebraMap R B a = b :=
by
obtain ⟨⟨a₀, y⟩, H⟩ := surj (Submonoid.powers x) b
obtain ⟨d, hy⟩ := (Submonoid.mem_powers_iff y.1 x).mp y.2
have ha₀ : a₀ ≠ 0 :=
by
haveI := isDomain_of_le_nonZeroDivisors B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
simp only [← hy, map_pow] at H
apply ((injective_iff_map_eq_zero' (algebraMap R B)).mp _ a₀).mpr.mt
· rw [← H]
apply mul_ne_zero hb (pow_ne_zero _ _)
exact
IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
(mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)
· exact IsLocalization.injective B (powers_le_nonZeroDivisors_of_noZeroDivisors hx.ne_zero)
simp only [← hy] at H
obtain ⟨m, a, hyp1, hyp2⟩ := WfDvdMonoid.max_power_factor ha₀ hx
refine ⟨a, m - d, ?_⟩
rw [← mk'_one (M := Submonoid.powers x) B, selfZPow_pow_sub, selfZPow_natCast, selfZPow_natCast, ← map_pow _ _ d,
mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m]
exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩
