Skip to content

Commit 84ddc46

Browse files
morrison-danielmorrison-daniel
committed
feat(LinearAlgebra/PiTensorProduct): PiTensorProducts over Finsupp, DFinsupp, and DirectSum (leanprover-community#32456)
Adds linear equivalences for `PiTensorProduct`s taken over `Finsupp`, `DFinsupp`, and `DirectSum`. The main definitions are: * `PiTensorProduct.ofDFinsuppEquiv` is the linear equivalence of tensor products over `DFinsupp` to a `DFinsupp` of tensor products * `PiTensorProduct.ofFinsuppEquiv` is the linear equivalence of tensor products over `Finsupp` to a `Finsupp` of tensor products * `PiTensorProduct.ofDirectSumEquiv` is the linear equivalence of tensor products over a direct sum to the direct sum over tensor products
1 parent 4d124cb commit 84ddc46

4 files changed

Lines changed: 207 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4652,6 +4652,9 @@ public import Mathlib.LinearAlgebra.PerfectPairing.Matrix
46524652
public import Mathlib.LinearAlgebra.PerfectPairing.Restrict
46534653
public import Mathlib.LinearAlgebra.Pi
46544654
public import Mathlib.LinearAlgebra.PiTensorProduct
4655+
public import Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
4656+
public import Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
4657+
public import Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
46554658
public import Mathlib.LinearAlgebra.Prod
46564659
public import Mathlib.LinearAlgebra.Projection
46574660
public import Mathlib.LinearAlgebra.Projectivization.Action

‎Mathlib/LinearAlgebra/PiTensorProduct/DFinsupp.lean‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
/-
2+
Copyright (c) 2024 Sophie Morel. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Sophie Morel, Eric Wieser
5+
-/
6+
module
7+
8+
public import Mathlib.LinearAlgebra.PiTensorProduct
9+
public import Mathlib.LinearAlgebra.DFinsupp
10+
public import Mathlib.LinearAlgebra.Multilinear.DFinsupp
11+
12+
/-!
13+
# Tensor products of finitely supported functions
14+
15+
This file shows that taking `PiTensorProduct`s commutes with taking `DFinsupp`s in all arguments.
16+
17+
## Main results
18+
19+
* `ofDFinsuppEquiv`: the linear equivalence between a `PiTensorProduct` of `DFinsupp`s
20+
and the `DFinsupp` of the `PiTensorProduct`s.
21+
-/
22+
23+
@[expose] public section
24+
25+
namespace PiTensorProduct
26+
27+
open LinearMap TensorProduct
28+
29+
variable {R ι : Type*} {κ : ι → Type*} {M : (i : ι) → κ i → Type*}
30+
[CommSemiring R] [Π i (j : κ i), AddCommMonoid (M i j)] [Π i (j : κ i), Module R (M i j)]
31+
[Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)]
32+
33+
/-- The `ι`-ary tensor product distributes over `κ i`-ary finitely supported functions. -/
34+
def ofDFinsuppEquiv :
35+
(⨂[R] i, (Π₀ j : κ i, M i j)) ≃ₗ[R] Π₀ p : Π i, κ i, ⨂[R] i, M i (p i) :=
36+
LinearEquiv.ofLinear
37+
(lift <| MultilinearMap.fromDFinsuppEquiv κ R
38+
fun p ↦ (DFinsupp.lsingle p).compMultilinearMap (tprod R))
39+
(DFinsupp.lsum R fun p ↦ lift <|
40+
(PiTensorProduct.map fun i ↦ DFinsupp.lsingle (p i)).compMultilinearMap (tprod R))
41+
(by ext p x; simp)
42+
(by ext x; simp)
43+
44+
@[simp]
45+
theorem ofDFinsuppEquiv_tprod_single (p : Π i, κ i) (x : Π i, M i (p i)) :
46+
ofDFinsuppEquiv (⨂ₜ[R] i, DFinsupp.single (p i) (x i)) =
47+
DFinsupp.single p (⨂ₜ[R] i, x i) := by
48+
simp [ofDFinsuppEquiv]
49+
50+
@[simp]
51+
theorem ofDFinsuppEquiv_symm_single_tprod (p : Π i, κ i) (x : Π i, M i (p i)) :
52+
ofDFinsuppEquiv.symm (DFinsupp.single p (tprod R x)) =
53+
(⨂ₜ[R] i, DFinsupp.single (p i) (x i)) := by
54+
simp [ofDFinsuppEquiv]
55+
56+
@[simp]
57+
theorem ofDFinsuppEquiv_tprod_apply (x : Π i, Π₀ j, M i j) (p : Π i, κ i) :
58+
ofDFinsuppEquiv (tprod R x) p = ⨂ₜ[R] i, x i (p i) := by
59+
classical
60+
simpa [ofDFinsuppEquiv, MultilinearMap.fromDFinsuppEquiv_apply] using fun i hi ↦
61+
((tprod R).map_coord_zero (m := fun i ↦ x i (p i)) i hi).symm
62+
63+
end PiTensorProduct

‎Mathlib/LinearAlgebra/PiTensorProduct/DirectSum.lean‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
/-
2+
Copyright (c) 2024 Sophie Morel. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Sophie Morel, Eric Wieser
5+
-/
6+
module
7+
8+
public import Mathlib.LinearAlgebra.PiTensorProduct
9+
public import Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
10+
public import Mathlib.Algebra.DirectSum.Module
11+
12+
/-!
13+
# Tensor products of direct sums
14+
15+
This file shows that taking `PiTensorProduct`s commutes with taking `DirectSum`s in all arguments.
16+
17+
## Main results
18+
19+
* `ofDirectSumEquiv`: the linear equivalence between a `PiTensorProduct` of `DirectSum`s
20+
and the `DirectSum` of the `PiTensorProduct`s.
21+
-/
22+
23+
@[expose] public section
24+
25+
namespace PiTensorProduct
26+
27+
open PiTensorProduct DirectSum TensorProduct
28+
29+
variable {R ι : Type*} {κ : ι → Type*} {M : (i : ι) → κ i → Type*}
30+
[CommSemiring R] [Π i (j : κ i), AddCommMonoid (M i j)] [Π i (j : κ i), Module R (M i j)]
31+
32+
open scoped Classical in
33+
/-- The n-ary tensor product distributes over m-ary direct sums. -/
34+
noncomputable def ofDirectSumEquiv [Finite ι] :
35+
(⨂[R] i, (⨁ j : κ i, M i j)) ≃ₗ[R] ⨁ p : Π i, κ i, ⨂[R] i, M i (p i) :=
36+
have : Fintype ι := Fintype.ofFinite ι
37+
ofDFinsuppEquiv
38+
39+
@[simp]
40+
theorem ofDirectSumEquiv_tprod_lof [Fintype ι] [(i : ι) → DecidableEq (κ i)]
41+
(p : Π i, κ i) (x : Π i, M i (p i)) :
42+
ofDirectSumEquiv (⨂ₜ[R] i, DirectSum.lof R _ _ (p i) (x i)) =
43+
DirectSum.lof R _ _ p (⨂ₜ[R] i, x i) := by
44+
classical
45+
rw [ofDirectSumEquiv]
46+
convert ofDFinsuppEquiv_tprod_single p x
47+
48+
@[simp]
49+
theorem ofDirectSumEquiv_symm_lof_tprod [Fintype ι] [(i : ι) → DecidableEq (κ i)]
50+
(p : Π i, κ i) (x : Π i, M i (p i)) :
51+
ofDirectSumEquiv.symm (DirectSum.lof R _ _ p (tprod R x)) =
52+
(⨂ₜ[R] i, DirectSum.lof R _ _ (p i) (x i)) := by
53+
classical
54+
rw [ofDirectSumEquiv]
55+
convert ofDFinsuppEquiv_symm_single_tprod p x
56+
57+
@[simp]
58+
theorem ofDirectSumEquiv_tprod_apply [Finite ι]
59+
(x : Π i, ⨁ j, M i j) (p : Π i, κ i) :
60+
ofDirectSumEquiv (tprod R x) p = ⨂ₜ[R] i, x i (p i) := by
61+
have : Fintype ι := Fintype.ofFinite ι
62+
convert ofDFinsuppEquiv_tprod_apply _ _
63+
64+
end PiTensorProduct

‎Mathlib/LinearAlgebra/PiTensorProduct/Finsupp.lean‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
/-
2+
Copyright (c) 2025 Daniel Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Daniel Morrison
5+
-/
6+
module
7+
8+
public import Mathlib.Data.Finsupp.ToDFinsupp
9+
public import Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
10+
public import Mathlib.RingTheory.PiTensorProduct
11+
12+
/-!
13+
# Results on finitely supported functions.
14+
15+
* `ofFinsuppEquiv`, the tensor product of the family `κ i →₀ M i` indexed by `ι` is linearly
16+
equivalent to `∏ i, κ i →₀ ⨂[R] i, M i`.
17+
-/
18+
19+
@[expose] public section
20+
21+
namespace PiTensorProduct
22+
23+
open PiTensorProduct BigOperators TensorProduct
24+
25+
attribute [local ext] TensorProduct.ext
26+
27+
variable {R ι : Type*} {κ M : ι → Type*}
28+
variable [CommSemiring R] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (κ i)]
29+
variable [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] [∀ i, DecidableEq (M i)]
30+
31+
/-- If `ι` is a `Fintype`, `κ i` is a family of types indexed by `ι` and `M i` is a family
32+
of modules indexed by `ι`, then the tensor product of the family `κ i →₀ M i` is linearly
33+
equivalent to `∏ i, κ i →₀ ⨂[R] i, M i`.
34+
-/
35+
noncomputable def ofFinsuppEquiv :
36+
(⨂[R] i, κ i →₀ M i) ≃ₗ[R] ((i : ι) → κ i) →₀ ⨂[R] i, M i :=
37+
haveI := Classical.typeDecidableEq (⨂[R] (i : ι), M i)
38+
PiTensorProduct.congr (fun _ ↦ finsuppLequivDFinsupp R) ≪≫ₗ
39+
ofDFinsuppEquiv ≪≫ₗ
40+
(finsuppLequivDFinsupp R).symm
41+
42+
@[simp]
43+
theorem ofFinsuppEquiv_tprod_single (p : (i : ι) → κ i) (m : (i : ι) → M i) :
44+
ofFinsuppEquiv (⨂ₜ[R] i, Finsupp.single (p i) (m i)) =
45+
Finsupp.single p (⨂ₜ[R] i, m i) := by
46+
simp [ofFinsuppEquiv]
47+
48+
@[simp]
49+
theorem ofFinsuppEquiv_apply (f : (i : ι) → (κ i →₀ M i)) (p : (i : ι) → κ i) :
50+
ofFinsuppEquiv (⨂ₜ[R] i, f i) p = ⨂ₜ[R] i, f i (p i) := by
51+
simp [ofFinsuppEquiv]
52+
53+
@[simp]
54+
theorem ofFinsuppEquiv_symm_single_tprod (p : (i : ι) → κ i) (m : (i : ι) → M i) :
55+
ofFinsuppEquiv.symm (Finsupp.single p (⨂ₜ[R] i, m i)) =
56+
⨂ₜ[R] i, Finsupp.single (p i) (m i) :=
57+
(LinearEquiv.symm_apply_eq _).2 (ofFinsuppEquiv_tprod_single _ _).symm
58+
59+
variable [DecidableEq R]
60+
61+
/-- A variant of `ofFinsuppEquiv` where all modules `M i` are the ground ring. -/
62+
noncomputable def ofFinsuppEquiv' : (⨂[R] i, (κ i →₀ R)) ≃ₗ[R] ((i : ι) → κ i) →₀ R :=
63+
ofFinsuppEquiv ≪≫ₗ
64+
Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) (constantBaseRingEquiv ι R).toLinearEquiv
65+
66+
@[simp]
67+
theorem ofFinsuppEquiv'_apply_apply (f : (i : ι) → κ i →₀ R) (p : (i : ι) → κ i) :
68+
ofFinsuppEquiv' (⨂ₜ[R] i, f i) p = ∏ i, f i (p i) := by
69+
simp [ofFinsuppEquiv']
70+
71+
@[simp]
72+
theorem ofFinsuppEquiv'_tprod_single (p : (i : ι) → κ i) (r : ι → R) :
73+
ofFinsuppEquiv' (⨂ₜ[R] i, Finsupp.single (p i) (r i)) =
74+
Finsupp.single p (∏ i, r i) := by
75+
simp [ofFinsuppEquiv']
76+
77+
end PiTensorProduct

0 commit comments

Comments
 (0)