CategoryBoundaries.lean

1 import PaperIRelease.CategoryPackets
2 import PaperIRelease.CategoryExport
3 import PaperIRelease.GrammarIdeal
4 import PaperIRelease.GrammarPaths
5 import PaperIRelease.GrammarFactorization
6 import KomorebiVerification.FibreRefinement
7 
8 set_option autoImplicit false
9 set_option linter.unnecessarySimpa false
10 set_option linter.unusedSimpArgs false
11 
12 noncomputable section
13 
14 namespace Komorebi.PaperIRelease.CategoryBoundaries
15 
16 open CategoryPackets GrammarAlgebra
17 
18 /-- Two actual nonzero coordinate packets over Q. -/
19 abbrev twoPackets : PacketObject ℚ where
20   carrier := Fin 2 → ℚ
21   index := Fin 2
22   algebra := ⊤
23   packets := Packet.fibreLinearProjectorFamily id
24   packet_nonzero i hi := by
25     have h := congrArg (fun T : Module.End ℚ (Fin 2 → ℚ) => T (fun _ => 1) i) hi
26     simpa [Packet.fibreLinearProjectorFamily, Packet.fibreLinearProj, Packet.fibreProj] using h
27 
28 /-- The same vector space viewed as one nonzero packet. -/
29 abbrev onePacket : PacketObject ℚ where
30   carrier := Fin 2 → ℚ
31   index := Unit
32   algebra := ⊤
33   packets := Packet.fibreLinearProjectorFamily (fun _ => ())
34   packet_nonzero i hi := by
35     cases i
36     have h := congrArg (fun T : Module.End ℚ (Fin 2 → ℚ) => T (fun _ => 1) 0) hi
37     simpa [Packet.fibreLinearProjectorFamily, Packet.fibreLinearProj, Packet.fibreProj] using h
38 
39 /-- A real label-merging morphism.  Injective-label formalizations cannot instantiate this. -/
40 def mergeTwoPackets : PacketMorphism twoPackets onePacket where
41   linearMap := LinearMap.id
42   algebraMap := AlgHom.id ℚ _
43   packetMap := fun _ => ()
44   operator_natural _ := by simp
45   packet_natural j := by
46     cases j
47     apply LinearMap.ext
48     intro x
49     change x = fiberProjector twoPackets (fun _ => ()) () x
50     rw [fiberProjector_apply twoPackets (fun _ => ()) () x]
51     simp only [↓reduceIte]
52     exact (twoPackets.packets.complete x).symm
53 
54 theorem merge_is_not_injective : ¬ Function.Injective mergeTwoPackets.packetMap := by
55   intro h
56   have hh : (0 : Fin 2) = 1 := h rfl
57   exact (by decide : (0 : Fin 2) ≠ 1) hh
58 
59 theorem merge_block_naturality (T : twoPackets.algebra) :
60     (Foundation.transferBlock onePacket.packets onePacket.packets
61       (mergeTwoPackets.algebraMap T).1 () ()).comp mergeTwoPackets.linearMap =
62       ∑ b, ∑ a, mergeTwoPackets.linearMap.comp
63         (Foundation.transferBlock twoPackets.packets twoPackets.packets T.1 b a) := by
64   simpa [mergeTwoPackets] using transferBlock_naturality mergeTwoPackets T () ()
65 
66 def emptySource : Fin 0 → Fin 0 := Fin.elim0
67 
68 /-- No vertices forces the presented path algebra to be the zero ring. -/
69 theorem empty_vertex_algebra (a : PathAlgebra (K := ℚ) emptySource emptySource) : a = 0 := by
70   have h : (0 : PathAlgebra (K := ℚ) emptySource emptySource) = 1 := by
71     simpa using vertex_complete (freeGrammar (K := ℚ) emptySource emptySource)
72   calc
73     a = a * 1 := (mul_one a).symm
74     _ = a * 0 := congrArg (a * ·) h.symm
75     _ = 0 := mul_zero a
76 
77 end Komorebi.PaperIRelease.CategoryBoundaries
78 
79 #print axioms Komorebi.PaperIRelease.GrammarAlgebra.typedModuleEquivalence
80 #print axioms Komorebi.PaperIRelease.GrammarAlgebra.typedIdealModuleEquivalence
81 #print axioms Komorebi.PaperIRelease.GrammarAlgebra.TypedData.path_action
82 #print axioms Komorebi.PaperIRelease.GrammarAlgebra.CollapsedRealization.seedRank_imageAlgebra_eq
83 #print axioms Komorebi.PaperIRelease.CategoryPackets.transferBlock_naturality
84 #print axioms Komorebi.PaperIRelease.CategoryPackets.seedCategory
85 #print axioms Komorebi.PaperIRelease.CategoryExport.equation_transport

Back to source controls