DirectSumPresentation.lean

1 import RealizationBoundaries.SubgroupSpectrum
2 import RealizationBoundaries.SpectrumComputability
3 import Mathlib.Algebra.DirectSum.Basic
4 import Mathlib.Data.ZMod.QuotientGroup
5 
6 /-! # The actual direct sum has precisely the commuting prime-order presentation -/
7 set_option autoImplicit false
8 noncomputable section
9 open scoped BigOperators
10 namespace RealizationBoundaries
11 
12 /-- The actual finite-support subgroup, identified with the genuine dependent direct sum. -/
13 def finiteSupportDirectSumEquiv : finiteSupport ≃+ (Π₀ p : Prime, Coordinate p) where
14   toFun := finiteSupportCode
15   invFun f := ⟨f, DFinsupp.finite_support f⟩
16   left_inv x := Subtype.ext rfl
17   right_inv f := by ext p; rfl
18   map_add' x y := by ext p; rfl
19 
20 /-- The original ambient prime seed is the actual direct-sum coordinate generator. -/
21 theorem finiteSupportDirectSumEquiv_primeSeed (p : Prime) :
22     finiteSupportDirectSumEquiv (primeSeed p) = DFinsupp.single p 1 := by
23   classical
24   ext q
25   by_cases hqp : q = p
26   · subst q
27     simp [finiteSupportDirectSumEquiv, primeSeed, cut]
28   · simp [finiteSupportDirectSumEquiv, primeSeed, cut, hqp, Ne.symm hqp]
29 
30 /-- Each standard generator satisfies its stated prime-order relation. -/
31 theorem primeSeed_prime_order_relation (p : Prime) : p.val • primeSeed p = 0 := by
32   apply Subtype.ext
33   funext q
34   by_cases hqp : q = p
35   · subst q
36     simp [primeSeed, cut]
37   · simp [primeSeed, cut, hqp]
38 
39 /-- A proposed generator killed by p induces a unique homomorphism out of C_p. -/
40 def coordinatePresentationHom (E : Type*) [AddCommGroup E] (g : Prime → E)
41     (hg : ∀ p : Prime, p.val • g p = 0) (p : Prime) : Coordinate p →+ E :=
42   ZMod.lift p.val ⟨zmultiplesHom E (g p), by
43     simpa only [zmultiplesHom_apply, natCast_zsmul] using hg p⟩
44 
45 @[simp] theorem coordinatePresentationHom_one (E : Type*) [AddCommGroup E]
46     (g : Prime → E) (hg : ∀ p : Prime, p.val • g p = 0) (p : Prime) :
47     coordinatePresentationHom E g hg p 1 = g p := by
48   unfold coordinatePresentationHom
49   rw [← Int.cast_one, ZMod.lift_coe]
50   simp only [zmultiplesHom_apply, one_zsmul]
51 
52 /-- The full homomorphism induced by any commuting prime-order generator assignment. -/
53 def directSumPresentationHom (E : Type*) [AddCommGroup E] (g : Prime → E)
54     (hg : ∀ p : Prime, p.val • g p = 0) : finiteSupport →+ E :=
55   (DirectSum.toAddMonoid (coordinatePresentationHom E g hg)).comp
56     finiteSupportDirectSumEquiv.toAddMonoidHom
57 
58 @[simp] theorem directSumPresentationHom_primeSeed (E : Type*) [AddCommGroup E]
59     (g : Prime → E) (hg : ∀ p : Prime, p.val • g p = 0) (p : Prime) :
60     directSumPresentationHom E g hg (primeSeed p) = g p := by
61   change DirectSum.toAddMonoid (coordinatePresentationHom E g hg)
62     (finiteSupportDirectSumEquiv (primeSeed p)) = g p
63   rw [finiteSupportDirectSumEquiv_primeSeed]
64   exact (DirectSum.toAddMonoid_of _ p 1).trans (coordinatePresentationHom_one E g hg p)
65 
66 /-- Equality on the actual prime generators determines every homomorphism. -/
67 theorem finiteSupport_hom_ext_primeSeed (E : Type*) [AddCommGroup E]
68     (f h : finiteSupport →+ E) (he : ∀ p : Prime, f (primeSeed p) = h (primeSeed p)) :
69     f = h := by
70   ext x
71   rw [finiteSupport_primeSeed_decomposition x]
72   simp only [map_sum, map_nsmul, he]
73 
74 /-- Universal presentation by commuting generators e_p and only the relations p e_p = 0.
75 The target commutativity is part of the presentation category. -/
76 theorem finiteSupport_prime_order_presentation (E : Type*) [AddCommGroup E]
77     (g : Prime → E) (hg : ∀ p : Prime, p.val • g p = 0) :
78     ∃! f : finiteSupport →+ E, ∀ p : Prime, f (primeSeed p) = g p := by
79   refine ⟨directSumPresentationHom E g hg, directSumPresentationHom_primeSeed E g hg, ?_⟩
80   intro f hf
81   apply finiteSupport_hom_ext_primeSeed E
82   intro p
83   exact (hf p).trans (directSumPresentationHom_primeSeed E g hg p).symm
84 
85 /-- The map from the standard presentation to the actual halting-spectrum group. -/
86 def directSumToHaltingGroup : finiteSupport →+ spectrumSubgroup haltingPrimeSpectrum :=
87   haltingRelatorQuotientEquiv.toAddMonoidHom.comp
88     (QuotientAddGroup.mk' (AddSubgroup.closure haltingSeedRelators))
89 
90 theorem directSumToHaltingGroup_surjective : Function.Surjective directSumToHaltingGroup :=
91   haltingRelatorQuotientEquiv.surjective.comp (QuotientAddGroup.mk'_surjective _)
92 
93 /-- The original generator labels, interpreted in the actual quotient group. -/
94 def haltingPresentedGenerator (p : Prime) : spectrumSubgroup haltingPrimeSpectrum :=
95   directSumToHaltingGroup (primeSeed p)
96 
97 /-- A valid generator assignment kills every actual extra halting relator. -/
98 theorem directSumPresentationHom_kills_halting_relators (E : Type*) [AddCommGroup E]
99     (g : Prime → E) (hg : ∀ p : Prime, p.val • g p = 0)
100     (hk : ∀ n : ℕ, diagonalHalting n → g (primeAt (2*n+1)) = 0) :
101     AddSubgroup.closure haltingSeedRelators ≤ (directSumPresentationHom E g hg).ker := by
102   apply (AddSubgroup.closure_le _).mpr
103   rintro _ ⟨n, hn, rfl⟩
104   change directSumPresentationHom E g hg (primeSeed (primeAt (2*n+1))) = 0
105   rw [directSumPresentationHom_primeSeed]
106   exact hk n hn
107 
108 /-- The actual homomorphism induced on H by all of the printed relators. -/
109 def haltingGroupPresentationHom (E : Type*) [AddCommGroup E]
110     (g : Prime → E) (hg : ∀ p : Prime, p.val • g p = 0)
111     (hk : ∀ n : ℕ, diagonalHalting n → g (primeAt (2*n+1)) = 0) :
112     spectrumSubgroup haltingPrimeSpectrum →+ E :=
113   (QuotientAddGroup.lift (AddSubgroup.closure haltingSeedRelators)
114     (directSumPresentationHom E g hg)
115     (directSumPresentationHom_kills_halting_relators E g hg hk)).comp
116       haltingRelatorQuotientEquiv.symm.toAddMonoidHom
117 
118 @[simp] theorem haltingGroupPresentationHom_generator (E : Type*) [AddCommGroup E]
119     (g : Prime → E) (hg : ∀ p : Prime, p.val • g p = 0)
120     (hk : ∀ n : ℕ, diagonalHalting n → g (primeAt (2*n+1)) = 0) (p : Prime) :
121     haltingGroupPresentationHom E g hg hk (haltingPresentedGenerator p) = g p := by
122   simp [haltingGroupPresentationHom, haltingPresentedGenerator, directSumToHaltingGroup]
123 
124 /-- Full generators-and-relators universal property for the actual halting group.
125 The generators commute, each e_p has relation p e_p = 0, and the only extra
126 relations are e_(2n+1) = 0 when program n halts on n. -/
127 theorem haltingGroup_prime_order_presentation (E : Type*) [AddCommGroup E]
128     (g : Prime → E) (hg : ∀ p : Prime, p.val • g p = 0)
129     (hk : ∀ n : ℕ, diagonalHalting n → g (primeAt (2*n+1)) = 0) :
130     ∃! f : spectrumSubgroup haltingPrimeSpectrum →+ E,
131       ∀ p : Prime, f (haltingPresentedGenerator p) = g p := by
132   refine ⟨haltingGroupPresentationHom E g hg hk,
133     haltingGroupPresentationHom_generator E g hg hk, ?_⟩
134   intro f hf
135   have he : f.comp directSumToHaltingGroup =
136       (haltingGroupPresentationHom E g hg hk).comp directSumToHaltingGroup := by
137     apply finiteSupport_hom_ext_primeSeed E
138     intro p
139     change f (haltingPresentedGenerator p) =
140       haltingGroupPresentationHom E g hg hk (haltingPresentedGenerator p)
141     rw [hf p, haltingGroupPresentationHom_generator]
142   ext y
143   obtain ⟨x, rfl⟩ := directSumToHaltingGroup_surjective y
144   exact DFunLike.congr_fun he x
145 
146 /-- The standard prime-order relator labels themselves form a total ordinary
147 computable list, using the production prime enumeration. -/
148 def primeOrderRelatorLabel (n : ℕ) : ℕ × ℕ := (n, (primeAt n).val)
149 
150 theorem computable_primeOrderRelatorLabel : Computable primeOrderRelatorLabel :=
151   Computable.id.pair computable_primeAt_value
152 
153 end RealizationBoundaries

Back to source controls