SurjectiveRepresentationPullback.lean

1 import PaperX.CompatibleSystemRigidity
2 
3 /-! Pullback along a surjective monoid homomorphism preserves and reflects the
4 actual representation structure: invariant subspaces, equivariant linear
5 isomorphisms, irreducibility, and characters. No finite-group or topological
6 assumption is needed for these algebraic statements. -/
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperX.SurjectiveRepresentationPullback
11 
12 section Algebra
13 variable {K G H V W : Type*} [Field K] [Monoid G] [Monoid H]
14 variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
15 variable (f : G →* H) (hf : Function.Surjective f)
16 variable (ρ : Representation K H V) (τ : Representation K H W)
17 
18 include hf in
19 /-- Equivariance on a surjective pullback is exactly equivariance for the
20 original action. This applies to arbitrary linear maps, including projectors. -/
21 theorem intertwines_iff (u : V →ₗ[K] W) :
22     (∀ g, u.comp ((ρ.comp f) g) = ((τ.comp f) g).comp u) ↔
23       ∀ h, u.comp (ρ h) = (τ h).comp u := by
24   constructor
25   · intro hu h
26     obtain ⟨g, rfl⟩ := hf h
27     exact hu g
28   · intro hu g
29     exact hu (f g)
30 
31 /-- Pull back an actual equivariant linear isomorphism. Surjectivity is not
32 needed in this direction. -/
33 def pullbackEquiv (e : ρ.Equiv τ) : Representation.Equiv (ρ.comp f) (τ.comp f) :=
34   Representation.Equiv.mk e.toLinearEquiv (fun g => e.isIntertwining' (f g))
35 
36 /-- Descend an actual equivariant linear isomorphism through a surjective
37 homomorphism. The underlying linear isomorphism does not change. -/
38 def equivOfPullback (e : Representation.Equiv (ρ.comp f) (τ.comp f)) : ρ.Equiv τ :=
39   Representation.Equiv.mk e.toLinearEquiv
40     ((intertwines_iff f hf ρ τ e.toLinearMap).mp e.isIntertwining')
41 
42 @[simp]
43 theorem pullbackEquiv_apply (e : ρ.Equiv τ) (v : V) :
44     pullbackEquiv f ρ τ e v = e v := rfl
45 
46 @[simp]
47 theorem equivOfPullback_apply (e : Representation.Equiv (ρ.comp f) (τ.comp f)) (v : V) :
48     equivOfPullback f hf ρ τ e v = e v := rfl
49 
50 include hf in
51 /-- Surjective pullback preserves and reflects isomorphism of representations,
52 even on different coefficient modules. -/
53 theorem nonempty_equiv_iff :
54     Nonempty (Representation.Equiv (ρ.comp f) (τ.comp f)) ↔ Nonempty (ρ.Equiv τ) := by
55   constructor
56   · rintro ⟨e⟩
57     exact ⟨equivOfPullback f hf ρ τ e⟩
58   · rintro ⟨e⟩
59     exact ⟨pullbackEquiv f ρ τ e⟩
60 
61 /-- The invariant-subspace lattices agree exactly under surjective pullback.
62 Both directions keep the underlying submodule. -/
63 def subrepresentationOrderIso : Subrepresentation (ρ.comp f) ≃o Subrepresentation ρ where
64   toFun S :=
65     { toSubmodule := S.toSubmodule
66       apply_mem_toSubmodule := by
67         intro h v hv
68         obtain ⟨g, rfl⟩ := hf h
69         exact S.apply_mem_toSubmodule g hv }
70   invFun S :=
71     { toSubmodule := S.toSubmodule
72       apply_mem_toSubmodule := fun g _ hv => S.apply_mem_toSubmodule (f g) hv }
73   left_inv S := by ext v; rfl
74   right_inv S := by ext v; rfl
75   map_rel_iff' := Iff.rfl
76 
77 @[simp]
78 theorem subrepresentationOrderIso_toSubmodule (S : Subrepresentation (ρ.comp f)) :
79     (subrepresentationOrderIso f hf ρ S).toSubmodule = S.toSubmodule := rfl
80 
81 include hf in
82 /-- Irreducibility is preserved and reflected, including its nontriviality
83 requirement. No finite-dimensional hypothesis is required. -/
84 theorem isIrreducible_iff : Representation.IsIrreducible (ρ.comp f) ↔ ρ.IsIrreducible :=
85   (subrepresentationOrderIso f hf ρ).isSimpleOrder_iff
86 
87 /-- The character of a pullback is the original character evaluated at the
88 image of the acting element. -/
89 theorem character_pullback (g : G) :
90     Representation.character (ρ.comp f) g = ρ.character (f g) := rfl
91 
92 /-- A prescribed image identifies the actual character at every lift. -/
93 theorem character_of_image (g : G) (h : H) (hg : f g = h) :
94     Representation.character (ρ.comp f) g = ρ.character h := by
95   rw [character_pullback, hg]
96 
97 end Algebra
98 
99 section Systems
100 variable {Λ I G H : Type*} [Group G] [Group H]
101 variable {K : Λ → Type*} [∀ l, Field (K l)]
102 variable {W : Λ → I → Type*} [∀ l i, AddCommGroup (W l i)]
103   [∀ l i, Module (K l) (W l i)]
104 
105 /-- Pulling every member back through a surjection preserves and reflects the
106 componentwise equivalence relation used for compatible systems. -/
107 theorem memberwiseEquiv_iff (f : G →* H) (hf : Function.Surjective f)
108     (ρ : (l : Λ) → (i : I) → Representation (K l) H (W l i)) (i j : I) :
109     PaperX.CompatibleSystemRigidity.MemberwiseEquiv (fun l i => (ρ l i).comp f) i j ↔
110       PaperX.CompatibleSystemRigidity.MemberwiseEquiv ρ i j := by
111   constructor <;> intro h l
112   · exact (nonempty_equiv_iff f hf (ρ l i) (ρ l j)).mp (h l)
113   · exact (nonempty_equiv_iff f hf (ρ l i) (ρ l j)).mpr (h l)
114 
115 end Systems
116 end PaperX.SurjectiveRepresentationPullback

Back to source controls