SeedGeneration.lean

1 import RealizationBoundaries.DirectSumEndomorphisms
2 
3 /-!
4 # Endomorphism hulls and closed coordinate obstructions
5 
6 The hull is generated by the images of the actual seeds under all actual additive
7 endomorphisms. Finite compositions require no extra rule because endomorphisms
8 already contain the identity and are closed under composition. The closure below
9 is taken in the supplied topology, not in the completion of the group.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace RealizationBoundaries
14 
15 universe u
16 variable {G : Type u} [AddGroup G]
17 
18 /-- All endomorphism images of the given seeds. -/
19 def endomorphismOrbit (S : Set G) : Set G :=
20   {x | ∃ f : AddMonoid.End G, ∃ s ∈ S, f s = x}
21 
22 /-- Algebraic generation with the entire endomorphism ring admitted. -/
23 def endomorphismHull (S : Set G) : AddSubgroup G :=
24   AddSubgroup.closure (endomorphismOrbit S)
25 
26 theorem seed_mem_endomorphismHull {S : Set G} {s : G} (hs : s ∈ S) :
27     s ∈ endomorphismHull S :=
28   AddSubgroup.subset_closure ⟨AddMonoidHom.id G, s, hs, rfl⟩
29 
30 theorem orbit_mem_endomorphismHull (S : Set G) (f : AddMonoid.End G)
31     {s : G} (hs : s ∈ S) : f s ∈ endomorphismHull S :=
32   AddSubgroup.subset_closure ⟨f, s, hs, rfl⟩
33 
34 /-- Universal property: an invariant subgroup containing the seeds contains their hull. -/
35 theorem endomorphismHull_le {S : Set G} {H : AddSubgroup G}
36     (hS : S ⊆ H) (hH : ∀ f : AddMonoid.End G, ∀ x ∈ H, f x ∈ H) :
37     endomorphismHull S ≤ H := by
38   apply (AddSubgroup.closure_le _).mpr
39   rintro x ⟨f, s, hs, rfl⟩
40   exact hH f s (hS hs)
41 
42 /-- The defined hull is itself invariant under every endomorphism. -/
43 theorem endomorphismHull_invariant (S : Set G) (f : AddMonoid.End G)
44     {x : G} (hx : x ∈ endomorphismHull S) : f x ∈ endomorphismHull S := by
45   have h : endomorphismHull S ≤ (endomorphismHull S).comap f := by
46     apply (AddSubgroup.closure_le _).mpr
47     rintro z ⟨g, s, hs, rfl⟩
48     exact orbit_mem_endomorphismHull S (f.comp g) hs
49   exact h hx
50 
51 @[simp] theorem endomorphismHull_univ : endomorphismHull (Set.univ : Set G) = ⊤ := by
52   apply top_unique
53   intro x _
54   exact seed_mem_endomorphismHull (Set.mem_univ x)
55 
56 @[simp] theorem endomorphismHull_empty : endomorphismHull (∅ : Set G) = ⊥ := by
57   apply le_antisymm _ bot_le
58   apply (AddSubgroup.closure_le _).mpr
59   rintro x ⟨f, s, hs, _⟩
60   exact False.elim hs
61 
62 /-- Topological operator generation inside the original group. -/
63 def topologicalEndomorphismHull [TopologicalSpace G] [IsTopologicalAddGroup G]
64     (S : Set G) : AddSubgroup G := (endomorphismHull S).topologicalClosure
65 
66 /-- A closed invariant subgroup remains an obstruction after topological closure. -/
67 theorem topologicalEndomorphismHull_le [TopologicalSpace G] [IsTopologicalAddGroup G]
68     {S : Set G} {H : AddSubgroup G} (hH : IsClosed (H : Set G))
69     (h : endomorphismHull S ≤ H) : topologicalEndomorphismHull S ≤ H := by
70   exact closure_minimal h hH
71 
72 /-- The exact coordinate-zero subgroup inside a given ambient subgroup. -/
73 def coordinateKernel (H : AddSubgroup Ambient) (p : Prime) : AddSubgroup H where
74   carrier := {x | x.val p = 0}
75   zero_mem' := rfl
76   add_mem' := by intro x y hx hy; change x.val p + y.val p = 0; rw [hx, hy, add_zero]
77   neg_mem' := by intro x hx; change -x.val p = 0; rw [hx, neg_zero]
78 
79 @[simp] theorem mem_coordinateKernel (H : AddSubgroup Ambient) (p : Prime) (x : H) :
80     x ∈ coordinateKernel H p ↔ x.val p = 0 := Iff.rfl
81 
82 theorem coordinateKernel_closed (H : AddSubgroup Ambient) (p : Prime) :
83     IsClosed (coordinateKernel H p : Set H) :=
84   isClosed_eq ((continuous_apply p).comp continuous_subtype_val) continuous_const
85 
86 /-- One omitted coordinate obstructs both algebraic and topological generation. -/
87 theorem coordinate_obstruction (H : AddSubgroup Ambient) (p : Prime) (S : Set H)
88     (hS : ∀ s ∈ S, s.val p = 0)
89     (hpres : ∀ f : AddMonoid.End H, ∀ x : H, x.val p = 0 → (f x).val p = 0) :
90     endomorphismHull S ≤ coordinateKernel H p ∧
91       topologicalEndomorphismHull S ≤ coordinateKernel H p := by
92   have h : endomorphismHull S ≤ coordinateKernel H p :=
93     endomorphismHull_le hS hpres
94   exact ⟨h, topologicalEndomorphismHull_le (coordinateKernel_closed H p) h⟩
95 
96 /-- The nonzero prime seed witnesses that this is a proper closed kernel. -/
97 theorem coordinateKernel_ne_top (H : AddSubgroup Ambient) (hD : finiteSupport ≤ H)
98     (p : Prime) : coordinateKernel H p ≠ ⊤ := by
99   classical
100   intro h
101   let e : H := ⟨(primeSeed p).val, hD (primeSeed p).property⟩
102   have he : e ∈ coordinateKernel H p := h.symm ▸ AddSubgroup.mem_top e
103   have h0 : (primeSeed p).val p = 0 := he
104   simp [primeSeed, cut] at h0
105 
106 end RealizationBoundaries

Back to source controls