ScalarHolonomy.lean

1 import Mathlib.Analysis.Complex.Basic
2 import Mathlib.Algebra.Module.Equiv.Basic
3 import Mathlib.LinearAlgebra.Dimension.Finrank
4 
5 /-! Scalar loop operators and the faithfulness boundary at rank zero. -/
6 set_option autoImplicit false
7 noncomputable section
8 
9 namespace PaperXI.ScalarHolonomy
10 
11 variable {K G V W : Type*} [Field K] [Group G]
12 variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
13 
14 /-- Scalars act by actual invertible linear operators, including on the zero space. -/
15 def scalarHom : Kˣ →* (V ≃ₗ[K] V) where
16   toFun := LinearEquiv.smulOfUnit
17   map_one' := by ext x; simp [LinearEquiv.smulOfUnit]
18   map_mul' a b := by ext x; simp [LinearEquiv.smulOfUnit, smul_smul]
19 
20 @[simp] theorem scalarHom_apply (c : Kˣ) (x : V) :
21     scalarHom (V := V) c x = (c : K) • x := rfl
22 
23 /-- Conjugation transports a scalar operator to the same scalar operator at any rank. -/
24 theorem scalar_conjugate (U : V ≃ₗ[K] W) (c : Kˣ) :
25     ((U.symm.trans (scalarHom c)).trans U) = scalarHom c := by
26   ext x
27   simp
28 
29 /-- Changing the identifying isomorphism has no effect on an actual scalar operator. -/
30 theorem scalar_conjugate_independent (U Q : V ≃ₗ[K] W) (A : V ≃ₗ[K] V)
31     (hA : ∃ c : Kˣ, A = scalarHom c) :
32     ((U.symm.trans A).trans U) = ((Q.symm.trans A).trans Q) := by
33   obtain ⟨c, rfl⟩ := hA
34   rw [scalar_conjugate, scalar_conjugate]
35 
36 /-- A nonzero vector makes the unit scalar identifiable. -/
37 theorem scalarHom_injective [Nontrivial V] :
38     Function.Injective (scalarHom (K := K) (V := V)) := by
39   intro a b h
40   obtain ⟨x, hx⟩ := exists_ne (0 : V)
41   apply Units.ext
42   exact (smul_left_injective K hx) (LinearEquiv.congr_fun h x)
43 
44 /-- Scalarity is a property of the actual operators. -/
45 def IsScalar (ρ : G →* (V ≃ₗ[K] V)) : Prop :=
46   ∀ g, ∃ c : Kˣ, ρ g = scalarHom c
47 
48 /-- For a nonzero space, scalar loop operators determine a character. -/
49 def character [Nontrivial V] (ρ : G →* (V ≃ₗ[K] V)) (hρ : IsScalar ρ) : G →* Kˣ where
50   toFun g := Classical.choose (hρ g)
51   map_one' := by
52     apply scalarHom_injective (V := V)
53     rw [← Classical.choose_spec (hρ 1), map_one, map_one]
54   map_mul' g h := by
55     apply scalarHom_injective (V := V)
56     rw [← Classical.choose_spec (hρ (g * h)), map_mul, map_mul,
57       ← Classical.choose_spec (hρ g), ← Classical.choose_spec (hρ h)]
58 
59 @[simp] theorem character_spec [Nontrivial V]
60     (ρ : G →* (V ≃ₗ[K] V)) (hρ : IsScalar ρ) (g : G) :
61     scalarHom (character ρ hρ g) = ρ g := (Classical.choose_spec (hρ g)).symm
62 
63 theorem character_apply [Nontrivial V]
64     (ρ : G →* (V ≃ₗ[K] V)) (hρ : IsScalar ρ) (g : G) (x : V) :
65     ρ g x = (character ρ hρ g : K) • x := by
66   rw [← character_spec ρ hρ g, scalarHom_apply]
67 
68 /-- The extracted character is the only scalar character realizing these operators. -/
69 theorem character_unique [Nontrivial V]
70     (ρ : G →* (V ≃ₗ[K] V)) (hρ : IsScalar ρ) (χ : G →* Kˣ)
71     (hχ : ∀ g, scalarHom (χ g) = ρ g) : χ = character ρ hρ := by
72   apply MonoidHom.ext
73   intro g
74   apply scalarHom_injective (V := V)
75   rw [hχ, character_spec]
76 
77 /-- Scalar operators on nonzero spaces intertwine exactly when their scalars agree. -/
78 theorem intertwines_iff [Nontrivial V] (U : V ≃ₗ[K] W) (a b : Kˣ) :
79     (∀ x, U (scalarHom a x) = scalarHom b (U x)) ↔ a = b := by
80   constructor
81   · intro h
82     obtain ⟨x, hx⟩ := exists_ne (0 : V)
83     have hUx : U x ≠ 0 := by simpa using (U.map_ne_zero_iff).mpr hx
84     apply Units.ext
85     exact (smul_left_injective K hUx) (by simpa using h x)
86   · intro h
87     subst b
88     intro x
89     simp
90 
91 /-- The matrix intertwining criterion becomes equality of the two scalar characters. -/
92 theorem character_intertwines_iff [Nontrivial V] [Nontrivial W]
93     (ρ : G →* (V ≃ₗ[K] V)) (σ : G →* (W ≃ₗ[K] W))
94     (hρ : IsScalar ρ) (hσ : IsScalar σ) (U : V ≃ₗ[K] W) :
95     (∀ g x, U (ρ g x) = σ g (U x)) ↔ character ρ hρ = character σ hσ := by
96   constructor
97   · intro h
98     apply MonoidHom.ext
99     intro g
100     apply (intertwines_iff U _ _).mp
101     simpa only [character_spec] using h g
102   · intro h g x
103     rw [character_apply ρ hρ, character_apply σ hσ, map_smul]
104     exact congrArg (fun c : Kˣ => (c : K) • U x) (DFunLike.congr_fun h g)
105 
106 /-- Ratios of scalar characters are characters even for nonabelian loop groups. -/
107 def ratio (χ ψ : G →* Kˣ) : G →* Kˣ := ψ * χ⁻¹
108 
109 @[simp] theorem ratio_apply (χ ψ : G →* Kˣ) (g : G) :
110     ratio χ ψ g = ψ g * (χ g)⁻¹ := rfl
111 
112 theorem ratio_eq_one_iff (χ ψ : G →* Kˣ) : ratio χ ψ = 1 ↔ χ = ψ := by
113   constructor
114   · intro h
115     apply MonoidHom.ext
116     intro g
117     exact (mul_inv_eq_one.mp (DFunLike.congr_fun h g)).symm
118   · intro h
119     subst ψ
120     apply MonoidHom.ext
121     intro g
122     exact mul_inv_cancel (χ g)
123 
124 theorem ratio_apply_eq_one_iff (χ ψ : G →* Kˣ) (g : G) :
125     ratio χ ψ g = 1 ↔ χ g = ψ g := by
126   change ψ g * (χ g)⁻¹ = 1 ↔ χ g = ψ g
127   rw [mul_inv_eq_one]
128   exact eq_comm
129 
130 /-- On a zero space every invertible operator is the same operator. -/
131 theorem zero_space_operator_eq [Subsingleton V] (A B : V ≃ₗ[K] V) : A = B := by
132   ext x
133   exact Subsingleton.elim _ _
134 
135 /-- Consequently the intertwining equations impose no condition on scalar representatives. -/
136 theorem zero_space_intertwines [Subsingleton V] (U : V ≃ₗ[K] W)
137     (A : V ≃ₗ[K] V) (B : W ≃ₗ[K] W) (x : V) : U (A x) = B (U x) := by
138   have hx : x = 0 := Subsingleton.elim _ _
139   simp [hx]
140 
141 theorem zero_space_scalar_eq [Subsingleton V] (a b : Kˣ) :
142     scalarHom (V := V) a = scalarHom (V := V) b := zero_space_operator_eq _ _
143 
144 /-- In particular, complex scalar extraction cannot be unique on a zero space. -/
145 theorem zero_space_complex_not_injective [Module ℂ V] [Subsingleton V] :
146     ¬Function.Injective (scalarHom (K := ℂ) (V := V)) := by
147   intro h
148   have he : (1 : ℂˣ) = -1 := h (zero_space_scalar_eq 1 (-1))
149   have hc := congrArg (fun c : ℂˣ => (c : ℂ)) he
150   norm_num at hc
151 
152 end PaperXI.ScalarHolonomy

Back to source controls