PureCorrespondence.lean

1 import RealizationBoundaries.Preimages
2 import Mathlib.Order.Hom.Basic
3 
4 /-!
5 # The reverse pure-preimage correspondence
6 
7 Purity means lifting roots that already exist in the ambient group. It does not
8 mean that every element has every root. Containment of the actual torsion subgroup
9 D is retained explicitly; it is what upgrades root lifting to root closure.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace RealizationBoundaries
14 
15 /-- Standard root-lifting purity relative to the actual ambient product. -/
16 def IsPure (H : AddSubgroup Ambient) : Prop :=
17   ∀ (m : ℕ), 0 < m → ∀ x : H,
18     (∃ y : Ambient, m • y = x.val) → ∃ y : H, m • y = x
19 
20 /-- A pure intermediate subgroup includes all finite-support torsion. -/
21 abbrev PureIntermediate := {H : AddSubgroup Ambient // finiteSupport ≤ H ∧ IsPure H}
22 
23 /-- With D included, any ambient root of a point of H lies in H. -/
24 theorem pure_root_closed (H : AddSubgroup Ambient) (hD : finiteSupport ≤ H)
25     (hH : IsPure H) {m : ℕ} (hm : 0 < m) (x : Ambient) (hx : m • x ∈ H) :
26     x ∈ H := by
27   obtain ⟨y, hy⟩ := hH m hm ⟨m • x, hx⟩ ⟨x, rfl⟩
28   have hdiff : m • (x - y.val) = 0 := by
29     rw [nsmul_sub]
30     exact sub_eq_zero.mpr (congrArg Subtype.val hy).symm
31   have hd : x - y.val ∈ finiteSupport :=
32     (torsion_iff_finiteSupport _).mp ⟨m, hm, hdiff⟩
33   have := H.add_mem (hD hd) y.property
34   simpa using this
35 
36 /-- The image of H under the quotient map remembers H exactly when D is included. -/
37 theorem mem_quotient_image_iff (H : AddSubgroup Ambient) (hD : finiteSupport ≤ H)
38     (x : Ambient) : quotientMap x ∈ H.map quotientMap ↔ x ∈ H := by
39   constructor
40   · rintro ⟨y, hy, hxy⟩
41     have hd : x - y ∈ finiteSupport := (quotientMap_eq_iff x y).mp hxy.symm
42     have := H.add_mem (hD hd) hy
43     simpa using this
44   · intro hx
45     exact ⟨x, hx, rfl⟩
46 
47 /-- Root closure descends to the actual quotient image. -/
48 theorem quotient_image_nsmul_closed (H : AddSubgroup Ambient)
49     (hD : finiteSupport ≤ H) (hH : IsPure H) {m : ℕ} (hm : 0 < m)
50     (v : TailSpace) (hv : m • v ∈ H.map quotientMap) : v ∈ H.map quotientMap := by
51   obtain ⟨x, rfl⟩ := quotientMap_surjective v
52   have hx : m • x ∈ H := (mem_quotient_image_iff H hD _).mp (by
53     simpa only [map_nsmul] using hv)
54   exact ⟨x, pure_root_closed H hD hH hm x hx, rfl⟩
55 
56 /-- The rational action on the quotient image is proved by clearing denominators. -/
57 theorem quotient_image_smul_mem (H : AddSubgroup Ambient)
58     (hD : finiteSupport ≤ H) (hH : IsPure H) (r : ℚ) (v : TailSpace)
59     (hv : v ∈ H.map quotientMap) : r • v ∈ H.map quotientMap := by
60   apply quotient_image_nsmul_closed H hD hH r.den_pos
61   have heq : r.den • (r • v) = r.num • v := by
62     rw [← Nat.cast_smul_eq_nsmul ℚ, ← Int.cast_smul_eq_zsmul ℚ, smul_smul,
63       Rat.den_mul_eq_num]
64   rw [heq]
65   exact (H.map quotientMap).zsmul_mem hv r.num
66 
67 /-- The rational subspace is constructed from the subgroup, not supplied as an input. -/
68 def rationalImage (H : AddSubgroup Ambient) (hD : finiteSupport ≤ H) (hH : IsPure H) :
69     Submodule ℚ TailSpace where
70   carrier := H.map quotientMap
71   zero_mem' := (H.map quotientMap).zero_mem
72   add_mem' := (H.map quotientMap).add_mem
73   smul_mem' := quotient_image_smul_mem H hD hH
74 
75 @[simp] theorem mem_rationalImage (H : AddSubgroup Ambient)
76     (hD : finiteSupport ≤ H) (hH : IsPure H) (v : TailSpace) :
77     v ∈ rationalImage H hD hH ↔ v ∈ H.map quotientMap := Iff.rfl
78 
79 /-- The reverse construction recovers the literal original subgroup. -/
80 @[simp] theorem preimage_rationalImage (H : AddSubgroup Ambient)
81     (hD : finiteSupport ≤ H) (hH : IsPure H) : preimage (rationalImage H hD hH) = H := by
82   ext x
83   exact mem_quotient_image_iff H hD x
84 
85 /-- Every rational preimage satisfies the root-lifting definition of purity. -/
86 theorem preimage_isPure (W : Submodule ℚ TailSpace) : IsPure (preimage W) := by
87   intro m hm x hx
88   exact preimage_pure W hm x hx
89 
90 /-- Quotienting a rational preimage recovers exactly the original rational subspace. -/
91 @[simp] theorem rationalImage_preimage (W : Submodule ℚ TailSpace) :
92     rationalImage (preimage W) (finiteSupport_le_preimage W) (preimage_isPure W) = W := by
93   ext v
94   constructor
95   · rintro ⟨x, hx, rfl⟩
96     exact hx
97   · intro hv
98     obtain ⟨x, rfl⟩ := quotientMap_surjective v
99     exact ⟨x, hv, rfl⟩
100 
101 /-- Canonical inclusion reflects the order on rational subspaces. -/
102 theorem preimage_le_iff (V W : Submodule ℚ TailSpace) : preimage V ≤ preimage W ↔ V ≤ W := by
103   constructor
104   · intro h v hv
105     obtain ⟨x, rfl⟩ := quotientMap_surjective v
106     exact h hv
107   · intro h x hx
108     exact h hx
109 
110 /-- Monograph Theorem 4.2: order equivalence, including both inverse laws. -/
111 def purePreimageOrderIso : Submodule ℚ TailSpace ≃o PureIntermediate where
112   toFun W := ⟨preimage W, finiteSupport_le_preimage W, preimage_isPure W⟩
113   invFun H := rationalImage H.val H.property.1 H.property.2
114   left_inv W := rationalImage_preimage W
115   right_inv H := Subtype.ext (preimage_rationalImage H.val H.property.1 H.property.2)
116   map_rel_iff' := fun {_ _} => preimage_le_iff _ _
117 
118 /-- A rational subspace witnessing a pure intermediate group exists uniquely. -/
119 theorem exists_unique_rational_preimage (H : AddSubgroup Ambient)
120     (hD : finiteSupport ≤ H) (hH : IsPure H) :
121     ∃! W : Submodule ℚ TailSpace, preimage W = H := by
122   refine ⟨rationalImage H hD hH, preimage_rationalImage H hD hH, ?_⟩
123   intro W hW
124   apply le_antisymm
125   · exact (preimage_le_iff _ _).mp (by rw [hW, preimage_rationalImage])
126   · exact (preimage_le_iff _ _).mp (by rw [hW, preimage_rationalImage])
127 
128 end RealizationBoundaries

Back to source controls