feat(RingTheory/UniqueFactorizationDomain): UFD iff height one primes are principal#36781
feat(RingTheory/UniqueFactorizationDomain): UFD iff height one primes are principal#36781hommmmm wants to merge 7 commits intoleanprover-community:masterfrom
Conversation
This is a new fork of mathlib 4 for PR on the factoriality criterion. Original edits were made in https://github.com/uw-math-ai/auslander-buchsbaum
Shorten proof significantly. Clean up comments. Refactor `ne_bot_of_height_one`.
Fix <= 1 and add attribution to doc string.
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
github-actions
bot
added
the
large-import
PR summary 316a0377d0Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky | 1113 | 1854 | +741 (+66.58%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RingTheory.PowerSeries.Ideal |
409 |
Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky |
741 |
Declarations diff
+ exists_height_one_le_of_finite_height
+ height_one_prime_principal
+ ne_bot_of_height_one
+ of_height_one_prime_principal
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
Note #36739 |
|
Welcome! Could you please clarify if and how you used AI for (parts of) this pull request? Note that our contribution guidelines require disclosure of any AI assistance. |
chrisflav
added
the
awaiting-author
Updated PR message with AI disclosure -awaiting-author |
github-actions
bot
removed
the
awaiting-author
6 participants
We prove that a Noetherian integral domain is a UFD if and only if every prime ideal of height one is principal (
UniqueFactorizationMonoid.iff_height_one_prime_principal).New declarations
UniqueFactorizationMonoid.exists_height_one_le_of_finite_height: given a prime of finite height ≥ 1, there exists a height one prime contained in it.UniqueFactorizationMonoid.ne_bot_of_height_one: an ideal of height one is nonzero.UniqueFactorizationMonoid.height_ge_one_of_prime_ne_bot: the height of a nonzero prime ideal in a domain is at least one.UniqueFactorizationMonoid.height_one_prime_principal: in a UFD, every height one prime is principal.UniqueFactorizationMonoid.of_height_one_prime_principal: every height one prime being principal implies UFD (Noetherian case).UniqueFactorizationMonoid.iff_height_one_prime_principal: the full iff statement.References
See https://stacks.math.columbia.edu/tag/0AFT
AI Disclosure
This code is written without AI, then uses Claude Code with cameronfreer's Lean4-skills (specifically, the
review,refactor, andgolfworkflow) for style changes, refactoring and golfing.