Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: add lemma exists_squarefree_dvd_pow_of_ne_zero #10241

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat: add lemma exists_squarefree_dvd_pow_of_ne_zero #10241

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
42e0176
feat: add lemma `exists_squarefree_dvd_pow_of_ne_zero`
ocfnash Feb 4, 2024
53f34b4
Feedback from CR
ocfnash Feb 5, 2024
ea1ee5e
Fix after CR changes
ocfnash Feb 5, 2024
14a9ce2
Strengthen lemma to add divisibility condition
ocfnash Feb 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
8 changes: 8 additions & 0 deletions Mathlib/Algebra/Associated.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -728,6 +728,14 @@ theorem Associated.of_pow_associated_of_prime' [CancelCommMonoidWithZero α] {p
(h.symm.of_pow_associated_of_prime hp₂ hp₁ hk₂).symm
#align associated.of_pow_associated_of_prime' Associated.of_pow_associated_of_prime'

/-- See also `Irreducible.coprime_iff_not_dvd`. -/
lemma Irreducible.coprime_iff_not_dvd' [Monoid α] {p n : α} (hp : Irreducible p) :
ocfnash marked this conversation as resolved.
Show resolved Hide resolved
(∀ d, d ∣ p → d ∣ n → IsUnit d) ↔ ¬ p ∣ n := by
refine ⟨fun h contra ↦ hp.not_unit (h p (refl _) contra), fun hpn d hdp hdn ↦ ?_⟩
contrapose! hpn
suffices Associated p d from this.dvd.trans hdn
exact (hp.dvd_iff.mp hdp).resolve_left hpn

section UniqueUnits

variable [Monoid α] [Unique αˣ]
Expand Down
14 changes: 14 additions & 0 deletions Mathlib/Algebra/Squarefree/UniqueFactorizationDomain.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,3 +94,17 @@ theorem squarefree_mul_iff :
rw [mul_mul_mul_comm] at contra; exact dvd_of_mul_right_dvd contra
exact ⟨hy.dvd_of_squarefree_of_mul_dvd_mul_left contra,
hx.dvd_of_squarefree_of_mul_dvd_mul_right contra⟩

lemma exists_squarefree_dvd_pow_of_ne_zero (hx : x ≠ 0) :
∃ (y : R) (n : ℕ), Squarefree y ∧ x ∣ y ^ n := by
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This can be strengthened to require that y divides x.

I started the DecompositionMonoid refactoring in that branch, and I think every lemma in this file can be generalized to DceompositionMonoid (and two only require CancelCommMonoidWithZero as you can see). However this new lemma can't be generalized, since (assuming DecompositionMonoid) it implies factorizability into squarefree elements, which is the subject of Proposition 3.4 in the paper. Note that DecompositionMonoid + factorizability into irreducibles would imply UFM right away.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This can be strengthened to require that y divides x.

Good point, I will add this.

I started the DecompositionMonoid refactoring in that branch ...

Great, thanks for taking this on. As an aside, I would argue that your proposed IsRelPrime should really get the label IsCoprime and what is currently called IsCoprime should either be dropped or renamed something like ExistsBezout or IsBezoutPair or something.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having Bezout in the name is nice; IsCoprime is equivalent to IsRelPrime in Bezout rings (IsBezout), and most results in Mathlib.RingTheory.PrincipalIdealDomain can be generalized to Bezout rings (but maybe the correct approach is to replace IsCoprime by IsRelPrime and use the equivalence when necessary ...). There is IsBezout.gcd but maybe it's better to allow a separate GCDMonoid instance and use that gcd so the lemmas won't just apply to the particular choice of gcd/generators.

Indeed most lemmas about IsRelPrime has coprime in their names instead. I think we have to use a new name (and IsRelPrime) is my choice, since IsCoprime is widely used and we'd like to deprecate it rather than renaming it right away. I won't rename the lemmas so that they have the right names when we later rename IsRelPrime back to IsCoprime. (But do we need to deprecate IsRelPrime then? Maybe it's better to rename IsCoprime right now ...)

I still think IsComaximal is a reasonable name, since IsCoprime x y is equivalent to the comaximality (currently with the unintuitive name Codisjoint) of the ideals they generate, and also to the comaximality of the basic opens in the spectrum.

induction' x using induction_on_prime with u hu z p hz hp ih
· contradiction
· exact ⟨1, 0, squarefree_one, hu.dvd⟩
· obtain ⟨y, n, hy, hy'⟩ := ih hz
rcases n.eq_zero_or_pos with rfl | hn
· exact ⟨p, 1, hp.squarefree, by simp [isUnit_of_dvd_one (pow_zero y ▸ hy')]⟩
by_cases hp' : p ∣ y
· exact ⟨y, n + 1, hy, mul_comm p z ▸ pow_succ' y n ▸ mul_dvd_mul hy' hp'⟩
· suffices Squarefree (p * y) by
exact ⟨p * y, n, this, mul_pow p y n ▸ mul_dvd_mul (dvd_pow_self p hn.ne') hy'⟩
exact squarefree_mul_iff.mpr ⟨hp.irreducible.coprime_iff_not_dvd'.mpr hp', hp.squarefree, hy⟩
1 change: 1 addition & 0 deletions Mathlib/RingTheory/PrincipalIdealDomain.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -447,6 +447,7 @@ theorem Prime.coprime_iff_not_dvd {p n : R} (pp : Prime p) : IsCoprime p n ↔
pp.irreducible.coprime_iff_not_dvd
#align prime.coprime_iff_not_dvd Prime.coprime_iff_not_dvd

/-- See also `Irreducible.coprime_iff_not_dvd'`. -/
theorem Irreducible.dvd_iff_not_coprime {p n : R} (hp : Irreducible p) : p ∣ n ↔ ¬IsCoprime p n :=
iff_not_comm.2 hp.coprime_iff_not_dvd
#align irreducible.dvd_iff_not_coprime Irreducible.dvd_iff_not_coprime
Expand Down