TensorSubspace.lean

1 import Mathlib.LinearAlgebra.Dimension.Constructions
2 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
3 import Mathlib.RingTheory.Flat.Basic
4 
5 /-! Tensoring a multiplicity subspace with a nonzero finite-dimensional
6 factor preserves whether it is zero or the whole space. The actual image
7 is transported through a specified, independently proved tensor equivalence. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.TensorSubspace
11 open scoped TensorProduct
12 
13 variable {k W M X : Type*} [Field k]
14 variable [AddCommGroup W] [Module k W] [AddCommGroup M] [Module k M]
15 variable [AddCommGroup X] [Module k X]
16 
17 /-- The actual tensor image of a subspace through the given equivalence. -/
18 def image (e : W ⊗[k] M ≃ₗ[k] X) (L : Submodule k M) : Submodule k X :=
19   LinearMap.range (e.toLinearMap.comp (L.subtype.lTensor W))
20 
21 theorem inclusion_injective (L : Submodule k M) :
22     Function.Injective (L.subtype.lTensor W) :=
23   Module.Flat.lTensor_preserves_injective_linearMap L.subtype L.subtype_injective
24 
25 theorem map_injective (e : W ⊗[k] M ≃ₗ[k] X) (L : Submodule k M) :
26     Function.Injective (e.toLinearMap.comp (L.subtype.lTensor W)) :=
27   e.injective.comp (inclusion_injective L)
28 
29 theorem tmul_mem (e : W ⊗[k] M ≃ₗ[k] X) (L : Submodule k M)
30     (w : W) (m : M) (hm : m ∈ L) : e (w ⊗ₜ[k] m) ∈ image e L := by
31   exact ⟨w ⊗ₜ[k] (⟨m, hm⟩ : L), by simp⟩
32 
33 /-- Stability follows from the actual factorwise action on pure tensors. -/
34 theorem image_stable (e : W ⊗[k] M ≃ₗ[k] X) (L : Submodule k M)
35     (P : Module.End k X) (A : Module.End k W) (B : Module.End k M)
36     (hL : ∀ m, m ∈ L → B m ∈ L)
37     (hP : ∀ w m, P (e (w ⊗ₜ[k] m)) = e (A w ⊗ₜ[k] B m)) :
38     ∀ x, x ∈ image e L → P x ∈ image e L := by
39   rintro x ⟨t, rfl⟩
40   induction t using TensorProduct.induction_on with
41   | zero => simp
42   | add s t hs ht => simpa using (image e L).add_mem hs ht
43   | tmul w m =>
44     change P (e (w ⊗ₜ[k] (m : M))) ∈ image e L
45     rw [hP]
46     exact tmul_mem e L (A w) (B m) (hL m m.property)
47 
48 theorem finrank_image (e : W ⊗[k] M ≃ₗ[k] X) (L : Submodule k M) :
49     Module.finrank k (image e L) = Module.finrank k W * Module.finrank k L := by
50   rw [image, LinearMap.finrank_range_of_inj (map_injective e L)]
51   exact Module.finrank_tensorProduct
52 
53 variable [FiniteDimensional k W] [FiniteDimensional k M] [Nontrivial W]
54 
55 theorem image_eq_bot_iff (e : W ⊗[k] M ≃ₗ[k] X) (L : Submodule k M) :
56     image e L = ⊥ ↔ L = ⊥ := by
57   let : FiniteDimensional k X := Module.Finite.equiv e
58   rw [← Submodule.finrank_eq_zero, finrank_image, ← Submodule.finrank_eq_zero]
59   exact mul_eq_zero.trans (or_iff_right (ne_of_gt (Module.finrank_pos (R := k) (M := W))))
60 
61 theorem image_eq_top_iff (e : W ⊗[k] M ≃ₗ[k] X) (L : Submodule k M) :
62     image e L = ⊤ ↔ L = ⊤ := by
63   let : FiniteDimensional k X := Module.Finite.equiv e
64   have he : Module.finrank k X = Module.finrank k W * Module.finrank k M := by
65     rw [← e.finrank_eq, Module.finrank_tensorProduct]
66   constructor
67   · intro h
68     apply Submodule.eq_top_of_finrank_eq
69     apply Nat.eq_of_mul_eq_mul_left (Module.finrank_pos (R := k) (M := W))
70     have hr := congrArg (fun S : Submodule k X => Module.finrank k S) h
71     simpa only [finrank_image, finrank_top, he] using hr
72   · rintro rfl
73     apply Submodule.eq_top_of_finrank_eq
74     rw [finrank_image, finrank_top, he]
75 
76 end PaperXI.TensorSubspace

Back to source controls