Nonassociative rings and algebras
The Lean Pool projects whose card's first MSC2020 code is in class 17, Nonassociative rings and algebras: 6 articles, one per card.
TheoremClassification of low-dimensional solvable Lie algebras#
Formalises the classification of solvable Lie algebras up to dimension three.
Quoted from the card LeanPool/projects/lowdimsolvclassification.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.
LieAlgebra.Dim3.classification(theorem; a main declaration), declared in LeanPool/LowDimSolvClassification/Classification3.lean, line 293: “Classifies three-dimensional solvable Lie algebras over arbitrary fields.”
Project
- Authors: Viviana del Barco, Gustavo Infanti, Exequiel Rivas, Paul Schwahn.
- Source: Classification and Identification of Lie Algebras by Pavel Winternitz, Libor Šnobl, doi:10.1090/crmm/033, https://bookstore.ams.org/crmm-33.
- Project repository: LieLean/LowDimSolvClassification.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 17B30.
- In Lean Pool: LeanPool/LowDimSolvClassification, from the card LeanPool/projects/lowdimsolvclassification.yaml.
Sources
TheoremComposition Algebras over Commutative Rings#
Develops conic algebras, Cayley--Dickson doubling, and finitely generated projective composition algebras over an arbitrary commutative ring, following Garibaldi, Petersson and Racine. Composition algebras are alternative over every base. Over a nontrivial base, if the underlying module has constant rank, that rank is 1, 2, 4 or 8. Over LG rings, a class containing all fields and semilocal rings, composition algebras are classified by their norms, and reduced composition algebras are shown to be split. Along the way the project proves Witt cancellation for quadratic forms over LG rings by the elementary Dias--Baeza--Knebusch route, Artin's theorem that a ring is alternative if and only if its two-generated subrings are associative, freeness of constant-rank projective modules over LG rings, and the classification of composition algebras over the reals and over finite fields. These main results do not assume that 2 is invertible.
Quoted from the card LeanPool/projects/composition-algebras-over-rings.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 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.
QuadraticForm.cancel(theorem; a main declaration), declared in LeanPool/CompositionAlgebrasOverRings/QuadraticForm/WittCancellation.lean, line 208: “Witt cancellation over an LG ring. If the orthogonal sums of q1 and of q2 with q3 are isometric, where q2 is nonsingular and q3 is regular on finitely generated projective modules, then q1 and q2 are isometric.”IsAlternative.isAlternative_iff_two_generated_assoc(theorem), declared in LeanPool/CompositionAlgebrasOverRings/Nonassociative/Alternative/Artin.lean, line 501: “Artin's theorem. A non-associative ring is alternative if and only if every subring generated by two elements is associative.”Module.free_of_isLGRing_of_rankAtStalk_eq(theorem), declared in LeanPool/CompositionAlgebrasOverRings/LGRing/ConstantRank.lean, line 96: “Over an LG ring, a finitely generated projective module of constant rank is free.”ConicAlgebra.IsComposition.isAlternative_general(theorem), declared in LeanPool/CompositionAlgebrasOverRings/Composition/Alternative.lean, line 184: “Every composition algebra over every commutative ring is alternative, with no hypothesis on 2, on the rank, or on nontriviality of the base ring.”ConicAlgebra.IsComposition.rankAtStalk_classification(theorem; a main declaration), declared in LeanPool/CompositionAlgebrasOverRings/Composition/RankOneTwoFourEight.lean, line 529: “A composition algebra of constant rank over a nontrivial commutative ring has rank 1, 2, 4 or 8; it is the base ring in rank 1, commutative and associative in rank 2, associative but not commutative in rank 4, and alternative but not associative in rank 8.”ConicAlgebra.IsComposition.exists_isometryEquiv_map_one_map_mul(theorem), declared in LeanPool/CompositionAlgebrasOverRings/Composition/NormClassification.lean, line 987: “Over an LG ring, composition algebras with isometric norms are isomorphic.”ConicAlgebra.IsReduced.isSplit_of_isLGRing(theorem), declared in LeanPool/CompositionAlgebrasOverRings/Composition/Reduced/Classification.lean, line 295: “Over an LG ring, every reduced composition algebra is split.”
Project
- Authors: Skip Garibaldi.
- Source: Albert Algebras over Commutative Rings by Skip Garibaldi, Holger P. Petersson, Michel L. Racine, doi:10.1017/9781009426862.
- Project repository: skipgaribaldi/CompositionAlgebras-lean, at commit 87b1eeb4.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 17A75, 17D05, 11E81, 11E08, 13C10.
- In Lean Pool: LeanPool/CompositionAlgebrasOverRings, from the card LeanPool/projects/composition-algebras-over-rings.yaml.
Sources
TheoremEuclidean Jordan algebras and the frame Peirce decomposition#
The frame Peirce decomposition: relative to a Jordan frame, a Euclidean Jordan algebra is the internal direct sum of the blocks V_ij over unordered pairs of frame indices, and in finite dimension the diagonal blocks are lines, dim V_ii = 1 - the Faraut-Koranyi table entry. The frame is carried as data, so frame conjugacy is sidestepped and nothing here claims anything about the rank of J. Machine checked, not peer reviewed, no priority claim.
Quoted from the card LeanPool/projects/euclidean-jordan.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.
EuclideanJordan.frameBlock_isInternal(theorem; a main declaration), declared in LeanPool/EuclideanJordan/EuclideanJordan/FramePeirce.lean, line 466: “A Euclidean Jordan algebra is the internal direct sum of the Peirce blocks associated with a Jordan frame.”EuclideanJordan.finrank_frameBlock_diag(theorem), declared in LeanPool/EuclideanJordan/EuclideanJordan/FramePeirceMul.lean, line 312: “In finite dimension, every diagonal block of a Jordan frame has dimension one.”
Project
- Authors: Bryan Ehrlich.
- Project repository: ehrlich-b/euclidean-jordan, at commit a83407e4.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 17C20, 17C27, 17C37, 17C65, 17A15, 46L70.
- In Lean Pool: LeanPool/EuclideanJordan, from the card LeanPool/projects/euclidean-jordan.yaml.
Sources
DefinitionExplicit type Aₙ and BCₙ root pairings#
Constructs the type Aₙ and BCₙ root pairings explicitly over ℤ — from signed intervals on Fin n and from the reflective vectors of the standard dot product — proves the pairing and reflection identities exhibiting them as Mathlib
RootPairings, and identifies the BCₙ roots with the classical set {±eᵢ, ±2eᵢ, ±eᵢ ± eⱼ}.
Quoted from the card LeanPool/projects/root-system.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 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.
An.rootPairing(def; a main declaration), declared in LeanPool/RootSystem/An.lean, line 456: “Constructs the type Aₙ root pairing over the integers from signed intervals on Fin n, with finiteness, reducedness, and crystallographic properties.” Its source, as the card gives it: “N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Springer, 2002; J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Springer, 1972, Ch. III.”BCn.rootPairing(def; a main declaration), declared in LeanPool/RootSystem/BCn.lean, line 81: “Constructs the type BCₙ root pairing from the reflective vectors of the standard dot product on ℤⁿ via a symmetric nondegenerate form.”BCn.isReflective_iff_isClassicalRoot(theorem; a main declaration), declared in LeanPool/RootSystem/BCn.lean, line 259: “Characterizes the reflective vectors of the standard dot product on ℤⁿ as exactly the classical type BCₙ roots ±eᵢ, ±2eᵢ, and ±eᵢ ± eⱼ for i ≠ j.”BCn.range_rootPairing_root(theorem), declared in LeanPool/RootSystem/BCn.lean, line 265: “Identifies the root set of the type BCₙ root pairing with the classical type BCₙ root set.”
Project
- Authors: Antoine de Saint Germain, Ambrose Tang.
- Source: Introduction to Lie Algebras and Representation Theory by James E. Humphreys, doi:10.1007/978-1-4612-6398-2, https://antoine-dsg.github.io/root_system/.
- Project repository: Antoine-dSG/root_system.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 17B22, 20F55.
- In Lean Pool: LeanPool/RootSystem, from the card LeanPool/projects/root-system.yaml.
Sources
TheoremHurwitz's Classification of Euclidean Composition Algebras#
Formalizes Hurwitz's classification of nontrivial finite-dimensional real Euclidean composition algebras: every such algebra has dimension 1, 2, 4, or 8 and is real-linearly equivalent to the real numbers, complex numbers, quaternions, or octonions through a map preserving the unit, multiplication, and norm form. The development also constructs the octonions from an explicit Fano multiplication table, proves Degen's eight-square identity, and shows that Cayley--Dickson doubling preserves the composition law for associative inputs.
Quoted from the card LeanPool/projects/composition-algebras.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 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.
CompositionAlgebra.hurwitz_classification(theorem; a main declaration), declared in LeanPool/CompositionAlgebras/Composition/Classification.lean, line 341: “Every nontrivial finite-dimensional real Euclidean composition algebra is linearly equivalent to the real numbers, complex numbers, quaternions, or octonions through a map preserving the unit, multiplication, and norm form.”CompositionAlgebra.finrank_eq_one_or_two_or_four_or_eight(theorem), declared in LeanPool/CompositionAlgebras/Composition/Hurwitz.lean, line 354: “The real dimension of a nontrivial finite-dimensional Euclidean composition algebra is exactly 1, 2, 4, or 8.”CompositionAlgebra.CD.instCompositionAlgebra(instance), declared in LeanPool/CompositionAlgebras/Composition/CayleyDickson.lean, line 247: “The Cayley--Dickson double of a nontrivial associative Euclidean composition algebra again satisfies the composition law.”Octonion.nucleus_real(theorem), declared in LeanPool/CompositionAlgebras/OctonionNucleus.lean, line 55: “Any octonion that associates in the third slot with every pair has zero imaginary coordinates and hence lies on the real line.”
Project
- Authors: Bryan Ehrlich.
- Source: Über die Composition der quadratischen Formen von beliebig vielen Variablen by Adolf Hurwitz, https://eudml.org/doc/58420.
- Project repository: ehrlich-b/composition-algebras, at commit e37e22b0.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 17A75, 17A35, 11E88.
- In Lean Pool: LeanPool/CompositionAlgebras, from the card LeanPool/projects/composition-algebras.yaml.
Sources
DefinitionVirasoro Project#
Formalizes the Virasoro algebra, its Witt-algebra central extension, Verma modules, and the basic bosonic Sugawara construction.
Quoted from the card LeanPool/projects/virasoroproject.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.
VirasoroProject.VirasoroAlgebra(def; a main declaration), declared in LeanPool/VirasoroProject/VirasoroAlgebra.lean, line 69: “Defines the Virasoro algebra as a one-dimensional central extension of the Witt algebra.”VirasoroProject.sugawaraRepresentation(def; a main declaration), declared in LeanPool/VirasoroProject/Sugawara.lean, line 750: “Constructs the basic bosonic Sugawara representation of the Virasoro algebra from locally truncated Heisenberg actions.”
Project
- Authors: Kalle Kytölä.
- Source: Infinite-Dimensional Lie Algebras by Victor Kac, https://doi.org/10.1017/CBO9780511626234.
- Project repository: kkytola/VirasoroProject.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 17B68, 17B56, 81R10.
- In Lean Pool: LeanPool/VirasoroProject, from the card LeanPool/projects/virasoroproject.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.