TameHomCriterion.lean

1 import PaperXI.SchurHom
2 import PaperXI.TensorFixed
3 
4 /-! Corollary 5.7: the actual tensor fixed space is the actual Hom space.
5 The refined packet data are precisely the inherited Proposition 5.6 contract.
6 The 0/1 bound is derived from irreducibility, not supplied with the packets. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.TameHomCriterion
10 open scoped BigOperators Classical TensorProduct
11 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.GeneratedIrreducibility
12 variable {G I X Y : Type*} [Group G] [Group I]
13 variable [AddCommGroup X] [Module ℂ X] [FiniteDimensional ℂ X]
14 variable [AddCommGroup Y] [Module ℂ Y] [FiniteDimensional ℂ Y]
15 variable {A : Type*} [Fintype A] {V : A → Type*}
16 variable [∀ a, AddCommGroup (V a)] [∀ a, Module ℂ (V a)] [∀ a, FiniteDimensional ℂ (V a)]
17 variable {M : ℕ} [NeZero M]
18 
19 /-- Actual Hom dimension, computed by the refined tensor packet test. -/
20 theorem hom_finrank_eq_trivial_count
21     (ξ : Representation ℂ G X) (η : Representation ℂ G Y) (τ : ∀ a, Representation ℂ G (V a))
22     (e : (X ⊗[ℂ] Y) ≃ₗ[ℂ] (∀ a, V a)) (he : ∀ g x a, e ((ξ.tprod η) g x) a = τ a g (e x a))
23     (ι : I →* G) (φ : G) (hgen : Submonoid.closure (Set.range ι ∪ {φ, φ⁻¹}) = ⊤)
24     (ρ : ∀ a, Action (K := ℂ) (V := V a) (M := M))
25     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s)
26     (hfactor : ∀ a, (τ a).comp ι = (ρ a).comp s) (q : (ZMod M)ˣ)
27     (hrel : ∀ a, (actionEquiv (τ a) φ).symm.conj (operator (ρ a) 1) =
28       operator (ρ a) (q : ZMod M))
29     (n : A → ℕ) (hn : ∀ a, 0 < n a) (b : ∀ a, Module.Basis (Fin (n a)) ℂ (V a))
30     (j : A → ZMod M) (v : ∀ a, V a) (hv : ∀ a, v a ∈ packet (ρ a) (j a))
31     (hb : ∀ a (i : Fin (n a)), b a i = (actionEquiv (τ a) φ ^ (i : ℕ)) (v a))
32     (c : A → ℂ) (hclose : ∀ a, (actionEquiv (τ a) φ ^ n a) (v a) = c a • v a) :
33     Module.finrank ℂ (Representation.IntertwiningMap ξ.dual η) =
34       (Finset.univ.filter (fun a => j a = 0 ∧ c a = 1)).card := by
35   rw [PaperXI.DualityLinear.hom_finrank_eq_tensor_invariants ξ η]
36   exact PaperXI.TensorFixed.count_trivial_packets (ξ.tprod η) τ e he ι φ hgen ρ s hs
37     hfactor q hrel n hn b j v hv hb c hclose
38 
39 /-- Source-facing zero-or-one criterion for irreducible tame atoms. -/
40 theorem tame_hom_test
41     (ξ : Representation ℂ G X) (η : Representation ℂ G Y)
42     [Representation.IsIrreducible ξ] [Representation.IsIrreducible η] (τ : ∀ a, Representation ℂ G (V a))
43     (e : (X ⊗[ℂ] Y) ≃ₗ[ℂ] (∀ a, V a)) (he : ∀ g x a, e ((ξ.tprod η) g x) a = τ a g (e x a))
44     (ι : I →* G) (φ : G) (hgen : Submonoid.closure (Set.range ι ∪ {φ, φ⁻¹}) = ⊤)
45     (ρ : ∀ a, Action (K := ℂ) (V := V a) (M := M))
46     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s)
47     (hfactor : ∀ a, (τ a).comp ι = (ρ a).comp s) (q : (ZMod M)ˣ)
48     (hrel : ∀ a, (actionEquiv (τ a) φ).symm.conj (operator (ρ a) 1) =
49       operator (ρ a) (q : ZMod M))
50     (n : A → ℕ) (hn : ∀ a, 0 < n a) (b : ∀ a, Module.Basis (Fin (n a)) ℂ (V a))
51     (j : A → ZMod M) (v : ∀ a, V a) (hv : ∀ a, v a ∈ packet (ρ a) (j a))
52     (hb : ∀ a (i : Fin (n a)), b a i = (actionEquiv (τ a) φ ^ (i : ℕ)) (v a))
53     (c : A → ℂ) (hclose : ∀ a, (actionEquiv (τ a) φ ^ n a) (v a) = c a • v a) :
54     let N := (Finset.univ.filter (fun a => j a = 0 ∧ c a = 1)).card
55     Module.finrank ℂ (Representation.IntertwiningMap ξ.dual η) = N ∧
56       (N = 0 ∨ N = 1) ∧
57       (Module.finrank ℂ (Representation.IntertwiningMap ξ.dual η) = 1 ↔ N = 1) := by
58   dsimp only
59   have hcount := hom_finrank_eq_trivial_count ξ η τ e he ι φ hgen ρ s hs hfactor q hrel
60     n hn b j v hv hb c hclose
61   let : Representation.IsIrreducible ξ.dual := PaperXI.DualityLinear.dual_irreducible ξ
62   have hdim := PaperXI.SchurHom.finrank_zero_or_one ξ.dual η
63   rw [hcount] at hdim
64   exact ⟨hcount, hdim, by rw [hcount]⟩
65 
66 end PaperXI.TameHomCriterion

Back to source controls