Quotient.lean

1 import RealizationBoundaries.Ambient
2 import Mathlib.GroupTheory.DivisibleHull
3 import Mathlib.Algebra.Module.TransferInstance
4 import Mathlib.Algebra.Module.Rat
5 
6 /-!
7 # Unique division in the actual quotient P/D
8 
9 The rational module structure is transported only after the concrete quotient
10 has been proved uniquely divisible. No rational-space witness is postulated.
11 -/
12 set_option autoImplicit false
13 set_option backward.isDefEq.respectTransparency false
14 noncomputable section
15 namespace RealizationBoundaries
16 
17 def TailSpace := Ambient ⧸ finiteSupport
18 
19 instance tailAddCommGroup : AddCommGroup TailSpace :=
20   QuotientAddGroup.Quotient.addCommGroup finiteSupport
21 
22 def quotientMap : Ambient →+ TailSpace := QuotientAddGroup.mk' finiteSupport
23 
24 @[simp] theorem quotientMap_eq_zero_iff (x : Ambient) :
25     quotientMap x = 0 ↔ x ∈ finiteSupport :=
26   QuotientAddGroup.eq_zero_iff x
27 
28 theorem quotientMap_surjective : Function.Surjective quotientMap :=
29   QuotientAddGroup.mk'_surjective finiteSupport
30 
31 theorem quotientMap_eq_iff (x y : Ambient) :
32     quotientMap x = quotientMap y ↔ x - y ∈ finiteSupport := by
33   rw [← sub_eq_zero, ← map_sub, quotientMap_eq_zero_iff]
34 
35 /-- Coordinate division is zero at the exceptional primes because inverse zero is zero. -/
36 def coordinateDivide (m : ℕ) (x : Ambient) : Ambient :=
37   fun p => (m : Coordinate p)⁻¹ * x p
38 
39 /-- Division has a genuinely finite error in the infinite product. -/
40 theorem division_defect_finite {m : ℕ} (hm : 0 < m) (x : Ambient) :
41     m • coordinateDivide m x - x ∈ finiteSupport := by
42   apply (exceptional_finite hm).subset
43   intro p hp
44   by_contra hn
45   have hcast : (m : Coordinate p) ≠ 0 := (coordinate_cast_eq_zero m p).not.mpr hn
46   apply hp
47   rw [Pi.sub_apply, coordinate_nsmul]
48   change (m : Coordinate p) * ((m : Coordinate p)⁻¹ * x p) - x p = 0
49   rw [mul_inv_cancel_left₀ hcast, sub_self]
50 
51 theorem tail_nsmul_surjective {m : ℕ} (hm : 0 < m) :
52     Function.Surjective (fun v : TailSpace => m • v) := by
53   intro v
54   obtain ⟨x, rfl⟩ := quotientMap_surjective v
55   refine ⟨quotientMap (coordinateDivide m x), ?_⟩
56   change m • quotientMap (coordinateDivide m x) = quotientMap x
57   rw [← map_nsmul]
58   exact (quotientMap_eq_iff _ _).mpr (division_defect_finite hm x)
59 
60 theorem tail_nsmul_injective {m : ℕ} (hm : 0 < m) :
61     Function.Injective (fun v : TailSpace => m • v) := by
62   intro v w hvw
63   obtain ⟨x, rfl⟩ := quotientMap_surjective v
64   obtain ⟨y, rfl⟩ := quotientMap_surjective w
65   apply (quotientMap_eq_iff x y).mpr
66   apply finiteSupport_of_nsmul hm
67   apply (quotientMap_eq_zero_iff _).mp
68   change m • quotientMap x = m • quotientMap y at hvw
69   rw [map_nsmul, map_sub, nsmul_sub, hvw, sub_self]
70 
71 /-- Monograph Theorem 2.6: every positive integer acts bijectively on P/D. -/
72 theorem tail_nsmul_bijective {m : ℕ} (hm : 0 < m) :
73     Function.Bijective (fun v : TailSpace => m • v) :=
74   ⟨tail_nsmul_injective hm, tail_nsmul_surjective hm⟩
75 
76 instance : IsAddTorsionFree TailSpace where
77   nsmul_right_injective := by
78     intro n hn
79     exact tail_nsmul_injective (Nat.pos_of_ne_zero hn)
80 
81 /-- The divisible hull contributes no new points after unique division is established. -/
82 theorem tail_to_divisibleHull_surjective :
83     Function.Surjective (DivisibleHull.coeAddMonoidHom TailSpace : TailSpace →+ DivisibleHull TailSpace) := by
84   intro z
85   induction z using DivisibleHull.ind with
86   | mk v n =>
87     obtain ⟨w, hw⟩ := tail_nsmul_surjective n.property v
88     refine ⟨w, ?_⟩
89     change DivisibleHull.mk w 1 = DivisibleHull.mk v n
90     rw [DivisibleHull.mk_eq_mk_iff_smul_eq_smul]
91     convert! hw using 1
92     simp
93 
94 def tailDivisibleEquiv : TailSpace ≃+ DivisibleHull TailSpace :=
95   AddEquiv.ofBijective (DivisibleHull.coeAddMonoidHom TailSpace)
96     ⟨DivisibleHull.coe_injective, tail_to_divisibleHull_surjective⟩
97 
98 instance tailRationalModule : Module ℚ TailSpace := tailDivisibleEquiv.module ℚ
99 
100 /-- The rational action is uniquely determined by the underlying quotient group. -/
101 theorem tail_rational_module_unique : Subsingleton (Module ℚ TailSpace) := inferInstance
102 
103 /-- Clearing a positive denominator in the installed rational action is valid. -/
104 theorem tail_denominator_clear {m : ℕ} (hm : 0 < m) (v : TailSpace) :
105     m • ((m : ℚ)⁻¹ • v) = v := by
106   rw [← Nat.cast_smul_eq_nsmul ℚ, smul_smul]
107   simp [Nat.ne_of_gt hm]
108 
109 end RealizationBoundaries

Back to source controls