TraceDiscrepancy.lean

1 import PaperXI.CharacterGenerators
2 import Mathlib.LinearAlgebra.Trace
3 
4 /-! A checked normalization route from actual operator traces to discrepancy.
5 Nonzero normalizing traces are essential and are retained in every cancellation. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TraceDiscrepancy
9 
10 variable {K V W : Type*} [Field K]
11 variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
12 
13 /-- Scalar intertwining is a scalar conjugacy identity of the actual operators. -/
14 theorem conjugate_eq (U : V ≃ₗ[K] W) (R : Module.End K V) (T : Module.End K W)
15     (d : K) (h : ∀ x, U (R x) = d • T (U x)) : U.conj R = d • T := by
16   ext y
17   simpa using h (U.symm y)
18 
19 /-- Trace covariance is derived from scalar conjugacy, not assumed as a phase identity. -/
20 theorem trace_eq (U : V ≃ₗ[K] W) (R : Module.End K V) (T : Module.End K W)
21     (d : K) (h : ∀ x, U (R x) = d • T (U x)) :
22     LinearMap.trace K V R = d * LinearMap.trace K W T := by
23   rw [← LinearMap.trace_conj' R U, conjugate_eq U R T d h, map_smul, smul_eq_mul]
24 
25 /-- Equality of nonzero actual traces forces a scalar discrepancy to be one. -/
26 theorem scalar_eq_one (U : V ≃ₗ[K] W) (R : Module.End K V) (T : Module.End K W)
27     (d : K) (h : ∀ x, U (R x) = d • T (U x))
28     (ht : LinearMap.trace K V R = LinearMap.trace K W T)
29     (hne : LinearMap.trace K W T ≠ 0) : d = 1 := by
30   have hd := trace_eq U R T d h
31   rw [ht] at hd
32   exact (mul_right_cancel₀ hne (hd.symm.trans (one_mul _).symm))
33 
34 /-- A shared nonzero normalization preserves the actual trace ratio. -/
35 theorem normalized_trace_eq (U : V ≃ₗ[K] W) (R : Module.End K V)
36     (T : Module.End K W) (d n : K) (h : ∀ x, U (R x) = d • T (U x)) :
37     LinearMap.trace K V R / n = d * (LinearMap.trace K W T / n) := by
38   rw [trace_eq U R T d h]
39   ring
40 
41 theorem scalar_eq_one_of_normalized (U : V ≃ₗ[K] W) (R : Module.End K V)
42     (T : Module.End K W) (d n : K) (hn : n ≠ 0)
43     (h : ∀ x, U (R x) = d • T (U x))
44     (ht : LinearMap.trace K V R / n = LinearMap.trace K W T / n)
45     (hne : LinearMap.trace K W T ≠ 0) : d = 1 := by
46   exact scalar_eq_one U R T d h ((div_left_inj' hn).mp ht) hne
47 
48 variable {C : Type*} [Group C]
49 
50 /-- A discrepancy character with equal nonzero generator traces is trivial. -/
51 theorem character_trivial (U : V ≃ₗ[K] W)
52     (R : Representation K C V) (T : Representation K C W) (δ : C →* Kˣ)
53     (hδ : ∀ g x, U (R g x) = (δ g : K) • T g (U x))
54     (S : Set C) (hgen : Subgroup.closure S = ⊤)
55     (htrace : ∀ g ∈ S, LinearMap.trace K V (R g) = LinearMap.trace K W (T g))
56     (hne : ∀ g ∈ S, LinearMap.trace K W (T g) ≠ 0) : ∀ g, δ g = 1 := by
57   apply CharacterGenerators.trivial δ S hgen
58   intro g hg
59   apply Units.ext
60   exact scalar_eq_one U (R g) (T g) (δ g : K) (hδ g) (htrace g hg) (hne g hg)
61 
62 /-- The scalar cancellation fails when both traces vanish. -/
63 theorem zero_trace_cannot_detect_scalar (d : K) : (0 : K) = d * 0 := by simp
64 
65 /-- Complete closure by trace phases, with the actual lift-covariance and
66 nonzero normalizer hypotheses exposed. -/
67 theorem bridge_from_traces {H : Type*} [Group H]
68     [Module ℂ V] [Module ℂ W] [FiniteDimensional ℂ V]
69     (ρ : Representation ℂ H V) [Representation.IsIrreducible ρ]
70     (σ : Representation ℂ H W) (U : V ≃ₗ[ℂ] W)
71     (hU : ∀ h x, U (ρ h x) = σ h (U x))
72     (α : C →* MulAut H) (R : Representation ℂ C V) (T : Representation ℂ C W)
73     (hR : ∀ g h x, R g (ρ h x) = ρ (α g h) (R g x))
74     (hT : ∀ g h x, T g (σ h x) = σ (α g h) (T g x))
75     (S : Set C) (hgen : Subgroup.closure S = ⊤)
76     (htrace : ∀ g ∈ S, LinearMap.trace ℂ V (R g) = LinearMap.trace ℂ W (T g))
77     (hne : ∀ g ∈ S, LinearMap.trace ℂ W (T g) ≠ 0) :
78     ∀ a x, U (CyclicBridge.semidirectRepresentation α ρ R hR a x) =
79       CyclicBridge.semidirectRepresentation α σ T hT a (U x) := by
80   obtain ⟨δ, hδ, hclose⟩ := CharacterGenerators.bridge_from_actions
81     ρ σ U hU α R T hR hT S hgen
82   exact hclose (fun g _ => character_trivial U R T δ hδ S hgen htrace hne g)
83 
84 end PaperXI.TraceDiscrepancy

Back to source controls