Ambient.lean

1 import Mathlib.Algebra.Field.ZMod
2 import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
3 import Mathlib.Data.Nat.Prime.Infinite
4 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
5 import Mathlib.GroupTheory.QuotientGroup.Basic
6 import Mathlib.Data.Set.Finite.Basic
7 
8 /-!
9 # The actual squarefree product and its finite-support subgroup
10 
11 The index type contains every natural prime exactly once. The product below is
12 an unrestricted dependent function space, not a finite truncation.
13 -/
14 
15 set_option autoImplicit false
16 noncomputable section
17 open scoped BigOperators
18 
19 namespace RealizationBoundaries
20 
21 abbrev Prime := Nat.Primes
22 abbrev Coordinate (p : Prime) := ZMod p.val
23 abbrev Ambient := (p : Prime) → Coordinate p
24 
25 instance primeFact (p : Prime) : Fact p.val.Prime := ⟨p.property⟩
26 
27 def support (x : Ambient) : Set Prime := {p | x p ≠ 0}
28 
29 @[simp] theorem mem_support (x : Ambient) (p : Prime) :
30     p ∈ support x ↔ x p ≠ 0 := Iff.rfl
31 
32 def finiteSupport : AddSubgroup Ambient where
33   carrier := {x | (support x).Finite}
34   zero_mem' := by simp [support]
35   add_mem' := by
36     intro x y hx hy
37     apply (hx.union hy).subset
38     intro p hp
39     by_contra hn
40     have hxy : x p = 0 ∧ y p = 0 := by simpa [support] using hn
41     exact hp (by simp [hxy.1, hxy.2])
42   neg_mem' := by
43     intro x hx
44     simpa [support] using hx
45 
46 @[simp] theorem mem_finiteSupport (x : Ambient) :
47     x ∈ finiteSupport ↔ (support x).Finite := Iff.rfl
48 
49 /-- A finite pattern interpreted as an actual infinite vector. -/
50 def cut (s : Finset Prime) (x : Ambient) : Ambient :=
51   fun p => if p ∈ s then x p else 0
52 
53 theorem cut_mem_finiteSupport (s : Finset Prime) (x : Ambient) :
54     cut s x ∈ finiteSupport := by
55   apply s.finite_toSet.subset
56   intro p hp
57   by_contra hn
58   have hn' : p ∉ s := hn
59   exact hp (by simp [cut, hn'])
60 
61 @[simp] theorem cut_apply_mem (s : Finset Prime) (x : Ambient) (p : Prime)
62     (hp : p ∈ s) : cut s x p = x p := by simp [cut, hp]
63 
64 @[simp] theorem cut_apply_not_mem (s : Finset Prime) (x : Ambient) (p : Prime)
65     (hp : p ∉ s) : cut s x p = 0 := by simp [cut, hp]
66 
67 /-- All prime coordinates at which multiplication by `m` can fail to be a unit. -/
68 def exceptional (m : ℕ) : Set Prime := {p | p.val ∣ m}
69 
70 theorem exceptional_finite {m : ℕ} (hm : 0 < m) : (exceptional m).Finite := by
71   have hfinite : {p : Prime | p.val ≤ m}.Finite :=
72     (Set.finite_Iic m).preimage Subtype.val_injective.injOn
73   exact hfinite.subset (fun p hp => Nat.le_of_dvd hm hp)
74 
75 @[simp] theorem coordinate_nsmul (m : ℕ) (x : Ambient) (p : Prime) :
76     (m • x) p = (m : Coordinate p) * x p := by
77   simp [nsmul_eq_mul]
78 
79 /-- Exact obstruction to multiplication by an integer in one prime coordinate. -/
80 theorem coordinate_cast_eq_zero (m : ℕ) (p : Prime) :
81     (m : Coordinate p) = 0 ↔ p.val ∣ m := by
82   exact CharP.cast_eq_zero_iff (Coordinate p) p.val m
83 
84 /-- A nonexceptional coordinate cannot disappear under multiplication. -/
85 theorem coordinate_eq_zero_of_nsmul_eq_zero {m : ℕ} {x : Ambient} (p : Prime)
86     (hp : ¬ p.val ∣ m) (hx : (m • x) p = 0) : x p = 0 := by
87   have hm : (m : Coordinate p) ≠ 0 := (coordinate_cast_eq_zero m p).not.mpr hp
88   exact (mul_eq_zero.mp ((coordinate_nsmul m x p) ▸ hx)).resolve_left hm
89 
90 /-- Integer multiplication cannot turn an infinitely supported vector into a finite one. -/
91 theorem finiteSupport_of_nsmul {m : ℕ} (hm : 0 < m) (x : Ambient)
92     (hx : m • x ∈ finiteSupport) : x ∈ finiteSupport := by
93   apply ((show (support (m • x)).Finite from hx).union (exceptional_finite hm)).subset
94   intro p hp
95   by_contra hn
96   have hn' : (m • x) p = 0 ∧ ¬p.val ∣ m := by
97     simpa only [Set.mem_union, mem_support, exceptional, Set.mem_ofPred_eq, not_or, not_not] using hn
98   exact hp (coordinate_eq_zero_of_nsmul_eq_zero p hn'.2 hn'.1)
99 
100 /-- Every finitely supported vector is killed by a positive integer. -/
101 theorem exists_annihilator_of_finiteSupport (x : Ambient) (hx : x ∈ finiteSupport) :
102     ∃ m : ℕ, 0 < m ∧ m • x = 0 := by
103   classical
104   let s := (show (support x).Finite from hx).toFinset
105   refine ⟨∏ p ∈ s, p.val, ?_, ?_⟩
106   · exact Finset.prod_pos (fun p _ => p.property.pos)
107   · funext p
108     by_cases hp : p ∈ s
109     · have hd : p.val ∣ ∏ q ∈ s, q.val := Finset.dvd_prod_of_mem (fun q : Prime => q.val) hp
110       simp [(coordinate_cast_eq_zero _ p).mpr hd]
111     · have hxp : x p = 0 := by simpa [s, support] using hp
112       simp [hxp]
113 
114 /-- Monograph Theorem 2.1, algebraic torsion assertion. -/
115 theorem torsion_iff_finiteSupport (x : Ambient) :
116     (∃ m : ℕ, 0 < m ∧ m • x = 0) ↔ x ∈ finiteSupport := by
117   constructor
118   · rintro ⟨m, hm, hmx⟩
119     exact finiteSupport_of_nsmul hm x (hmx ▸ finiteSupport.zero_mem)
120   · exact exists_annihilator_of_finiteSupport x
121 
122 end RealizationBoundaries

Back to source controls