English
If R is a domain with UniqueFactorizationMonoid structure and irreducibles behave well under associates, then R has a unit-mul-power irreducible factorization compatible with DVR structure.
Русский
Если R имеет единично-однозначное разложение и ирредуцируемые соответствуют асоциированию, то R имеет факторизацию единица-множитель-степенной формы, согласованную с DVR.
LaTeX
$$$HasUnitMulPowIrreducibleFactorization R \;\Rightarrow\; UniqueFactorizationMonoid R$$$
Lean4
/-- An integral domain in which there is an irreducible element `p`
such that every nonzero element is associated to a power of `p` is a unique factorization domain.
See `IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization`. -/
theorem toUniqueFactorizationMonoid (hR : HasUnitMulPowIrreducibleFactorization R) : UniqueFactorizationMonoid R :=
let p := Classical.choose hR
let spec := Classical.choose_spec hR
UniqueFactorizationMonoid.of_exists_prime_factors fun x hx =>
by
use Multiset.replicate (Classical.choose (spec.2 hx)) p
constructor
· intro q hq
have hpq := Multiset.eq_of_mem_replicate hq
rw [hpq]
refine ⟨spec.1.ne_zero, spec.1.not_isUnit, ?_⟩
intro a b h
by_cases ha : a = 0
· rw [ha]
simp only [true_or, dvd_zero]
obtain ⟨m, u, rfl⟩ := spec.2 ha
rw [mul_assoc, mul_left_comm, Units.dvd_mul_left] at h
rw [Units.dvd_mul_right]
by_cases hm : m = 0
· simp only [hm, one_mul, pow_zero] at h ⊢
right
exact h
left
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
rw [pow_succ']
apply dvd_mul_of_dvd_left dvd_rfl _
· rw [Multiset.prod_replicate]
exact Classical.choose_spec (spec.2 hx)
