FiniteTensor.lean

1 import Mathlib.LinearAlgebra.PiTensorProduct.Basis
2 import Mathlib.LinearAlgebra.PiTensorProduct.Finite
3 import Mathlib.RepresentationTheory.Basic
4 import Mathlib.LinearAlgebra.Dimension.Finrank
5 
6 /-! Actual tensor products indexed by an arbitrary finite family, with their
7 external product actions. The empty family retains its scalar tensor unit. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.FiniteTensor
11 open TensorProduct
12 
13 variable {ι K : Type*} [Field K] {H V : ι → Type*}
14 variable [∀ i, Monoid (H i)] [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
15 
16 /-- The external tensor representation, on Mathlib's actual multiple tensor product. -/
17 def representation (σ : ∀ i, Representation K (H i) (V i)) :
18     Representation K (∀ i, H i) (PiTensorProduct K V) where
19   toFun h := PiTensorProduct.map (fun i => σ i (h i))
20   map_one' := by simp
21   map_mul' h k := by
22     simpa using PiTensorProduct.map_mul
23       (fun i => σ i (h i)) (fun i => σ i (k i))
24 
25 @[simp] theorem representation_tprod (σ : ∀ i, Representation K (H i) (V i))
26     (h : ∀ i, H i) (v : ∀ i, V i) :
27     representation σ h (PiTensorProduct.tprod K v) =
28       PiTensorProduct.tprod K (fun i => σ i (h i) (v i)) :=
29   PiTensorProduct.map_tprod _ _
30 
31 /-- The actual tensor dimension is the product of the actual factor dimensions. -/
32 theorem finrank [Fintype ι] [∀ i, FiniteDimensional K (V i)] :
33     Module.finrank K (PiTensorProduct K V) = ∏ i, Module.finrank K (V i) := by
34   classical
35   let b := Basis.piTensorProduct (fun i => Module.finBasis K (V i))
36   rw [Module.finrank_eq_card_basis b]
37   simp only [Fintype.card_pi, Fintype.card_fin]
38 
39 /-- In particular, the empty family has dimension one. -/
40 theorem finrank_empty [Fintype ι] [IsEmpty ι] [∀ i, FiniteDimensional K (V i)] :
41     Module.finrank K (PiTensorProduct K V) = 1 := by
42   rw [finrank]
43   simp
44 
45 /-- A product of nonzero finite-dimensional factors is nonzero, including the empty family. -/
46 theorem nontrivial [Fintype ι] [∀ i, FiniteDimensional K (V i)] [∀ i, Nontrivial (V i)] :
47     Nontrivial (PiTensorProduct K V) := by
48   apply Module.nontrivial_of_finrank_pos (R := K)
49   rw [finrank]
50   exact Finset.prod_pos (fun i _ => Module.finrank_pos)
51 
52 /-- The empty tensor equivalence intertwines the external action with the identity. -/
53 theorem empty_action [IsEmpty ι] (σ : ∀ i, Representation K (H i) (V i))
54     (h : ∀ i, H i) (x : PiTensorProduct K V) : representation σ h x = x := by
55   have hh : h = 1 := Subsingleton.elim _ _
56   rw [hh, map_one]
57   rfl
58 
59 /-- Multiplying every factor by a scalar multiplies its tensor by their product. -/
60 theorem scalar_map [Fintype ι] (c : ι → K) :
61     PiTensorProduct.map (fun i => c i • (LinearMap.id : V i →ₗ[K] V i)) =
62       (∏ i, c i) • LinearMap.id := by
63   apply PiTensorProduct.ext
64   ext v
65   simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod,
66     LinearMap.smul_apply, LinearMap.id_apply]
67   exact (PiTensorProduct.tprod K).map_smul_univ c v
68 
69 end PaperXI.FiniteTensor

Back to source controls