Skip to content

feat(LinearAlgebra/CliffordAlgebra): bivector Lie subalgebra#36917

Open
iarnoldy wants to merge 7 commits intoleanprover-community:masterfrom
iarnoldy:bivector-lie-subalgebra
Open

feat(LinearAlgebra/CliffordAlgebra): bivector Lie subalgebra#36917
iarnoldy wants to merge 7 commits intoleanprover-community:masterfrom
iarnoldy:bivector-lie-subalgebra

Conversation

@iarnoldy
Copy link
Copy Markdown

@iarnoldy iarnoldy commented Mar 20, 2026

Define the submodule of grade-n elements (n-vectors) in a Clifford algebra
and show that bivectors (n = 2) form a LieSubalgebra under the commutator
bracket. This gives the standard construction of so(Q) from Cl(Q).

Main definitions:

  • CliffordAlgebra.nvector — grade-n submodule, spanned by n-fold products of ι
  • CliffordAlgebra.bivector — nvector 2 Q, the bivector submodule
  • CliffordAlgebra.bivectorLieSubalgebra — LieSubalgebra of bivectors

Main results:

  • CliffordAlgebra.lie_ι_mul_ι — explicit commutator formula for bivector generators
  • CliffordAlgebra.lie_mem_bivector — bracket closure of the bivector submodule
  • CliffordAlgebra.bivector_le_evenOdd_zero — bivectors lie in the even part

The LieModule instance for CliffordAlgebra Q acting on itself is provided
explicitly (instLieModuleSelf) because automatic synthesis exceeds the default
heartbeat limit.

AI disclosure: This code was generated with AI assistance (Claude, Anthropic).
The submitter directed the construction and QA but is not a Lean programmer.
The mathematical content is classical (Doran & Lasenby, Ch. 3). Extra review
scrutiny is welcomed.

Co-authored-by: Claude [email protected]

Open design questions for reviewers:

  1. Naming: Is nvector the right name? Eric Wieser suggested generalizing
    to n-vectors. Alternatives: ιProd, grade, or following the exteriorPower
    pattern via equivExterior pullback.

  2. Scalar contamination: The spanning set {ι m₁ * ι m₂} includes
    ι m * ι m = Q(m) (scalars). Eric suggested pulling back exteriorPower
    through equivExterior for pure grades (requires Invertible (2 : R)).
    Happy to rework if that's preferred.

  3. instLieModuleSelf: Should this be an upstream issue rather than a
    local workaround? @ocfnash

  4. ι_mul_ι_comm': This may duplicate existing API (ι_mul_ι_comm b a
    plus polar_comm). Happy to inline if reviewers prefer.

Discussed on Zulip: https://leanprover.zulipchat.com (Is there code for X? thread)

iarnoldy and others added 2 commits March 20, 2026 15:22
@iarnoldy @claude
feat(LinearAlgebra/CliffordAlgebra): bivector Lie subalgebra
6de452a 
Define the submodule of bivectors in a Clifford algebra (spanned by
products `ι Q m₁ * ι Q m₂`) and show it forms a `LieSubalgebra` under
the commutator bracket. This gives the standard construction of the
orthogonal Lie algebra so(Q) from Cl(Q).

Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
@iarnoldy @claude
refactor: generalize to nvector, eliminate noncomm_ring
4261fc2 
Generalize bivector definition to nvector n Q (grade-n submodule),
with bivector Q := nvector Q 2. Replace all noncomm_ring calls with
direct rw chains (mul_assoc, sub_mul, Algebra.commutes). Close
lie_ι_mul_ι with abel. Drop Tactic.NoncommRing import.

Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 20, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 20, 2026

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 awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

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
Copy link
Copy Markdown

github-actions bot commented Mar 20, 2026 •
edited
Loading

PR summary 1f3cdaa7a7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.LinearAlgebra.CliffordAlgebra.Bivector (new file) 1619

Declarations diff

+ bivector
+ bivectorLieSubalgebra
+ bivector_le_evenOdd_zero
+ instLieModuleSelf
+ lie_mem_bivector
+ lie_ι_mul_ι
+ lie_ι_mul_ι_mem_bivector
+ mem_bivector
+ mem_bivectorLieSubalgebra
+ mem_nvector
+ mul_ι_mul_ι_left
+ mul_ι_mul_ι_right
+ nvector
+ nvector_two_prod
+ prod_ι_mem_nvector
+ zero_mem_bivector
+ ι_mul_ι_comm'
+ ι_mul_ι_mem_bivector

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Mar 20, 2026
iarnoldy added 5 commits March 20, 2026 18:42
@iarnoldy
chore: add Bivector to import file
8c19aa7 
Register Mathlib.LinearAlgebra.CliffordAlgebra.Bivector in Mathlib.lean.
@iarnoldy
fix: add module declaration and public imports
655e7e3 
Mathlib requires `module` declaration and `public import` syntax.
@iarnoldy
fix: use @[expose] public section, not noncomputable section
083e78f 
Match current mathlib convention: all CliffordAlgebra files use
@[expose] public section with noncomputable on individual defs
where needed.
@iarnoldy
fix: convert algebraMap to smul for Submodule.smul_mem
3a5bacc 
Use Algebra.algebraMap_eq_smul_one to convert algebraMap R _ r * x
to r • (1 * x) = r • x before applying Submodule.smul_mem.
@iarnoldy
fix: remove @[simp] from ι_mul_ι_mem_bivector
e3abb60 
The simp linter reports that mem_bivector already simplifies the
LHS, making this @[simp] attribute redundant.
@themathqueen themathqueen added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 21, 2026
@dagurtomas dagurtomas removed their assignment Apr 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@eric-wieser eric-wieser

Labels

LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@iarnoldy @eric-wieser @themathqueen @dagurtomas