feat(LinearAlgebra/MultilinearMap): generalize `MultilinearMap` with common `RingHom` by gloges · Pull Request #42534 · leanprover-community/mathlib4

gloges · 2026-08-07T13:29:57Z

Generalizes multilinear maps to multi-semilinear maps.
In analogy with LinearMap σ M N, MultilinearMap σ M N is the space of multilinear maps from the R-module ∀ i, M i to the S-module N over a ring homomorphism σ : R →+* S: fixing all but one coordinate gives a map M i →ₛₗ[σ] N.

Both ContinuousLinearMap and AlternatingMap extend MultilinearMap and are left defined in terms of RingHom.id.

github-actions · 2026-08-07T13:30:09Z

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 · 2026-08-07T13:31:26Z

PR summary 179fedd67f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ _root_.LinearEquiv.multilinearMapCongrRightₛₗ
+ _root_.LinearMap.compMultilinearMapₛₗ
+ compMultilinearMap_smulₛₗ
+ instance : Add (MultilinearMap σ M N)
+ instance : AddCommGroup (MultilinearMap σ M N) := fast_instance% FunLike.addCommGroup
+ instance : AddMonoid (MultilinearMap σ M N) := fast_instance% FunLike.addMonoid
+ instance : FunLike (MultilinearMap σ M N) (∀ i, M i) N
+ instance : Inhabited (MultilinearMap σ M N)
+ instance : IsAddApply (MultilinearMap σ M N) (∀ i, M i) N
+ instance : IsNegApply (MultilinearMap σ M N) (∀ i, M i) N
+ instance : IsSMulApply S' (MultilinearMap σ M N) (∀ i, M i) N
+ instance : IsSubApply (MultilinearMap σ M N) (∀ i, M i) N
+ instance : IsZeroApply (MultilinearMap σ M N) (∀ i, M i) N
+ instance : Module S (MultilinearMap σ₁₂ M₁ N₂) := fast_instance%
+ instance : Neg (MultilinearMap σ M N)
+ instance : SMul S' (MultilinearMap σ M N)
+ instance : Sub (MultilinearMap σ M N)
+ instance : Zero (MultilinearMap σ M N)
+ instance [Module.IsTorsionFree S N₂] : Module.IsTorsionFree S (MultilinearMap σ₁₂ M₁ N₂)
+ instance [Monoid S] [DistribMulAction S N₂] [SMulCommClass R₂ S N₂] :
+ instance _root_.Module.Finite.multilinearMap : Module.Finite R (MultilinearMap (.id R) M₁ M₂)
+ instance _root_.Module.Free.multilinearMap : Module.Free R (MultilinearMap (.id R) M₁ M₂)
+-++-- tprod
+-+- coe_mk
- instance : Add (MultilinearMap R M₁ M₂)
- instance : AddCommGroup (MultilinearMap R M₁ M₂) := fast_instance% FunLike.addCommGroup
- instance : AddMonoid (MultilinearMap R M₁ M₂) := fast_instance% FunLike.addMonoid
- instance : FunLike (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂
- instance : Inhabited (MultilinearMap R M₁ M₂)
- instance : IsAddApply (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂
- instance : IsNegApply (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂
- instance : IsSMulApply S (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂
- instance : IsSubApply (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂
- instance : IsZeroApply (MultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂
- instance : Module S (MultilinearMap R M₁ M₂) := fast_instance%
- instance : Neg (MultilinearMap R M₁ M₂)
- instance : SMul S (MultilinearMap R M₁ M₂)
- instance : Sub (MultilinearMap R M₁ M₂)
- instance : Zero (MultilinearMap R M₁ M₂)
- instance [Module.IsTorsionFree S M₂] : Module.IsTorsionFree S (MultilinearMap R M₁ M₂)
- instance [Monoid S] [DistribMulAction S M₂] [SMulCommClass R S M₂] :
- instance _root_.Module.Finite.multilinearMap : Module.Finite R (MultilinearMap R M₁ M₂)
- instance _root_.Module.Free.multilinearMap : Module.Free R (MultilinearMap R M₁ M₂)
-+-+ compMultilinearMap

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)

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

+13 new declarations
−0 removed declarations

+LinearEquiv.multilinearMapCongrLeft.congr_simp
+LinearEquiv.multilinearMapCongrRightₛₗ
+LinearEquiv.multilinearMapCongrRightₛₗ_apply
+LinearEquiv.multilinearMapCongrRightₛₗ_symm_apply
+LinearMap.compMultilinearMap.congr_simp
+LinearMap.compMultilinearMap_smulₛₗ
+LinearMap.compMultilinearMapₛₗ
+LinearMap.compMultilinearMapₛₗ.congr_simp
+LinearMap.compMultilinearMapₛₗ_apply
+MultilinearMap.compLinearMap.congr_simp
+MultilinearMap.compLinearMapMultilinear.congr_simp
+MultilinearMap.compLinearMapₗ.congr_simp
+MultilinearMap.piLinearMap.congr_simp

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 179fedd67f
Reference commit 20a3b032e0

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.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).

eric-wieser · 2026-08-07T14:44:28Z

-    g.compMultilinearMap (s • f) = s • g.compMultilinearMap f :=
+theorem compMultilinearMap_smul [DistribSMul S' N₂] [DistribSMul S' N₂']
+    [SMulCommClass R₂ S' N₂] [SMulCommClass R₂ S' N₂'] [CompatibleSMul N₂ N₂' S' R₂]
+    (g : N₂ →ₗ[R₂] N₂') (s : S') (f : MultilinearMap σ₁₂ M₁ N₂) :


Do we want a semilinear version of this lemma too?

Sounds good - added as compMultilinearMap_smulₛₗ.

eric-wieser · 2026-08-07T14:45:27Z

+    [LinearMap.CompatibleSMul N₂' N₂ S R₂] (g : N₂ ≃ₗ[R₂] N₂') :
+    MultilinearMap σ₁₂ M₁ N₂ ≃ₗ[S] MultilinearMap σ₁₂ M₁ N₂' where


Here I think we can introduce another ring in g

I've added LinearMap.compMultilinearMapₛₗ and LinearEquiv.multilinearMapCongrRightₛₗ for when R₂ and R₃ are commutative (making use of the new compMultilinearMap_smulₛₗ). Are these name okay?

eric-wieser · 2026-08-07T14:46:25Z

-theorem map_piecewise_smul [DecidableEq ι] (c : ι → R) (m : ∀ i, M₁ i) (s : Finset ι) :
-    f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, c i) • f m := by
+theorem map_piecewise_smul [DecidableEq ι] (c : ι → R) (m : ∀ i, M i) (s : Finset ι) :
+    f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, σ (c i)) • f m := by


Would we prefer the following, do you think?

Suggested change

f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, σ (c i)) • f m := by

f (s.piecewise (fun i => c i • m i) m) = σ (∏ i ∈ s, c i) • f m := by

I think ∏ i ∈ s, σ (c i) would be better - it doesn't require that R be commutative and is in normal form even when it is (c.f. map_prod).

eric-wieser · 2026-08-07T14:49:42Z

 `MultilinearMap R s E` with the property that its composition with the canonical
 `MultilinearMap R s (⨂[R] i, s i)` is the given multilinear map. -/
-def liftAux (φ : MultilinearMap R s E) : (⨂[R] i, s i) →+ E :=
+def liftAux (φ : MultilinearMap (.id R) s E) : (⨂[R] i, s i) →+ E :=


Is the intent to generalize this in a follow-up PR?

Yes - after some tinkering I think it will take more than superficial changes to generalize the TensorProduct.lift and TensorProduct.map machinery, so I'd like to do this in a separate PR.

eric-wieser

This looks great, thanks! I think it's ok to keep MultilinearMap (.id R) around in downstream files in this PR, and address those in a follow-up.

gloges added 17 commits August 7, 2026 16:00

var organize

cd9554b

basic to semilinear

4280cde

tidy variables

e5e1710

update docs

6b398a4

curry to semilinear

627320f

finsupp to semilinear

48f05eb

directsum to semilinear

078bf0b

finitedim to semilinear

3c63066

basis to semilinear

1e0af59

pi to semilinear

fc4d761

tensorproduct to semilinear

92aff5f

fix alternating

2fad446

fix alternating domcoprod

463c312

fix tensoralgebra

a815a52

fix pitensorproduct

60280a5

fix normed

0b0c0cf

fix misc

0cb8d40

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 Aug 7, 2026

eric-wieser reviewed Aug 7, 2026

View reviewed changes

gloges added 3 commits August 8, 2026 12:11

add compMultilinearMap_smul

c373b4c

compMultilinearMap/multilinearMapCongrRight variants

2c1ce6b

stray variable

97156f8

gloges marked this pull request as ready for review August 8, 2026 05:50

fix file length

179fedd

gloges mentioned this pull request Aug 8, 2026

feat(LinearAlgeabra/PiTensorProduct): add lifts of multi-semilinear maps #42575

Open

1 task

Navigation Menu

Uh oh!

feat(LinearAlgebra/MultilinearMap): generalize `MultilinearMap` with common `RingHom` - #42534

feat(LinearAlgebra/MultilinearMap): generalize `MultilinearMap` with common `RingHom`#42534
gloges wants to merge 21 commits into
leanprover-community:masterfrom
gloges:multi-linear-map

gloges commented Aug 7, 2026

Uh oh!

github-actions Bot commented Aug 7, 2026

Uh oh!

github-actions Bot commented Aug 7, 2026 •

edited

Loading

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

eric-wieser Aug 7, 2026

Uh oh!

gloges Aug 8, 2026

Uh oh!

eric-wieser Aug 7, 2026

Uh oh!

gloges Aug 8, 2026

Uh oh!

eric-wieser Aug 7, 2026

Uh oh!

gloges Aug 8, 2026

Uh oh!

eric-wieser Aug 7, 2026

Uh oh!

gloges Aug 8, 2026

Uh oh!

eric-wieser left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		[LinearMap.CompatibleSMul N₂' N₂ S R₂] (g : N₂ ≃ₗ[R₂] N₂') :
		MultilinearMap σ₁₂ M₁ N₂ ≃ₗ[S] MultilinearMap σ₁₂ M₁ N₂' where

	f (s.piecewise (fun i => c i • m i) m) = (∏ i ∈ s, σ (c i)) • f m := by
	f (s.piecewise (fun i => c i • m i) m) = σ (∏ i ∈ s, c i) • f m := by

Uh oh!

Conversation

gloges commented Aug 7, 2026

Uh oh!

github-actions Bot commented Aug 7, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 179fedd67f

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented Aug 7, 2026 •

edited

Loading