HomomorphismObstruction.lean

1 import RealizationBoundaries.SelectorClassification
2 
3 /-!
4 # The torsion-image obstruction for arbitrary group homomorphisms
5 
6 This block obtains the structural obstruction directly from root preservation.
7 It does not presuppose the still-separate full diagonal homomorphism formula.
8 -/
9 set_option autoImplicit false
10 set_option backward.isDefEq.respectTransparency false
11 noncomputable section
12 namespace RealizationBoundaries
13 
14 /-- Monograph Corollary 7.6: selectors with infinitely many disagreements force
15 all images of any additive homomorphism to belong to the actual subgroup D. -/
16 theorem hom_image_finiteSupport (a b : ℕ → Bool)
17     (h : {n : ℕ | a n ≠ b n}.Infinite) (f : pairedGroup a →+ pairedGroup b)
18     (x : pairedGroup a) : (f x).val ∈ finiteSupport := by
19   by_contra hx
20   exact h (finite_disagreement_of_nontorsion_image a b f x hx)
21 
22 /-- The obstruction is expressed intrinsically as an actual positive annihilator
23 for every image element, not merely as a coordinate-support assertion. -/
24 theorem hom_image_torsion (a b : ℕ → Bool)
25     (h : {n : ℕ | a n ≠ b n}.Infinite) (f : pairedGroup a →+ pairedGroup b)
26     (x : pairedGroup a) : ∃ m : ℕ, 0 < m ∧ m • f x = 0 :=
27   (preimage_torsion_iff (selectorLine (pairedSelector b)) (f x)).mpr
28     (hom_image_finiteSupport a b h f x)
29 
30 /-- Canonical factorization of every such homomorphism through D. -/
31 def torsionFactor (a b : ℕ → Bool) (h : {n : ℕ | a n ≠ b n}.Infinite)
32     (f : pairedGroup a →+ pairedGroup b) : pairedGroup a →+ finiteSupport where
33   toFun x := ⟨(f x).val, hom_image_finiteSupport a b h f x⟩
34   map_zero' := by
35     apply Subtype.ext
36     exact congrArg (fun y : pairedGroup b => y.val) (map_zero f)
37   map_add' x y := by
38     apply Subtype.ext
39     exact congrArg (fun z : pairedGroup b => z.val) (map_add f x y)
40 
41 @[simp] theorem torsionFactor_val (a b : ℕ → Bool)
42     (h : {n : ℕ | a n ≠ b n}.Infinite) (f : pairedGroup a →+ pairedGroup b)
43     (x : pairedGroup a) : (torsionFactor a b h f x).val = (f x).val := rfl
44 
45 /-- The factorization commutes with the original embeddings in the prime product. -/
46 theorem torsionFactor_commutes (a b : ℕ → Bool)
47     (h : {n : ℕ | a n ≠ b n}.Infinite) (f : pairedGroup a →+ pairedGroup b) :
48     finiteSupport.subtype.comp (torsionFactor a b h f) = (pairedGroup b).subtype.comp f := rfl
49 
50 /-- There is no freedom in the D-valued factor once the original map is fixed. -/
51 theorem torsionFactor_unique (a b : ℕ → Bool)
52     (h : {n : ℕ | a n ≠ b n}.Infinite) (f : pairedGroup a →+ pairedGroup b)
53     (g : pairedGroup a →+ finiteSupport)
54     (hg : finiteSupport.subtype.comp g = (pairedGroup b).subtype.comp f) :
55     g = torsionFactor a b h f := by
56   apply AddMonoidHom.ext
57   intro x
58   apply Subtype.ext
59   exact DFunLike.congr_fun hg x
60 
61 /-- Infinite selector disagreement forbids embeddings of the original groups. -/
62 theorem no_injective_hom_of_infinite_disagreement (a b : ℕ → Bool)
63     (h : {n : ℕ | a n ≠ b n}.Infinite) (f : pairedGroup a →+ pairedGroup b) :
64     ¬ Function.Injective f := by
65   intro hi
66   let x : pairedGroup a := markedElement (pairedSelector a)
67   have hx : x.val ∉ finiteSupport := markedElement_not_finiteSupport (pairedSelector_infinite a)
68   obtain ⟨m, hm, hmx⟩ := hom_image_torsion a b h f x
69   have he : m • x = 0 := hi (by simpa only [map_nsmul, map_zero] using hmx)
70   exact hx ((preimage_torsion_iff (selectorLine (pairedSelector a)) x).mp ⟨m, hm, he⟩)
71 
72 /-- Infinite selector disagreement also forbids surjections. -/
73 theorem no_surjective_hom_of_infinite_disagreement (a b : ℕ → Bool)
74     (h : {n : ℕ | a n ≠ b n}.Infinite) (f : pairedGroup a →+ pairedGroup b) :
75     ¬ Function.Surjective f := by
76   intro hs
77   let y : pairedGroup b := markedElement (pairedSelector b)
78   have hy : y.val ∉ finiteSupport := markedElement_not_finiteSupport (pairedSelector_infinite b)
79   obtain ⟨x, hx⟩ := hs y
80   apply hy
81   rw [← hx]
82   exact hom_image_finiteSupport a b h f x
83 
84 /-- For this family embeddings, surjections and isomorphisms have the same existence criterion. -/
85 theorem pairedGroup_embeds_iff (a b : ℕ → Bool) :
86     (∃ f : pairedGroup a →+ pairedGroup b, Function.Injective f) ↔
87       {n : ℕ | a n ≠ b n}.Finite := by
88   constructor
89   · rintro ⟨f, hf⟩
90     by_contra h
91     exact no_injective_hom_of_infinite_disagreement a b h f hf
92   · intro h
93     exact ⟨(pairedEquivOfFiniteDisagreement a b h).toAddMonoidHom,
94       (pairedEquivOfFiniteDisagreement a b h).injective⟩
95 
96 theorem pairedGroup_surjects_iff (a b : ℕ → Bool) :
97     (∃ f : pairedGroup a →+ pairedGroup b, Function.Surjective f) ↔
98       {n : ℕ | a n ≠ b n}.Finite := by
99   constructor
100   · rintro ⟨f, hf⟩
101     by_contra h
102     exact no_surjective_hom_of_infinite_disagreement a b h f hf
103   · intro h
104     exact ⟨(pairedEquivOfFiniteDisagreement a b h).toAddMonoidHom,
105       (pairedEquivOfFiniteDisagreement a b h).surjective⟩
106 
107 end RealizationBoundaries

Back to source controls