DiagonalRealization.lean

1 import RealizationBoundaries.DiagonalHomomorphisms
2 import Mathlib.Algebra.Ring.Subring.Basic
3 import Mathlib.Algebra.Ring.Equiv
4 
5 /-!
6 # Exact realization of the diagonal families
7 
8 A family is admitted precisely when its actual ambient multiplier takes the
9 source preimage into the target. This condition is equivalent to rational-line
10 membership and to a finite section defect in the selector setting.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace RealizationBoundaries
15 
16 /-- The condition is on actual points in the two original subgroups. -/
17 def DiagonalAdmissible (U V : Submodule ℚ TailSpace) (c : Ambient) : Prop :=
18   ∀ x : Ambient, x ∈ preimage U → diagonal c x ∈ preimage V
19 
20 /-- Every recovered family is admissible, as a consequence of the coordinate formula. -/
21 theorem homDiagonal_admissible (U V : Submodule ℚ TailSpace)
22     (f : preimage U →+ preimage V) : DiagonalAdmissible U V (homDiagonal U V f) := by
23   intro x hx
24   rw [← hom_eq_diagonal U V f ⟨x, hx⟩]
25   exact (f ⟨x, hx⟩).property
26 
27 /-- Restricting a family is legitimate only after its preservation condition is proved. -/
28 def diagonalRestriction (U V : Submodule ℚ TailSpace) (c : Ambient)
29     (h : DiagonalAdmissible U V c) : preimage U →+ preimage V where
30   toFun x := ⟨diagonal c x.val, h x.val x.property⟩
31   map_zero' := Subtype.ext (map_zero (diagonal c))
32   map_add' x y := Subtype.ext (map_add (diagonal c) x.val y.val)
33 
34 @[simp] theorem diagonalRestriction_val (U V : Submodule ℚ TailSpace) (c : Ambient)
35     (h : DiagonalAdmissible U V c) (x : preimage U) :
36     (diagonalRestriction U V c h x).val = diagonal c x.val := rfl
37 
38 @[simp] theorem homDiagonal_restriction (U V : Submodule ℚ TailSpace) (c : Ambient)
39     (h : DiagonalAdmissible U V c) : homDiagonal U V (diagonalRestriction U V c h) = c := by
40   funext p
41   simp [homDiagonal, diagonalRestriction]
42 
43 @[simp] theorem diagonalRestriction_recovery (U V : Submodule ℚ TailSpace)
44     (f : preimage U →+ preimage V) :
45     diagonalRestriction U V (homDiagonal U V f) (homDiagonal_admissible U V f) = f := by
46   apply AddMonoidHom.ext
47   intro x
48   exact Subtype.ext (hom_eq_diagonal U V f x).symm
49 
50 /-- Classification of all abstract homomorphisms by their unique admissible families. -/
51 def diagonalHomEquiv (U V : Submodule ℚ TailSpace) :
52     (preimage U →+ preimage V) ≃ {c : Ambient // DiagonalAdmissible U V c} where
53   toFun f := ⟨homDiagonal U V f, homDiagonal_admissible U V f⟩
54   invFun c := diagonalRestriction U V c.val c.property
55   left_inv := diagonalRestriction_recovery U V
56   right_inv c := Subtype.ext (homDiagonal_restriction U V c.val c.property)
57 
58 /-- A diagonal map preserves the original preimages exactly when its derived rational
59 map takes the source subspace into the target subspace. -/
60 theorem diagonalAdmissible_iff_tail (U V : Submodule ℚ TailSpace) (c : Ambient) :
61     DiagonalAdmissible U V c ↔ ∀ v ∈ U, diagonalTail c v ∈ V := by
62   constructor
63   · intro h v hv
64     obtain ⟨x, rfl⟩ := quotientMap_surjective v
65     exact h x hv
66   · intro h x hx
67     exact h (quotientMap x) hx
68 
69 /-- For lines, the entire preservation contract reduces to the actual generating tail. -/
70 theorem diagonalAdmissible_selector_iff (S T : Set Prime) (c : Ambient) :
71     DiagonalAdmissible (selectorLine S) (selectorLine T) c ↔
72       diagonal c (indicator S) ∈ selectorGroup T := by
73   constructor
74   · intro h
75     exact h (indicator S) (markedElement S).property
76   · intro h x hx
77     obtain ⟨r, hr⟩ := (mem_selectorGroup_iff S x).mp hx
78     change quotientMap (diagonal c x) ∈ selectorLine T
79     rw [← diagonalTail_quotient, ← hr, map_smul]
80     exact (selectorLine T).smul_mem r h
81 
82 /-- The section defect is finite precisely when the diagonal can be realized. -/
83 theorem diagonalAdmissible_iff_finite_defect (S T : Set Prime) (c : Ambient) :
84     DiagonalAdmissible (selectorLine S) (selectorLine T) c ↔
85       ∃ r : ℚ, diagonal c (indicator S) - rationalSection T r ∈ finiteSupport := by
86   rw [diagonalAdmissible_selector_iff, mem_selectorGroup_iff]
87   constructor
88   · rintro ⟨r, hr⟩
89     refine ⟨r, (quotientMap_eq_iff _ _).mp ?_⟩
90     rw [quotientMap_rationalSection, hr]
91   · rintro ⟨r, hr⟩
92     refine ⟨r, ?_⟩
93     have hq := (quotientMap_eq_iff _ _).mpr hr
94     rw [quotientMap_rationalSection] at hq
95     exact hq.symm
96 
97 /-- Monograph Theorem 7.5: exact full-family realization and uniqueness. -/
98 def selectorHomEquiv (S T : Set Prime) :
99     (selectorGroup S →+ selectorGroup T) ≃
100       {c : Ambient // ∃ r : ℚ,
101         diagonal c (indicator S) - rationalSection T r ∈ finiteSupport} where
102   toFun f := ⟨homDiagonal (selectorLine S) (selectorLine T) f,
103     (diagonalAdmissible_iff_finite_defect S T _).mp
104       (homDiagonal_admissible (selectorLine S) (selectorLine T) f)⟩
105   invFun c := diagonalRestriction (selectorLine S) (selectorLine T) c.val
106     ((diagonalAdmissible_iff_finite_defect S T c.val).mpr c.property)
107   left_inv f := diagonalRestriction_recovery (selectorLine S) (selectorLine T) f
108   right_inv c := Subtype.ext (homDiagonal_restriction (selectorLine S) (selectorLine T) c.val
109     ((diagonalAdmissible_iff_finite_defect S T c.val).mpr c.property))
110 
111 /-- The actual admissible families form a subring of the coordinate product. -/
112 def diagonalEndRing (W : Submodule ℚ TailSpace) : Subring Ambient where
113   carrier := {c | DiagonalAdmissible W W c}
114   zero_mem' := by
115     intro x _
116     have hz : diagonal 0 x = 0 := by funext p; simp
117     rw [hz]
118     exact (preimage W).zero_mem
119   one_mem' := by intro x hx; simpa using hx
120   add_mem' := by
121     intro c d hc hd x hx
122     rw [diagonal_add]
123     exact (preimage W).add_mem (hc x hx) (hd x hx)
124   neg_mem' := by
125     intro c hc x hx
126     have hn : diagonal (-c) x = -(diagonal c x) := by funext p; simp
127     rw [hn]
128     exact (preimage W).neg_mem (hc x hx)
129   mul_mem' := by
130     intro c d hc hd x hx
131     rw [diagonal_mul]
132     exact hc _ (hd x hx)
133 
134 /-- Addition and composition of actual endomorphisms become coordinate ring operations. -/
135 def homDiagonalRing (W : Submodule ℚ TailSpace) :
136     AddMonoid.End (preimage W) →+* diagonalEndRing W where
137   toFun f := ⟨homDiagonal W W f, homDiagonal_admissible W W f⟩
138   map_zero' := rfl
139   map_one' := by
140     apply Subtype.ext
141     funext p
142     exact preimageSeed_apply W p
143   map_add' _ _ := rfl
144   map_mul' f g := by
145     apply Subtype.ext
146     funext p
147     exact hom_coordinate_formula W W f (g (preimageSeed W p)) p
148 
149 /-- Ring equivalence, not merely a bijection between underlying sets. -/
150 def endomorphismRingEquiv (W : Submodule ℚ TailSpace) :
151     AddMonoid.End (preimage W) ≃+* diagonalEndRing W :=
152   RingEquiv.ofBijective (homDiagonalRing W) (by
153     constructor
154     · intro f g h
155       exact homDiagonal_injective W W (congrArg Subtype.val h)
156     · intro c
157       exact ⟨diagonalRestriction W W c.val c.property,
158         Subtype.ext (homDiagonal_restriction W W c.val c.property)⟩)
159 
160 /-- Commutativity is a proved property of this endomorphism ring. -/
161 theorem preimage_endomorphisms_commute (W : Submodule ℚ TailSpace)
162     (f g : AddMonoid.End (preimage W)) : f * g = g * f := by
163   apply (endomorphismRingEquiv W).injective
164   simp only [map_mul, mul_comm]
165 
166 end RealizationBoundaries

Back to source controls