Extensions.lean

1 import RealizationBoundaries.Preimages
2 
3 /-! # Exact rational quotients and nonsplitting inside the actual ambient product -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace RealizationBoundaries
7 
8 /-- Any homomorphism from a divisible additive group into the prime product is zero.
9 No linearity or continuity of the homomorphism is assumed. -/
10 theorem hom_zero_of_divisible (E : Type*) [AddGroup E]
11     (hdiv : ∀ m : ℕ, 0 < m → ∀ x : E, ∃ y : E, m • y = x)
12     (f : E →+ Ambient) : f = 0 := by
13   ext x p
14   obtain ⟨y, hy⟩ := hdiv p.val p.property.pos x
15   rw [← hy, map_nsmul]
16   change (p.val • f y) p = 0
17   rw [coordinate_nsmul]
18   simp
19 
20 /-- The ambient product has no embedded nonzero divisible group. -/
21 theorem not_injective_hom_of_divisible (E : Type*) [AddGroup E] [Nontrivial E]
22     (hdiv : ∀ m : ℕ, 0 < m → ∀ x : E, ∃ y : E, m • y = x)
23     (f : E →+ Ambient) : ¬ Function.Injective f := by
24   intro hf
25   have hzero := hom_zero_of_divisible E hdiv f
26   obtain ⟨x, hx⟩ := exists_ne (0 : E)
27   apply hx
28   apply hf
29   simp [hzero]
30 
31 theorem rational_hom_zero (E : Type*) [AddCommGroup E] [Module ℚ E]
32     (f : E →+ Ambient) : f = 0 := by
33   apply hom_zero_of_divisible E _ f
34   intro m hm x
35   refine ⟨(m : ℚ)⁻¹ • x, ?_⟩
36   rw [← Nat.cast_smul_eq_nsmul ℚ, smul_smul]
37   simp [Nat.ne_of_gt hm]
38 
39 /-- Restriction of the actual quotient map to the selected rational subspace. -/
40 def preimageProjection (W : Submodule ℚ TailSpace) : preimage W →+ W where
41   toFun x := ⟨quotientMap x.val, x.property⟩
42   map_zero' := Subtype.ext (map_zero quotientMap)
43   map_add' x y := Subtype.ext (map_add quotientMap x.val y.val)
44 
45 theorem preimageProjection_surjective (W : Submodule ℚ TailSpace) :
46     Function.Surjective (preimageProjection W) := by
47   intro w
48   obtain ⟨x, hx⟩ := quotientMap_surjective w.val
49   refine ⟨⟨x, ?_⟩, Subtype.ext hx⟩
50   change quotientMap x ∈ W
51   rw [hx]
52   exact w.property
53 
54 /-- The finite-support kernel, as a subgroup of the original preimage group. -/
55 def finiteKernel (W : Submodule ℚ TailSpace) : AddSubgroup (preimage W) :=
56   finiteSupport.comap (preimage W).subtype
57 
58 theorem preimageProjection_ker (W : Submodule ℚ TailSpace) :
59     (preimageProjection W).ker = finiteKernel W := by
60   ext x
61   change (⟨quotientMap x.val, x.property⟩ : W) = 0 ↔ x.val ∈ finiteSupport
62   rw [Subtype.ext_iff]
63   exact quotientMap_eq_zero_iff x.val
64 
65 /-- The quotient by the actual finite-support subgroup is the selected rational subspace. -/
66 def preimageQuotientEquiv (W : Submodule ℚ TailSpace) :
67     (preimage W ⧸ finiteKernel W) ≃+ W :=
68   (QuotientAddGroup.quotientAddEquivOfEq (preimageProjection_ker W).symm).trans
69     (QuotientAddGroup.quotientKerEquivOfSurjective (preimageProjection W)
70       (preimageProjection_surjective W))
71 
72 /-- No homomorphic section exists when the rational quotient contains a nonzero point. -/
73 theorem no_section (W : Submodule ℚ TailSpace) (w : W) (hw : w ≠ 0)
74     (s : W →+ preimage W) : (preimageProjection W).comp s ≠ AddMonoidHom.id W := by
75   intro hs
76   have hz : (preimage W).subtype.comp s = 0 :=
77     rational_hom_zero W ((preimage W).subtype.comp s)
78   have hsw : s w = 0 := by
79     apply Subtype.ext
80     exact DFunLike.congr_fun hz w
81   have h := DFunLike.congr_fun hs w
82   apply hw
83   simpa [hsw] using h.symm
84 
85 /-- A nonsplitting statement with no selected witness in its public hypotheses. -/
86 theorem no_section_of_nontrivial (W : Submodule ℚ TailSpace) [Nontrivial W] :
87     ¬ ∃ s : W →+ preimage W, (preimageProjection W).comp s = AddMonoidHom.id W := by
88   obtain ⟨w, hw⟩ := exists_ne (0 : W)
89   rintro ⟨s, hs⟩
90   exact no_section W w hw s hs
91 
92 end RealizationBoundaries

Back to source controls