DiagonalHomomorphisms.lean

1 import RealizationBoundaries.Countability
2 import RealizationBoundaries.TailSignature
3 import RealizationBoundaries.ProductTopology
4 
5 /-!
6 # Diagonality of arbitrary homomorphisms
7 
8 The coefficient at a prime is defined by the image of the actual prime seed.
9 The coordinate formula is derived from prime-root solvability, without assuming
10 continuity, linearity over the product ring, or a prescribed diagonal action.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace RealizationBoundaries
15 
16 /-- The original prime seed regarded as a member of an arbitrary rational preimage. -/
17 def preimageSeed (W : Submodule ℚ TailSpace) (p : Prime) : preimage W :=
18   ⟨(primeSeed p).val, finiteSupport_le_preimage W (primeSeed p).property⟩
19 
20 @[simp] theorem preimageSeed_apply (W : Submodule ℚ TailSpace) (p : Prime) :
21     (preimageSeed W p).val p = 1 := by
22   classical
23   simp [preimageSeed, primeSeed, cut]
24 
25 /-- A homomorphism preserves a zero prime coordinate because it preserves roots. -/
26 theorem hom_preserves_zero_coordinate (U V : Submodule ℚ TailSpace)
27     (f : preimage U →+ preimage V) (x : preimage U) (p : Prime)
28     (hx : x.val p = 0) : (f x).val p = 0 :=
29   (preimage_prime_root_iff V (f x) p).mp
30     (hasPrimeRoot_map f x p ((preimage_prime_root_iff U x p).mpr hx))
31 
32 /-- Coefficients are recovered from the given homomorphism, not chosen as hypotheses. -/
33 def homDiagonal (U V : Submodule ℚ TailSpace) (f : preimage U →+ preimage V) : Ambient :=
34   fun p => (f (preimageSeed U p)).val p
35 
36 /-- Subtract a multiple of one prime seed and use the root criterion on the remainder. -/
37 theorem hom_coordinate_formula (U V : Submodule ℚ TailSpace)
38     (f : preimage U →+ preimage V) (x : preimage U) (p : Prime) :
39     (f x).val p = homDiagonal U V f p * x.val p := by
40   let n := (x.val p).val
41   let e := preimageSeed U p
42   have hz : (x - n • e).val p = 0 := by
43     change x.val p - n • e.val p = 0
44     simp [n, e, nsmul_eq_mul]
45   have h := hom_preserves_zero_coordinate U V f (x - n • e) p hz
46   rw [map_sub, map_nsmul] at h
47   change (f x).val p - n • (f e).val p = 0 at h
48   simpa [n, e, homDiagonal, nsmul_eq_mul, mul_comm] using sub_eq_zero.mp h
49 
50 /-- The coefficient family is unique, since each prime seed is an actual source element. -/
51 theorem homDiagonal_unique (U V : Submodule ℚ TailSpace)
52     (f : preimage U →+ preimage V) (c : Ambient)
53     (h : ∀ x : preimage U, ∀ p : Prime, (f x).val p = c p * x.val p) :
54     c = homDiagonal U V f := by
55   funext p
56   simpa [homDiagonal] using (h (preimageSeed U p) p).symm
57 
58 /-- Scalar families determine homomorphisms on the entire infinite group. -/
59 theorem homDiagonal_injective (U V : Submodule ℚ TailSpace) :
60     Function.Injective (homDiagonal U V) := by
61   intro f g h
62   apply AddMonoidHom.ext
63   intro x
64   apply Subtype.ext
65   funext p
66   rw [hom_coordinate_formula U V f, hom_coordinate_formula U V g, h]
67 
68 /-- Coordinate multiplication on the unrestricted product. -/
69 def diagonal (c : Ambient) : Ambient →+ Ambient where
70   toFun x p := c p * x p
71   map_zero' := by funext p; simp
72   map_add' x y := by funext p; exact mul_add (c p) (x p) (y p)
73 
74 @[simp] theorem diagonal_apply (c x : Ambient) (p : Prime) :
75     diagonal c x p = c p * x p := rfl
76 
77 @[simp] theorem diagonal_one (x : Ambient) : diagonal 1 x = x := by
78   funext p
79   simp
80 
81 @[simp] theorem diagonal_add (c d x : Ambient) :
82     diagonal (c + d) x = diagonal c x + diagonal d x := by
83   funext p
84   exact add_mul (c p) (d p) (x p)
85 
86 @[simp] theorem diagonal_mul (c d x : Ambient) :
87     diagonal (c * d) x = diagonal c (diagonal d x) := by
88   funext p
89   exact mul_assoc (c p) (d p) (x p)
90 
91 /-- Arbitrary diagonal families preserve finite support. -/
92 theorem diagonal_finiteSupport (c : Ambient) (x : Ambient) (hx : x ∈ finiteSupport) :
93     diagonal c x ∈ finiteSupport := by
94   apply (show (support x).Finite from hx).subset
95   intro p hp hxp
96   exact hp (by simp [hxp])
97 
98 /-- The original map is exactly the restriction of its recovered ambient diagonal. -/
99 theorem hom_eq_diagonal (U V : Submodule ℚ TailSpace)
100     (f : preimage U →+ preimage V) (x : preimage U) :
101     (f x).val = diagonal (homDiagonal U V f) x.val := by
102   funext p
103   exact hom_coordinate_formula U V f x p
104 
105 /-- Every coordinate multiplier is continuous for the actual product topology. -/
106 theorem diagonal_continuous (c : Ambient) : Continuous (diagonal c) := by
107   apply continuous_pi
108   intro p
109   exact (continuous_of_discreteTopology : Continuous (fun z : Coordinate p => c p * z)).comp
110     (continuous_apply p)
111 
112 /-- Automatic continuity: the abstract homomorphism needs no topological hypothesis. -/
113 theorem preimage_hom_continuous (U V : Submodule ℚ TailSpace)
114     (f : preimage U →+ preimage V) : Continuous f := by
115   apply continuous_induced_rng.mpr
116   have he : (fun x : preimage U => (f x).val) =
117       (diagonal (homDiagonal U V f)) ∘ (fun x : preimage U => x.val) := by
118     funext x
119     exact hom_eq_diagonal U V f x
120   rw [show (Subtype.val ∘ f) = (fun x : preimage U => (f x).val) from rfl, he]
121   exact (diagonal_continuous _).comp continuous_subtype_val
122 
123 /-- The induced quotient map exists because preservation of D was proved. -/
124 def diagonalTailAdd (c : Ambient) : TailSpace →+ TailSpace :=
125   QuotientAddGroup.map finiteSupport finiteSupport (diagonal c)
126     (fun x hx => diagonal_finiteSupport c x hx)
127 
128 @[simp] theorem diagonalTailAdd_quotient (c x : Ambient) :
129     diagonalTailAdd c (quotientMap x) = quotientMap (diagonal c x) := rfl
130 
131 /-- Rational linearity follows from unique division, not an assumed scalar action. -/
132 def diagonalTail (c : Ambient) : TailSpace →ₗ[ℚ] TailSpace where
133   toAddHom := diagonalTailAdd c
134   map_smul' r x := map_rat_smul (diagonalTailAdd c) r x
135 
136 @[simp] theorem diagonalTail_quotient (c x : Ambient) :
137     diagonalTail c (quotientMap x) = quotientMap (diagonal c x) := rfl
138 
139 @[simp] theorem diagonalTail_one (v : TailSpace) : diagonalTail 1 v = v := by
140   obtain ⟨x, rfl⟩ := quotientMap_surjective v
141   simp
142 
143 @[simp] theorem diagonalTail_add (c d : Ambient) (v : TailSpace) :
144     diagonalTail (c + d) v = diagonalTail c v + diagonalTail d v := by
145   obtain ⟨x, rfl⟩ := quotientMap_surjective v
146   simp
147 
148 @[simp] theorem diagonalTail_mul (c d : Ambient) (v : TailSpace) :
149     diagonalTail (c * d) v = diagonalTail c (diagonalTail d v) := by
150   obtain ⟨x, rfl⟩ := quotientMap_surjective v
151   simp
152 
153 end RealizationBoundaries

Back to source controls