Relaxing from UFDs to Euclidean domains

Stream: maths

[Yaël Dillies]

I just read the TODOs in ring_theory.euclidean_domain:

-- this should be proved for UFDs surely?
theorem is_coprime_of_dvd {α} [euclidean_domain α] {x y : α}
  (z : ¬ (x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬ z ∣ y) :
  is_coprime x y :=
begin
  rw [← gcd_is_unit_iff],
  by_contra h,
  refine H _ h _ (gcd_dvd_left _ _) (gcd_dvd_right _ _),
  rwa [ne, euclidean_domain.gcd_eq_zero_iff]
end

-- this should be proved for UFDs surely?
theorem dvd_or_coprime {α} [euclidean_domain α] (x y : α)
  (h : irreducible x) : x ∣ y ∨ is_coprime x y :=
begin
  refine or_iff_not_imp_left.2 (λ h', _),
  apply is_coprime_of_dvd,
  { unfreezingI { rintro ⟨rfl, rfl⟩ }, simpa using h },
  { unfreezingI { rintro z nu nz ⟨w, rfl⟩ dy },
    refine h' (dvd_trans _ dy),
    simpa using mul_dvd_mul_left z (is_unit_iff_dvd_one.1 $
      (of_irreducible_mul h).resolve_left nu) }
end

Am I right in thinking that multivariate polynomials over anything reasonable form a UFD? Then the following note in ring_theory.coprime shows that the two above theorems are wrong if we relax euclidean_domain to unique_factorization_domain, right?
```` /-- The proposition that x and y are coprime, defined to be the existence of a and b such that a * x + b * y = 1. Note that elements with no common divisors are not necessarily coprime, e.g., the multivariate polynomials x₁ and x₂` are not coprime. -/
@[simp] def is_coprime : Prop :=
∃ a b, a * x + b * y = 1

[Kevin Buzzard]

Looks like there are two competing definitions of coprime here. I would argue that in real world mathematics, coprime for elements means the weaker thing (no common factors) and coprime for ideals means the stronger thing (sum is 1), so you can get coprime elements which do not generate coprime ideals. Looks like mathlib has a different convention?

[Yaël Dillies]

Yep, that's what I think too. Whoever wrote that TODO had the weaker notion of coprimality in mind.

[Kevin Buzzard]

I was guessing that your (currently ill-formatted) quoted def of is_coprime was coming from mathlib? I'm guessing that the "weaker notion" is what people would usually call coprime in practice.

[Yaël Dillies]

(I don't know what's wrong with my formatting btw... seems like Zulip is confused with the docstring)

[Kevin Buzzard]

On second thoughts, I am not sure that I would call two elements of the ring of integers of a number field coprime if they had no common factors but together generated, say, a non-principal prime ideal (so e.g. 1+sqrt(-5) and 2 in Z[sqrt(-5)]). Maybe the word is not used for general rings? For UFDs I wouldn't think twice about using the word to mean the weaker notion though, so X and Y are coprime in C[X,Y].

[Yaël Dillies]

Do we even have the weaker notion as a definition in mathlib? Maybe both are useful on their own rights.

[Mario Carneiro]

the issue with your formatting is a space before the `````