Commutative algebra
The Lean Pool projects whose card's first MSC2020 code is in class 13, Commutative algebra: 2 articles, one per card.
TheoremThe Anderson Conjecture: A Weakly Quasi-Complete Ring Need Not Be Quasi-Complete#
Formalizes a counterexample to Anderson's question, constructing a weakly quasi-complete Noetherian local ring that is not quasi-complete via the Jensen-Heitmann-Loepp transfinite construction.
Quoted from the card LeanPool/projects/anderson-conjecture.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
anderson_main_theorem(theorem; a main declaration), declared in LeanPool/AndersonConjecture/Main.lean, line 781: “Proves that there exists a weakly quasi-complete Noetherian local ring that is not quasi-complete.”
Project
- Authors: FrenzyMath.
- Source: doi:10.1007/978-1-4939-0925-4_2.
- Project repository: frenzymath/Anderson-Conjecture.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 13B35, 13H10.
- In Lean Pool: LeanPool/AndersonConjecture, from the card LeanPool/projects/anderson-conjecture.yaml.
Sources
TheoremNagata's prime-generated factoriality theorem#
Nagata’s factoriality criterion for noetherian domains localized at prime-generated multiplicative sets, with concrete and abstract localization interfaces and applications to polynomial rings through Laurent and fraction-field localizations.
Quoted from the card LeanPool/projects/nagatafactoriality.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
NagataFactoriality.nagata_theorem(theorem; a main declaration), declared in LeanPool/NagataFactoriality/NagataFactoriality/Nagata/Theorem.lean, line 21: “A noetherian integral domain is a unique factorization domain when localization at a prime-generated multiplicative set is a unique factorization domain.”
Project
- Authors: Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira.
- Project repository: arthur742ramos/nagatafactoriality, at commit 2efdf7f8.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”. The card's note: “Inferred from explicit Copilot coauthor trailers in the pinned upstream history: 83.5% of surviving noncomment Lean code lines, including 94.8% of the core localization lemmas and 96.6% of the theorem module, trace to those commits. Commits 5b1698879b05fc76597723347544cb0b02c268c4 and ef73ee27e4b0a8d1260350801c6915bfb56b6658 add substantial new proofs, including prime-generated descent and the fraction-field polynomial application. Coauthorship records support this classification but do not identify who wrote each individual line.”
- License: Apache-2.0.
- MSC2020: 13F15.
- In Lean Pool: LeanPool/NagataFactoriality, from the card LeanPool/projects/nagatafactoriality.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.