DualityLinear.lean

1 import PaperXI.RepresentationStability
2 import Mathlib.LinearAlgebra.Dual.Lemmas
3 import Mathlib.RepresentationTheory.Invariants
4 
5 /-! Actual dual representations, invariant spaces and tensor/Hom comparison.
6 No fixed-space dimension, invariant-space equivalence or dual irreducibility
7 is supplied as a hypothesis. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.DualityLinear
11 open scoped TensorProduct
12 open Representation
13 variable {k G V W : Type*} [Field k] [Group G]
14 variable [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
15 
16 /-- Restrict an actual equivariant linear equivalence to fixed subspaces. -/
17 def invariantsEquiv (ρ : Representation k G V) (σ : Representation k G W)
18     (e : Representation.Equiv ρ σ) : ρ.invariants ≃ₗ[k] σ.invariants where
19   toFun x := ⟨e x, fun g => by
20     have h := LinearMap.congr_fun (e.isIntertwining' g) (x : V)
21     change e (ρ g x) = σ g (e x) at h
22     rw [x.property g] at h
23     exact h.symm⟩
24   invFun x := ⟨e.symm x, fun g => by
25     have h := LinearMap.congr_fun (e.symm.isIntertwining' g) (x : W)
26     change e.symm (σ g x) = ρ g (e.symm x) at h
27     rw [x.property g] at h
28     exact h.symm⟩
29   left_inv x := by apply Subtype.ext; exact e.toLinearEquiv.symm_apply_apply x
30   right_inv x := by apply Subtype.ext; exact e.toLinearEquiv.apply_symm_apply x
31   map_add' x y := by apply Subtype.ext; exact e.map_add x y
32   map_smul' c x := by apply Subtype.ext; exact e.map_smul c x
33 
34 /-- The canonical double-dual equivalence is equivariant. -/
35 def bidualEquiv [FiniteDimensional k V] (ρ : Representation k G V) :
36     Representation.Equiv ρ ρ.dual.dual where
37   toLinearEquiv := Module.evalEquiv k V
38   isIntertwining' g := by
39     ext v f
40     simp [Representation.dual_apply, Module.Dual.transpose_apply]
41 
42 /-- The annihilator in V of a stable dual subspace is stable in V. -/
43 theorem coannihilator_stable (ρ : Representation k G V)
44     (S : Submodule k (Module.Dual k V))
45     (hS : PaperXI.RepresentationStability.Stable ρ.dual S) :
46     PaperXI.RepresentationStability.Stable ρ S.dualCoannihilator := by
47   intro g v hv
48   rw [Submodule.mem_dualCoannihilator] at hv ⊢
49   intro f hf
50   have hh := hv (ρ.dual g⁻¹ f) (hS g⁻¹ f hf)
51   simpa [Representation.dual_apply, Module.Dual.transpose_apply] using hh
52 
53 /-- Finite-dimensional duality preserves irreducibility; proved by annihilators. -/
54 theorem dual_irreducible [FiniteDimensional k V]
55     (ρ : Representation k G V) [Representation.IsIrreducible ρ] :
56     Representation.IsIrreducible ρ.dual := by
57   let : Nontrivial V := PaperXI.GeneratedIrreducibility.nontrivial_space ρ
58   let : Nontrivial (Module.Dual k V) := inferInstance
59   apply PaperXI.RepresentationStability.irreducible_of_stable
60   intro S hS
61   have h := PaperXI.RepresentationStability.eq_bot_or_top ρ S.dualCoannihilator
62     (coannihilator_stable ρ S hS)
63   have he := Subspace.dualCoannihilator_dualAnnihilator_eq (W := S)
64   rcases h with h | h
65   · right
66     simpa [h] using he.symm
67   · left
68     simpa [h] using he.symm
69 
70 /-- Actual V tensor W is Hom(V*,W), with its natural group action. -/
71 def tensorHomEquiv [FiniteDimensional k V] [FiniteDimensional k W]
72     (ρ : Representation k G V) (σ : Representation k G W) :
73     Representation.Equiv (ρ.tprod σ) (Representation.linHom ρ.dual σ) where
74   toLinearEquiv :=
75     (TensorProduct.congr (Module.evalEquiv k V) (LinearEquiv.refl k W)).trans
76       (dualTensorHomEquiv (R := k) (M := Module.Dual k V) (N := W))
77   isIntertwining' g := by
78     ext v w f
79     simp [Representation.dual_apply, Module.Dual.transpose_apply]
80 
81 /-- Fixed tensors correspond linearly to genuine intertwining maps. -/
82 def fixedTensorHomEquiv [FiniteDimensional k V] [FiniteDimensional k W]
83     (ρ : Representation k G V) (σ : Representation k G W) :
84     (ρ.tprod σ).invariants ≃ₗ[k] Representation.IntertwiningMap ρ.dual σ :=
85   (invariantsEquiv _ _ (tensorHomEquiv ρ σ)).trans
86     (Representation.invariantsEquivIntertwiningMap ρ.dual σ)
87 
88 theorem hom_finrank_eq_tensor_invariants [FiniteDimensional k V] [FiniteDimensional k W]
89     (ρ : Representation k G V) (σ : Representation k G W) :
90     Module.finrank k (Representation.IntertwiningMap ρ.dual σ) =
91       Module.finrank k (ρ.tprod σ).invariants :=
92   (fixedTensorHomEquiv ρ σ).finrank_eq.symm
93 
94 end PaperXI.DualityLinear

Back to source controls