Associative rings and algebras
The Lean Pool projects whose card's first MSC2020 code is in class 16, Associative rings and algebras: 6 articles, one per card.
TheoremArtin-Wedderburn Theorem#
Formalizes the Artin-Wedderburn theorem for prime and simple Artinian rings.
Quoted from the card LeanPool/projects/artin-wedderburn.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.
LeanPool.ArtinWedderburn.ArtinWedderburnForPrime(theorem; a main declaration), declared in LeanPool/ArtinWedderburn/ArtinWedderburnTheorem.lean, line 36: “A nontrivial prime Artinian ring is isomorphic to a matrix ring over a division ring.”
Project
- Authors: Matevz Miščič, Maša Žaucer, Job Petrovčič.
- Source: A First Course in Noncommutative Rings by T. Y. Lam, doi:10.1007/978-1-4419-8616-0, arXiv:2405.04588.
- Project repository: JobPetrovcic/ArtinWedderburn.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2024 Job Petrovčič”.
- MSC2020: 16K20, 16P20.
- In Lean Pool: LeanPool/ArtinWedderburn, from the card LeanPool/projects/artin-wedderburn.yaml.
Sources
InstanceBrauer Group Core#
Formalizes central simple algebra infrastructure, Wedderburn-Artin structure theorems, and finite-field triviality for Brauer groups.
Quoted from the card LeanPool/projects/brauergroup_new.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 8 main results, each with its informal statement quoted from the card. The scan finds 8 of their declarations 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.
BrauerGroup.BruaerGroup(instance; a main declaration), declared in LeanPool/BrauerGroupNew/BrauerGroup.lean, line 409: “Constructs the Brauer group of a field from Brauer equivalence classes of central simple algebras.”BrauerGroupHom.Br(def; a main declaration), declared in LeanPool/BrauerGroupNew/BrauerGroup.lean, line 678: “Constructs the Brauer group functor from fields to commutative groups via scalar extension.”WedderburnArtin(theorem; a main declaration), declared in LeanPool/BrauerGroupNew/Wedderburn.lean, line 403: “Proves a Wedderburn-Artin decomposition for simple Artinian rings as matrix algebras over division rings.”trivialBrauer(theorem), declared in LeanPool/BrauerGroupNew/FiniteField.lean, line 38: “Proves that every element of the Brauer group of a finite field is trivial.”WedderburnArtin_algebra_version(lemma), declared in LeanPool/BrauerGroupNew/Wedderburn.lean, line 525: “Gives an algebra equivalence form of Wedderburn-Artin for finite-dimensional central simple algebras.”IsCentralSimple.TensorProduct.simple(instance), declared in LeanPool/BrauerGroupNew/CentralSimple.lean, line 493: “Proves simplicity of tensor products of central simple algebras over a field.”IsCentralSimple.TensorProduct.isCentral(instance), declared in LeanPool/BrauerGroupNew/CentralSimple.lean, line 252: “Proves centrality of tensor products of central algebras over a field.”CSA_implies_CSA(theorem), declared in LeanPool/BrauerGroupNew/CentralSimple.lean, line 569: “Shows that the division algebra factor in a matrix presentation of a central simple algebra is central over the base field.”
Project
- Authors: Yunzhou Xie, Yichen Feng, Jujian Zhang, Yael Dillies.
- Source: Central Simple Algebras and Galois Cohomology by Philippe Gille, Tamás Szamuely, https://doi.org/10.1017/9781316661277.
- Project repository: Whysoserioushah/BrauerGroup.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 16K20, 16K50, 16S35.
- In Lean Pool: LeanPool/BrauerGroupNew, from the card LeanPool/projects/brauergroup_new.yaml.
Sources
InstanceConnes-Kreimer Hopf algebra of rooted trees#
Formalizes the planar Connes-Kreimer/Foissy Hopf algebra of rooted trees, its cut coproduct, bialgebra and Hopf algebra structures, the commutative quotient, Adams operators, and the Eulerian idempotent on the quotient.
Quoted from the card LeanPool/projects/connes-kreimer.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations 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.
CK.instCKHopf(instance; a main declaration), declared in LeanPool/ConnesKreimer/Core.lean, line 992: “Constructs the planar rooted-tree Connes-Kreimer/Foissy Hopf algebra as a MathlibHopfAlgebra.”CK.instHabHopf(instance; a main declaration), declared in LeanPool/ConnesKreimer/Core.lean, line 1774: “Constructs the Hopf algebra structure on the commutative quotient of the planar rooted-tree algebra.”CK.eulerian1_idem_ab(theorem; a main declaration), declared in LeanPool/ConnesKreimer/Core.lean, line 2339: “Proves that the first Eulerian idempotent is idempotent on the commutative quotient.”CK.coassoc_map(theorem), declared in LeanPool/ConnesKreimer/Core.lean, line 344: “Lifts the list-level cut coassociativity proof to equality of linear maps for the coproduct.”PowerSeries.logOf_mul(theorem), declared in LeanPool/ConnesKreimer/PowerSeriesLogMul.lean, line 56: “Proves additivity ofPowerSeries.logOffor power series with constant coefficient one.”
Project
- Authors: Carles Marín.
- Source: How a Tree Remembers Its Cuts: the Connes-Kreimer-Foissy Hopf Algebra of Rooted Trees, Machine-Checked in Lean 4 by Carles Marín, doi:10.5281/zenodo.20762280.
- Project repository: karlesmarin/connes-kreimer-lean.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 16T05, 05C05, 81T15.
- In Lean Pool: LeanPool/ConnesKreimer, from the card LeanPool/projects/connes-kreimer.yaml.
Sources
TheoremDisproof of the Köthe conjecture (Krempa's matrix form)#
Refutes Köthe's 1930 conjecture in Krempa's matrix form: there is a ring R (the unitization of a nil algebra of three weighted backward shifts over the algebraic closure of F_2) with a nil two-sided ideal I such that the matrix ideal M_2(I) contains a non-nilpotent matrix. The compared theorem is exactly the negation of the research-open statement
Koethe.KotherConjecture.variants.general_matrixfrom Google DeepMind's Formal Conjectures, in every universe. The supporting library proves a multiprojective common-zero theorem via the Segre cone, the Nullstellensatz and Krull's height theorem, a mask-mortality theorem for one-row matrix pencils, a diagonal construction of universal mortal sequences, and a linearization theorem reducing nilness of a three-generator algebra to nilness of its root-row pencils.
Quoted from the card LeanPool/projects/koethe-conjecture-disproof.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations 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.
Koethe.KotherConjecture.variants.general_matrix.disproof(theorem; a main declaration), declared in LeanPool/Koethe/Disproof.lean, line 71: “It is not the case that for every ring R, every nil two-sided ideal I of R and every finite index type n, the matrix ideal M_n(I) of M_n(R) is nil. This is the negation of Krempa's matrix form of Köthe's conjecture, stated verbatim as in Formal Conjectures.”KoetheCounterexample.counterexample(theorem), declared in LeanPool/Koethe/Counterexample.lean, line 70: “In every universe there is a ring R with a nil two-sided ideal I such that some 2 x 2 matrix with entries in I is not nilpotent.”KoetheMultiProjective.exists_common_zero(theorem), declared in LeanPool/Koethe/MultiProjective.lean, line 752: “Over an algebraically closed field, at most 2N polynomials that are multihomogeneous of a common positive degree in each of N blocks of three variables have a common zero with no block equal to zero.”KoetheCounterexample.maskMortality(theorem), declared in LeanPool/Koethe/Mortality/MaskMortality.lean, line 144: “Over an algebraically closed field, every one-row matrix pencil and every periodic mask with more than half of its residues free admit a mask-compatible word of nonzero letters whose forward product is the zero matrix.”KoetheCounterexample.exists_universalMortalSequence(theorem), declared in LeanPool/Koethe/MaskSequence/Universal.lean, line 91: “Over a countable field satisfying mask mortality there is a sequence of nonzero letter triples such that every pencil has all its windows of some fixed positive length equal to zero.”KoetheCounterexample.nil_of_all_pencils_nil(theorem), declared in LeanPool/Koethe/Linearization/Nil.lean, line 89: “If every root-row pencil lifted along three elements of an algebra is nilpotent, then the non-unital subalgebra they generate is nil.”
Project
- Authors: Tom Adamczewski.
- Source: A counterexample to Köthe's conjecture and a question of Rowen by Tom Adamczewski, Bernhard Böhmler, Rene Marczinzik, arXiv:2609.07996.
- Project repository: tadamcz/koethe, at commit a94a72ae.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 16N40, 16S50.
- In Lean Pool: LeanPool/Koethe, from the card LeanPool/projects/koethe-conjecture-disproof.yaml.
Sources
InstancePolylean Unit Conjecture Counterexample#
Formalizes Gardam's counterexample to Kaplansky's Unit Conjecture, including the Promislow group, group rings, torsion-freeness of the group, and the non-trivial unit in 𝔽₂[P].
Quoted from the card LeanPool/projects/polylean.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations 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.
LeanPool.Polylean.P.torsionFree(instance; a main declaration), declared in LeanPool/Polylean/UnitConjecture/TorsionFree.lean, line 189: “Proves that the Promislow group used in Gardam's construction is torsion-free.”LeanPool.Polylean.Gardam.GardamTheorem(theorem; a main declaration), declared in LeanPool/Polylean/UnitConjecture/GardamTheorem.lean, line 177: “Proves Gardam's counterexample to Kaplansky's Unit Conjecture by constructing a non-trivial unit in the group ring 𝔽₂[P].”
Project
- Authors: Siddhartha Gadgil, Anand Rao.
- Source: doi:10.4007/annals.2021.194.3.9, arXiv:2102.11818.
- Project repository: siddhartha-gadgil/Polylean.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 16S34, 20F65.
- In Lean Pool: LeanPool/Polylean, from the card LeanPool/projects/polylean.yaml.
Sources
TheoremStafford 3.8#
Lean formalization of Stafford's Conjecture 3.8 for every characteristic-zero field and every Weyl-algebra rank, proving that each nonzero d admits F, R, and S with 1 = d*R + F*d*S. The development also proves an exact Bernstein-degree fixed-source strengthening and derived localization, adjoint, and evolutionary results.
Quoted from the card LeanPool/projects/stafford38-formal.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations 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.
Stafford38.universalStatement(theorem; a main declaration), declared in LeanPool/Stafford38/Stafford38/FoundationClosure.lean, line 74: “For every characteristic-zero field, every Weyl algebra rank, and every nonzero d, there are F, R, S with 1 = d*R + F*d*S.”Stafford38.universalFixedSourceStatement(theorem), declared in LeanPool/Stafford38/Stafford38/FoundationClosure.lean, line 78: “The stated fixed-source strengthening holds with its exact Bernstein-degree bound.”
Project
- Authors: Christopher Albert.
- Project repository: itpplasma/stafford38-formal, at commit 1e234855.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 16S32.
- In Lean Pool: LeanPool/Stafford38, from the card LeanPool/projects/stafford38-formal.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.