PacketCorners.lean

1 import PaperIRelease.PacketDescent
2 import PaperIRelease.AlgebraTransfer
3 import KomorebiVerification.SeedRankOperations
4 
5 set_option autoImplicit false
6 set_option linter.unnecessarySimpa false
7 noncomputable section
8 
9 namespace Komorebi.PaperIRelease
10 
11 open Komorebi.Foundation
12 
13 universe u
14 variable {𝕜 X : Type u} [Field 𝕜] [AddCommGroup X] [Module 𝕜 X]
15 
16 /-- Compress an ambient operator to the actual range of an idempotent.
17 On a range vector this is the literal action `e T e`, because `e x = x`. -/
18 def cornerCompression (e : Module.End 𝕜 X) (T : Module.End 𝕜 X) :
19     Module.End 𝕜 (LinearMap.range e) where
20   toFun x := ⟨e (T x), ⟨T x, rfl⟩⟩
21   map_add' x y := Subtype.ext (by simp)
22   map_smul' a x := Subtype.ext (by simp)
23 
24 theorem idempotent_range_fixed (e : Module.End 𝕜 X)
25     (he : ∀ x, e (e x) = e x) (x : LinearMap.range e) : e (x : X) = x := by
26   obtain ⟨y, hy⟩ := x.property
27   rw [← hy]
28   exact he y
29 
30 /-- The genuine unital corner acting on `range(e)`. The identity here is the
31 restriction of `e`, rather than the ambient identity on unrelated packets. -/
32 def packetCornerAlgebra (A : Subalgebra 𝕜 (Module.End 𝕜 X))
33     (e : Module.End 𝕜 X) (heA : e ∈ A) (he : ∀ x, e (e x) = e x) :
34     Subalgebra 𝕜 (Module.End 𝕜 (LinearMap.range e)) where
35   carrier := {T | ∃ a ∈ A, cornerCompression e a = T}
36   zero_mem' := ⟨0, A.zero_mem, by ext x; simp [cornerCompression]⟩
37   add_mem' := by
38     rintro T U ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
39     exact ⟨a + b, A.add_mem ha hb, by ext x; simp [cornerCompression]⟩
40   mul_mem' := by
41     rintro T U ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
42     exact ⟨a * e * b, A.mul_mem (A.mul_mem ha heA) hb, rfl⟩
43   algebraMap_mem' a := by
44     refine ⟨algebraMap 𝕜 (Module.End 𝕜 X) a, A.algebraMap_mem a, ?_⟩
45     ext x
46     change e (a • (x : X)) = a • (x : X)
47     rw [map_smul, idempotent_range_fixed e he x]
48 
49 /-- Every corner action is an actual action by an element of the ambient
50 algebra. The representing ambient element can be chosen independently of x. -/
51 theorem corner_action_ambient
52     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (e : Module.End 𝕜 X)
53     (heA : e ∈ A) (he : ∀ x, e (e x) = e x)
54     (T : packetCornerAlgebra A e heA he) :
55     ∃ a : A, ∀ x : LinearMap.range e, (T • x : LinearMap.range e).val = a • (x : X) := by
56   obtain ⟨a, ha, hT⟩ := T.property
57   refine ⟨⟨e * a, A.mul_mem heA ha⟩, ?_⟩
58   intro x
59   change (T.val x : X) = e (a (x : X))
60   rw [← hT]
61   rfl
62 
63 /-- The unital corner identity acts as the original projector on its range. -/
64 theorem corner_one_eq_projector
65     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (e : Module.End 𝕜 X)
66     (heA : e ∈ A) (he : ∀ x, e (e x) = e x) (x : LinearMap.range e) :
67     ((1 : packetCornerAlgebra A e heA he) • x : LinearMap.range e).val = e (x : X) := by
68   rw [one_smul, idempotent_range_fixed e he x]
69 
70 end Komorebi.PaperIRelease

Back to source controls