unique factorization

Stream: general

[Paul van Wamelen]

In lean-3.19.0 we had

theorem associates.eq_of_prod_eq_prod : ∀ {α : Type u_1} [_inst_1 : integral_domain α] [_inst_2 : unique_factorization_domain α]
{a b : associates.factor_set α}, a.prod = b.prod → a = b

but now we have:

theorem associates.eq_of_prod_eq_prod : ∀ {α : Type u_1} [_inst_1 : comm_cancel_monoid_with_zero α] [_inst_2 : unique_factorization_monoid α]
[_inst_3 : nontrivial α] [_inst_4 : normalization_monoid α] {a b : associates.factor_set α},
  a.prod = b.prod → a = b

This seems a lot weaker because of that normalization_monoid requirement. Should this be fixed?

[Aaron Anderson]

The only thing that the entire factor_set section is used for in thhe entirety of mathlib is establishing the gcd_monoid instance, which needs normalization_monoid anyway.

[Paul van Wamelen]

Thanks Aaron! I wanted to show that in a PID the ideal generated by x and y is the ideal generated by gcd x y. I was thinking of stating this as follows:

theorem span_gcd (x y : R) :
  associates.mk (submodule.is_principal.generator (ideal.span ({x, y} : set R)))
  = (associates.mk x) ⊓ (associates.mk y) :=
begin

But ⊓ now requires normalization monoid. Any suggestions on how to proceed?

[Aaron Anderson]

If you want to prove that statement, then I can see how you want a versatile associates.factor_set.

[Aaron Anderson]

(deleted)

[Aaron Anderson]

associates always has a normalization_monoid instance, so you should probably be able to refactor factor_set to just use that

[Aaron Anderson]

In the meantime, I don't think the name of your theorem matches its statement.

[Aaron Anderson]

Wouldn't you just want

theorem span_gcd (x y : R) :
  ideal.span ({x, y} : set R)
  = ideal.span( gcd_monoid.gcd x y) :=
begin

?

[Paul van Wamelen]

Technically not every PID is a gcd_monoid. Is refactoring gcd_monoid to not require normalization, and only have all of the equations be true up to associated, still an option? I wouldn't mind giving that a go...