English
In the prime-homogeneous localization, an element is a unit if and only if its val is a unit in the ambient ring.
Русский
В локализации по простому однородному случаю элемент является единицей тогда и только тогда, когда его значение является единицей в исходном кольце.
LaTeX
$$$$ \IsUnit( f ) \iff \IsUnit( f.\mathrm{val} ) $$$$
Lean4
theorem isUnit_iff_isUnit_val (f : HomogeneousLocalization.AtPrime 𝒜 𝔭) : IsUnit f.val ↔ IsUnit f :=
by
refine ⟨fun h1 ↦ ?_, IsUnit.map (algebraMap _ _)⟩
rcases h1 with ⟨⟨a, b, eq0, eq1⟩, rfl : a = f.val⟩
obtain ⟨f, rfl⟩ := mk_surjective f
obtain ⟨b, s, rfl⟩ := IsLocalization.mk'_surjective 𝔭.primeCompl b
rw [val_mk, Localization.mk_eq_mk', ← IsLocalization.mk'_mul, IsLocalization.mk'_eq_iff_eq_mul, one_mul,
IsLocalization.eq_iff_exists (M := 𝔭.primeCompl)] at eq0
obtain ⟨c, hc : _ = c.1 * (f.den.1 * s.1)⟩ := eq0
have : f.num.1 ∉ 𝔭 := by
exact fun h ↦ mul_mem c.2 (mul_mem f.den_mem s.2) (hc ▸ Ideal.mul_mem_left _ c.1 (Ideal.mul_mem_right b _ h))
refine isUnit_of_mul_eq_one _ (Quotient.mk'' ⟨f.1, f.3, f.2, this⟩) ?_
rw [← mk_mul, ext_iff_val, val_mk]
simp [mul_comm f.den.1]
