SchurHom.lean

1 import PaperXI.DualityLinear
2 import PaperXI.SchurScalar
3 
4 /-! Exact Hom dimensions for actual irreducible complex representations. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.SchurHom
8 open Representation
9 open scoped Classical
10 variable {G V W : Type*} [Group G]
11 variable [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W]
12 
13 /-- An equivalence transports Hom(V,W) to End(V), linearly. -/
14 def postcomposeEquiv (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
15     (e : Representation.Equiv ρ σ) :
16     Representation.IntertwiningMap ρ σ ≃ₗ[ℂ] Representation.IntertwiningMap ρ ρ where
17   toFun f := e.symm.toIntertwiningMap.comp f
18   invFun f := e.toIntertwiningMap.comp f
19   left_inv f := by ext x; exact e.toLinearEquiv.apply_symm_apply (f x)
20   right_inv f := by ext x; exact e.toLinearEquiv.symm_apply_apply (f x)
21   map_add' f g := by ext x; exact e.toLinearEquiv.symm.map_add (f x) (g x)
22   map_smul' c f := by ext x; exact e.toLinearEquiv.symm.map_smul c (f x)
23 
24 /-- The Schur zero-or-one statement uses isomorphism, not an assumed dimension. -/
25 theorem finrank_eq_indicator [FiniteDimensional ℂ V]
26     (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
27     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ] :
28     Module.finrank ℂ (Representation.IntertwiningMap ρ σ) =
29       if Nonempty (Representation.Equiv ρ σ) then 1 else 0 := by
30   classical
31   by_cases h : Nonempty (Representation.Equiv ρ σ)
32   · rw [ite_eq_left h]
33     obtain ⟨e⟩ := h
34     rw [(postcomposeEquiv ρ σ e).finrank_eq]
35     exact Representation.IsIrreducible.finrank_intertwiningMap_self ρ
36   · let : IsEmpty (Representation.Equiv ρ σ) := ⟨fun e => h ⟨e⟩⟩
37     rw [ite_eq_right h]
38     exact Module.finrank_zero_of_subsingleton
39 
40 theorem finrank_zero_or_one [FiniteDimensional ℂ V]
41     (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
42     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ] :
43     Module.finrank ℂ (Representation.IntertwiningMap ρ σ) = 0 ∨
44       Module.finrank ℂ (Representation.IntertwiningMap ρ σ) = 1 := by
45   classical
46   rw [finrank_eq_indicator ρ σ]
47   split_ifs <;> simp
48 
49 theorem finrank_one_iff_equiv [FiniteDimensional ℂ V]
50     (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
51     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ] :
52     Module.finrank ℂ (Representation.IntertwiningMap ρ σ) = 1 ↔
53       Nonempty (Representation.Equiv ρ σ) := by
54   classical
55   rw [finrank_eq_indicator ρ σ]
56   split_ifs <;> simp_all
57 
58 /-- There cannot be two independent invariant tensors for irreducible inputs. -/
59 theorem tensor_invariants_zero_or_one [FiniteDimensional ℂ V] [FiniteDimensional ℂ W]
60     (ρ : Representation ℂ G V) (σ : Representation ℂ G W)
61     [Representation.IsIrreducible ρ] [Representation.IsIrreducible σ] :
62     Module.finrank ℂ (ρ.tprod σ).invariants = 0 ∨
63       Module.finrank ℂ (ρ.tprod σ).invariants = 1 := by
64   let : Representation.IsIrreducible ρ.dual := PaperXI.DualityLinear.dual_irreducible ρ
65   rw [← PaperXI.DualityLinear.hom_finrank_eq_tensor_invariants ρ σ]
66   exact finrank_zero_or_one ρ.dual σ
67 
68 end PaperXI.SchurHom

Back to source controls