RootFibers.lean

1 import RealizationBoundaries.FiniteQuotients
2 import Mathlib.SetTheory.Cardinal.Finite
3 
4 /-! # Actual integer-root fibers and their translation parameters
5 
6 Roots are elements of the original infinite preimage group. Translation by a
7 supplied root identifies the entire fiber with its integer-torsion kernel.
8 The kernel is then identified with the actual divisor-coordinate product.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace RealizationBoundaries
13 
14 /-- The full fiber of multiplication on the original group. -/
15 def RootFiber (W : Submodule ℚ TailSpace) (m : ℕ) (x : preimage W) :=
16   {y : preimage W // m • y = x}
17 
18 /-- The actual integer-torsion kernel inside the original group. -/
19 def rootKernel (W : Submodule ℚ TailSpace) (m : ℕ) : AddSubgroup (preimage W) :=
20   (integerMultiplication W m).ker
21 
22 @[simp] theorem mem_rootKernel (W : Submodule ℚ TailSpace) (m : ℕ) (y : preimage W) :
23     y ∈ rootKernel W m ↔ m • y = 0 := Iff.rfl
24 
25 /-- A kernel element cannot have a nonzero coordinate away from the multiplier. -/
26 theorem rootKernel_coordinate_zero (W : Submodule ℚ TailSpace) (m : ℕ)
27     (y : rootKernel W m) (p : Prime) (hp : ¬ p.val ∣ m) : y.val.val p = 0 := by
28   apply coordinate_eq_zero_of_nsmul_eq_zero p hp
29   exact congrArg (fun z : preimage W => z.val p) y.property
30 
31 /-- Zero extension is killed by m, before any finiteness assumption is used. -/
32 theorem coordinateExtension_annihilated (m : ℕ) (z : DivisorCoordinates m) :
33     m • coordinateExtension m z = 0 := by
34   funext p
35   rw [coordinate_nsmul]
36   by_cases hp : p.val ∣ m
37   · simp [(coordinate_cast_eq_zero m p).mpr hp]
38   · simp [coordinateExtension, hp]
39 
40 /-- All m-torsion is given by arbitrary values in precisely the prime-divisor coordinates. -/
41 def rootKernelEquiv (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
42     rootKernel W m ≃+ DivisorCoordinates m where
43   toFun y := coordinateMap W m y.val
44   invFun z := ⟨⟨coordinateExtension m z,
45     finiteSupport_le_preimage W (coordinateExtension_finite hm z)⟩,
46     Subtype.ext (coordinateExtension_annihilated m z)⟩
47   left_inv y := by
48     apply Subtype.ext
49     apply Subtype.ext
50     funext p
51     by_cases hp : p.val ∣ m
52     · simp [coordinateExtension, coordinateMap, hp]
53     · simp [coordinateExtension, hp, rootKernel_coordinate_zero W m y p hp]
54   right_inv z := by
55     funext p
56     simp [coordinateMap, coordinateExtension, p.property]
57   map_add' _ _ := rfl
58 
59 @[simp] theorem rootKernelEquiv_apply (W : Submodule ℚ TailSpace) {m : ℕ}
60     (hm : 0 < m) (y : rootKernel W m) (p : DivisorPrime m) :
61     rootKernelEquiv W hm y p = y.val.val p.val := rfl
62 
63 @[simp] theorem rootKernelEquiv_symm_apply (W : Submodule ℚ TailSpace) {m : ℕ}
64     (hm : 0 < m) (z : DivisorCoordinates m) :
65     ((rootKernelEquiv W hm).symm z).val.val = coordinateExtension m z := rfl
66 
67 /-- Translation is an equivalence of sets, not an additive equivalence to a nonzero fiber. -/
68 def rootFiberTranslation (W : Submodule ℚ TailSpace) (m : ℕ) (x : preimage W)
69     (y : RootFiber W m x) : rootKernel W m ≃ RootFiber W m x where
70   toFun k := ⟨y.val + k.val, by
71     rw [nsmul_add, y.property, (mem_rootKernel W m k.val).mp k.property, add_zero]⟩
72   invFun z := ⟨z.val - y.val, by
73     change m • (z.val - y.val) = 0
74     rw [nsmul_sub, z.property, y.property, sub_self]⟩
75   left_inv k := by
76     apply Subtype.ext
77     simp
78   right_inv z := by
79     apply Subtype.ext
80     simp
81 
82 @[simp] theorem rootFiberTranslation_apply (W : Submodule ℚ TailSpace) (m : ℕ)
83     (x : preimage W) (y : RootFiber W m x) (k : rootKernel W m) :
84     (rootFiberTranslation W m x y k).val = y.val + k.val := rfl
85 
86 /-- One actual root and arbitrary divisor-coordinate values parameterize every root exactly once. -/
87 def rootFiberEquiv (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
88     (x : preimage W) (y : RootFiber W m x) : RootFiber W m x ≃ DivisorCoordinates m :=
89   (rootFiberTranslation W m x y).symm.trans (rootKernelEquiv W hm).toEquiv
90 
91 /-- Literal affine solution formula in the original ambient product. -/
92 @[simp] theorem rootFiberEquiv_symm_apply (W : Submodule ℚ TailSpace) {m : ℕ}
93     (hm : 0 < m) (x : preimage W) (y : RootFiber W m x) (z : DivisorCoordinates m) :
94     ((rootFiberEquiv W hm x y).symm z).val.val =
95       y.val.val + coordinateExtension m z := rfl
96 
97 /-- The coset criterion retains the supplied root and actual kernel membership. -/
98 theorem rootFiber_coset_iff (W : Submodule ℚ TailSpace) (m : ℕ) (x : preimage W)
99     (y : RootFiber W m x) (z : preimage W) :
100     m • z = x ↔ z - y.val ∈ rootKernel W m := by
101   rw [mem_rootKernel, nsmul_sub, y.property, sub_eq_zero]
102 
103 /-- Unsolvability gives a genuinely empty type of roots. -/
104 theorem rootFiber_isEmpty (W : Submodule ℚ TailSpace) (m : ℕ) (x : preimage W)
105     (h : ¬ ∃ y : preimage W, m • y = x) : IsEmpty (RootFiber W m x) :=
106   ⟨fun y => h ⟨y.val, y.property⟩⟩
107 
108 /-- Nonempty root fibers are finite for every positive multiplier. -/
109 theorem rootFiber_finite (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
110     (x : preimage W) : Finite (RootFiber W m x) := by
111   classical
112   by_cases h : Nonempty (RootFiber W m x)
113   · let y := Classical.choice h
114     let : Finite (DivisorCoordinates m) := divisorCoordinates_finite hm
115     exact Finite.of_injective (rootFiberEquiv W hm x y) (rootFiberEquiv W hm x y).injective
116   · let : IsEmpty (RootFiber W m x) := not_nonempty_iff.mp h
117     infer_instance
118 
119 /-- Kernel finiteness is proved using its explicit coordinate equivalence. -/
120 theorem rootKernel_finite (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
121     Finite (rootKernel W m) := by
122   let : Finite (DivisorCoordinates m) := divisorCoordinates_finite hm
123   exact Finite.of_injective (rootKernelEquiv W hm) (rootKernelEquiv W hm).injective
124 
125 end RealizationBoundaries

Back to source controls