feat(LinearAlgebra/ExteriorPower): add HodgeStar

[kirill-kondrashov]

---

Implements the plan #maths > Hodge star operator @ 💬

GPT-5.6 Luna Max was used to fill in the sorry blocks in a manually written definition with a review comments from Zulip from @ocfnash .

Then there were conducted many iterations of manual and LLM-generated changes with very specific prompts addressing concrete code issues until the initial iteration was almost fully overwritten.

Closes #17722

Co-authored-by: @ocfnash

[github-actions]

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.

[kirill-kondrashov]

WIP

[github-actions]

PR summary 40624f3148

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.ExteriorPower.WedgePairing (new file)	1700
Mathlib.LinearAlgebra.ExteriorPower.HodgeStar (new file)	1717

---

Declarations diff (regex)

+ basis_mul_of_complement
+ basis_mul_of_not_disjoint
+ bijective_wedgePairing
+ disjoint_compl
+ disjoint_iff_eq_compl
+ hodgeStar
+ topVector
+ volumeBasis
+ volumeCoordinate
+ volumeCoordinate_topVector_ne_zero
+ wedgePairing
+ wedgePairingBasis
+ wedgePairingBasis_apply
+ wedgePairingEquiv
+ wedgePairingEquiv_apply

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- stale, waiting for the new build)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 660400e).

• +6 new declarations
• −0 removed declarations

+Module.Basis.groupSMul.congr_simp
+exteriorPower.hodgeStar
+exteriorPower.hodgeStar_apply
+exteriorPower.hodgeStar_symm_apply
+exteriorPower.wedgePairingEquiv
+exteriorPower.wedgePairingEquiv.congr_simp

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5046	1

Current commit 40624f3148
Reference commit 52b284ff12

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[kirill-kondrashov]

LLM-generated

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[kirill-kondrashov]

-WIP

[wwylele]

I am not super familiar with this topic, but as a general guideline, could you add appropriate simp lemma for each morphism def? Usually they are in the shape of "applying the morphism on a element = some unbundled function applications". Try @[simps] first to see if it can correctly generate them

This includes complementEquiv, volumeCoordinate, wedgePairing, wedgePairingEquiv, and hodgeStar

If there is a good reason not to provide these lemma, it should be noted in the description.

[kirill-kondrashov]

I am not super familiar with this topic, but as a general guideline, could you add appropriate simp lemma for each morphism def? Usually they are in the shape of "applying the morphism on a element = some unbundled function applications". Try @[simps] first to see if it can correctly generate them

This includes complementEquiv, volumeCoordinate, wedgePairing, wedgePairingEquiv, and hodgeStar

If there is a good reason not to provide these lemma, it should be noted in the description.

@wwylele That's a good point, I tried that and applied changes.

[kirill-kondrashov]

t-algebra

[ocfnash]

Thanks, I've left some initial review. I'll try to follow up more promptly once you've have had a chance to respond to these suggestions.

[ocfnash]

What you're really doing here is turning a non-zero vector of a one-dimensional vector space into linear form. If we really need this construction, then we should develop that in generality elsewhere in the library, rather than in this very specific case.

However if the data you really need is such a linear form, then you might as give yourself this data by defining vol as (vol : Dual K (⋀[K]^(finrank K V) V)) and avoid needing to do this here. (Depending on how things work out, at the very end of the API when we get to the Hodge star, we could support users who want to pass in a volume form living in ⋀[K]^(finrank K V) V but I think not here.)

[kirill-kondrashov]

That's a good point, let me change that part.