PacketPureBoundaryTests.lean

1 import PaperIRelease.PacketSourceRank
2 
3 set_option autoImplicit false
4 noncomputable section
5 
6 namespace Komorebi.PaperIRelease.PureBoundaryTests
7 
8 open Cardinal Set Komorebi.Foundation Komorebi.SeedRankBasics
9 open Komorebi.PacketNaturalityCompletion.Reachability
10 open FiniteDigraph
11 
12 universe u
13 variable {𝕜 X I : Type u} [Field 𝕜] [AddCommGroup X] [Module 𝕜 X] [Fintype I]
14 
15 /-- With at most one packet all vectors are pure, so the constrained minimum
16 is exactly the original cardinal-valued seed rank. -/
17 theorem singleton_packet_rank [Subsingleton I]
18     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I) :
19     packetPureSeedRank A P = seedRank A X := by
20   apply le_antisymm
21   · obtain ⟨S, hS, hc⟩ := exists_generating_set_card_eq_seedRank A X
22     rw [← hc]
23     exact packetPureSeedRank_le_card ⟨hS, fun _ _ _ _ _ _ ↦ Subsingleton.elim _ _⟩
24   · exact seedRank_le_packetPureSeedRank A P
25 
26 /-- On the zero module the minimum is zero, even when indices exist and
27 every projector is zero. -/
28 theorem zero_module_rank [Subsingleton X]
29     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I) :
30     packetPureSeedRank A P = 0 := by
31   apply le_antisymm
32   · have hgen : PureGenerates A P (∅ : Set X) := by
33       refine ⟨?_, ?_⟩
34       · rw [Generates, Submodule.span_empty]
35         exact Subsingleton.elim _ _
36       · simp
37     simpa using packetPureSeedRank_le_card hgen
38   · exact zero_le
39 
40 /-- The identity projector on a countably infinite-dimensional rational
41 space. There is deliberately no finite generation hypothesis. -/
42 def infiniteSinglePacket : LinearProjectorFamily ℚ (ℕ →₀ ℚ) Unit where
43   proj _ := LinearMap.id
44   idempotent _ _ := rfl
45   orthogonal hij := (hij (Subsingleton.elim _ _)).elim
46   complete x := by simp
47 
48 theorem infinite_single_packet_rank :
49     packetPureSeedRank (packetGeneratedAlgebra infiniteSinglePacket ∅) infiniteSinglePacket =
50       seedRank (packetGeneratedAlgebra infiniteSinglePacket ∅) (ℕ →₀ ℚ) :=
51   singleton_packet_rank _ _
52 
53 /-- The exact weighted source formula applies unchanged to infinite packet
54 dimensions, and the no-generator edge condition is discharged, not supplied. -/
55 theorem infinite_single_source_formula :
56     packetPureSeedRank (packetGeneratedAlgebra infiniteSinglePacket ∅) infiniteSinglePacket =
57       Cardinal.sum (fun C : Sources (TransferEdge infiniteSinglePacket ∅) ↦
58         localPureSeedRank (packetGeneratedAlgebra infiniteSinglePacket ∅) infiniteSinglePacket
59           (projector_mem_generatedAlgebra infiniteSinglePacket ∅)
60           (component (TransferEdge infiniteSinglePacket ∅)) C.val) := by
61   apply source_component_pureSeedRank
62   rintro a b ⟨T, hT, _⟩
63   exact hT.elim
64 
65 /-- Zero deletion preserves the constrained cardinal minimum, including the
66 case of an entirely zero local packet system. -/
67 theorem deleted_zero_rank
68     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I) :
69     packetPureSeedRank A P.discardZeros = packetPureSeedRank A P :=
70   packetPureSeedRank_discardZeros A P
71 
72 end Komorebi.PaperIRelease.PureBoundaryTests
73 
74 #print axioms Komorebi.PaperIRelease.PureBoundaryTests.singleton_packet_rank
75 #print axioms Komorebi.PaperIRelease.PureBoundaryTests.zero_module_rank
76 #print axioms Komorebi.PaperIRelease.PureBoundaryTests.infinite_single_source_formula

Back to source controls