FiniteQuotients.lean

1 import RealizationBoundaries.Preimages
2 import Mathlib.GroupTheory.OrderOfElement
3 
4 /-! # Canonical integer quotients and cofinal finite-target kernels -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 abbrev DivisorPrime (m : ℕ) := {p : Prime // p.val ∣ m}
10 abbrev DivisorCoordinates (m : ℕ) := (p : DivisorPrime m) → Coordinate p.val
11 
12 theorem divisorPrime_finite {m : ℕ} (hm : 0 < m) : Finite (DivisorPrime m) :=
13   (exceptional_finite hm).to_subtype
14 
15 theorem divisorCoordinates_finite {m : ℕ} (hm : 0 < m) : Finite (DivisorCoordinates m) := by
16   let : Finite (DivisorPrime m) := divisorPrime_finite hm
17   infer_instance
18 
19 /-- Restriction to the finitely many prime coordinates dividing the multiplier. -/
20 def coordinateMap (W : Submodule ℚ TailSpace) (m : ℕ) :
21     preimage W →+ DivisorCoordinates m where
22   toFun x p := x.val p.val
23   map_zero' := rfl
24   map_add' _ _ := rfl
25 
26 /-- Extend a finite divisor-coordinate assignment by zero. -/
27 def coordinateExtension (m : ℕ) (z : DivisorCoordinates m) : Ambient :=
28   fun p => if hp : p.val ∣ m then z ⟨p, hp⟩ else 0
29 
30 theorem coordinateExtension_finite {m : ℕ} (hm : 0 < m) (z : DivisorCoordinates m) :
31     coordinateExtension m z ∈ finiteSupport := by
32   apply (exceptional_finite hm).subset
33   intro p hp
34   by_contra hn
35   apply hp
36   have hn' : ¬ p.val ∣ m := hn
37   simp [coordinateExtension, hn']
38 
39 theorem coordinateMap_surjective (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
40     Function.Surjective (coordinateMap W m) := by
41   intro z
42   refine ⟨⟨coordinateExtension m z,
43     finiteSupport_le_preimage W (coordinateExtension_finite hm z)⟩, ?_⟩
44   funext p
45   change coordinateExtension m z p.val = z p
46   simp [coordinateExtension, p.property]
47 
48 /-- Integer multiplication as a homomorphism on the original group. -/
49 def integerMultiplication (W : Submodule ℚ TailSpace) (m : ℕ) :
50     preimage W →+ preimage W where
51   toFun x := m • x
52   map_zero' := nsmul_zero m
53   map_add' x y := nsmul_add x y m
54 
55 /-- The actual subgroup m H_W, not just an abstract kernel with the same cardinality. -/
56 def multiples (W : Submodule ℚ TailSpace) (m : ℕ) : AddSubgroup (preimage W) :=
57   (integerMultiplication W m).range
58 
59 @[simp] theorem mem_multiples (W : Submodule ℚ TailSpace) (m : ℕ) (x : preimage W) :
60     x ∈ multiples W m ↔ ∃ y : preimage W, m • y = x := Iff.rfl
61 
62 /-- Both inclusions are proved using the concrete infinite-coordinate root theorem. -/
63 theorem coordinateMap_ker (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
64     (coordinateMap W m).ker = multiples W m := by
65   ext x
66   change coordinateMap W m x = 0 ↔ ∃ y : preimage W, m • y = x
67   rw [preimage_root_iff W hm x]
68   constructor
69   · intro h p hp
70     exact congrFun h ⟨p, hp⟩
71   · intro h
72     funext p
73     exact h p.val p.property
74 
75 /-- Monograph Theorem 4.4, algebraic quotient clause, with its canonical coordinate map. -/
76 def integerQuotientEquiv (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
77     (preimage W ⧸ multiples W m) ≃+ DivisorCoordinates m :=
78   (QuotientAddGroup.quotientAddEquivOfEq (coordinateMap_ker W hm).symm).trans
79     (QuotientAddGroup.quotientKerEquivOfSurjective (coordinateMap W m)
80       (coordinateMap_surjective W hm))
81 
82 @[simp] theorem integerQuotientEquiv_mk (W : Submodule ℚ TailSpace) {m : ℕ}
83     (hm : 0 < m) (x : preimage W) :
84     integerQuotientEquiv W hm (QuotientAddGroup.mk x) = coordinateMap W m x := by
85   rfl
86 
87 /-- The quotient kernels depend on the prime divisors, not their multiplicities. -/
88 theorem multiples_eq_of_same_prime_divisors (W : Submodule ℚ TailSpace)
89     {m n : ℕ} (hm : 0 < m) (hn : 0 < n)
90     (h : ∀ p : Prime, p.val ∣ m ↔ p.val ∣ n) : multiples W m = multiples W n := by
91   ext x
92   simp only [mem_multiples, preimage_root_iff W hm, preimage_root_iff W hn]
93   constructor
94   · intro hx p hp
95     exact hx p ((h p).mpr hp)
96   · intro hx p hp
97     exact hx p ((h p).mp hp)
98 
99 /-- The canonical finite-coordinate transition for divisibility of multipliers. -/
100 def coordinateRestriction {m n : ℕ} (hmn : m ∣ n) :
101     DivisorCoordinates n →+ DivisorCoordinates m where
102   toFun z p := z ⟨p.val, dvd_trans p.property hmn⟩
103   map_zero' := rfl
104   map_add' _ _ := rfl
105 
106 @[simp] theorem coordinateRestriction_map (W : Submodule ℚ TailSpace)
107     {m n : ℕ} (hmn : m ∣ n) (x : preimage W) :
108     coordinateRestriction hmn (coordinateMap W n x) = coordinateMap W m x := rfl
109 
110 /-- Every finite additive target kills a canonical integer-multiple subgroup.
111 This is the cofinal-kernel input, not a substitute definition of profinite completion. -/
112 theorem finite_target_kills_multiples (W : Submodule ℚ TailSpace)
113     (F : Type*) [AddGroup F] [Fintype F] (f : preimage W →+ F) :
114     multiples W (Fintype.card F) ≤ f.ker := by
115   rintro x ⟨y, rfl⟩
116   change f (Fintype.card F • y) = 0
117   rw [map_nsmul]
118   exact card_nsmul_eq_zero
119 
120 /-- A finite-coordinate quotient kernel is contained in the kernel of every finite-target map. -/
121 theorem finite_target_coordinate_kernel (W : Submodule ℚ TailSpace)
122     (F : Type*) [AddGroup F] [Fintype F] (f : preimage W →+ F) :
123     (coordinateMap W (Fintype.card F)).ker ≤ f.ker := by
124   rw [coordinateMap_ker W Fintype.card_pos]
125   exact finite_target_kills_multiples W F f
126 
127 end RealizationBoundaries

Back to source controls