PairIndex110.lean

1 import PaperXI.IntersectionModel108
2 import Mathlib.GroupTheory.Index
3 
4 /-! The pair group is identified with the first-coordinate intersection.
5 The orientation is literal: `ι b = g * ι a * g⁻¹`. The intersection in `K`
6 therefore contains the `a` whose conjugated image remains in `ι(K)`.
7 All results are generic group and index results; no arithmetic identity is assumed. -/
8 
9 set_option autoImplicit false
10 noncomputable section
11 
12 namespace PaperXI.PairIndex110
13 
14 open IntersectionModel108
15 
16 variable {K G : Type*} [Group K] [Group G]
17 
18 /-- The original element is the first coordinate of the pair model. -/
19 def intersection (ι : K →* G) (g : G) : Subgroup K :=
20   ι.range.comap ((MulAut.conj g).toMonoidHom.comp ι)
21 
22 /-- Both the first coordinate and its conjugated image lie in the scalar subgroup. -/
23 def scalarIntersection (ι : K →* G) (H : Subgroup K) (g : G) : Subgroup K :=
24   H ⊓ (H.map ι).comap ((MulAut.conj g).toMonoidHom.comp ι)
25 
26 theorem scalarIntersection_le (ι : K →* G) (H : Subgroup K) (g : G) :
27     scalarIntersection ι H g ≤ H := inf_le_left
28 
29 theorem scalarIntersection_le_intersection (ι : K →* G) (H : Subgroup K) (g : G) :
30     scalarIntersection ι H g ≤ intersection ι g := by
31   intro a ha
32   exact (H.map_le_range ι) ha.2
33 
34 /-- The ambient intersection has the same first-coordinate orientation. -/
35 theorem intersection_image (ι : K →* G) (g : G) :
36     (intersection ι g).map ι =
37       ι.range ⊓ ι.range.comap (MulAut.conj g).toMonoidHom := by
38   ext x
39   constructor
40   · rintro ⟨a, ha, rfl⟩
41     exact ⟨⟨a, rfl⟩, ha⟩
42   · intro hx
43     rcases hx.1 with ⟨a, rfl⟩
44     exact ⟨a, hx.2, rfl⟩
45 
46 /-- The two scalar membership conditions commute with embedding into `G`. -/
47 theorem scalarIntersection_image (ι : K →* G) (H : Subgroup K) (g : G) :
48     (scalarIntersection ι H g).map ι =
49       H.map ι ⊓ (H.map ι).comap (MulAut.conj g).toMonoidHom := by
50   ext x
51   constructor
52   · rintro ⟨a, ha, rfl⟩
53     exact ⟨⟨a, ha.1, rfl⟩, ha.2⟩
54   · intro hx
55     rcases hx.1 with ⟨a, ha, rfl⟩
56     exact ⟨a, ⟨ha, hx.2⟩, rfl⟩
57 
58 theorem left_mem_intersection (ι : K →* G) (g : G) (x : pairs ι g) :
59     left ι g x ∈ intersection ι g := by
60   exact ⟨x.val.2, x.property⟩
61 
62 theorem left_range (ι : K →* G) (g : G) :
63     (left ι g).range = intersection ι g := by
64   apply le_antisymm
65   · rintro a ⟨x, rfl⟩
66     exact left_mem_intersection ι g x
67   · intro a ha
68     rcases ha with ⟨b, hb⟩
69     exact ⟨⟨(a, b), hb⟩, rfl⟩
70 
71 theorem left_injective (ι : K →* G) (g : G) (hι : Function.Injective ι) :
72     Function.Injective (left ι g) := by
73   intro x y hxy
74   apply Subtype.ext
75   apply Prod.ext
76   · exact hxy
77   · apply hι
78     exact x.property.trans ((congrArg ((MulAut.conj g).toMonoidHom ∘ ι) hxy).trans
79       y.property.symm)
80 
81 /-- The formal group equivalence retaining the first-coordinate orientation. -/
82 def pairEquivIntersection (ι : K →* G) (g : G) (hι : Function.Injective ι) :
83     pairs ι g ≃* intersection ι g :=
84   MulEquiv.ofBijective
85     ((left ι g).codRestrict (intersection ι g) (left_mem_intersection ι g))
86     ⟨fun x y hxy => left_injective ι g hι (congrArg Subtype.val hxy),
87       fun a => by
88         rcases a.property with ⟨b, hb⟩
89         exact ⟨⟨(a.val, b), hb⟩, rfl⟩⟩
90 
91 theorem pairSupport_eq_comap (ι : K →* G) (H : Subgroup K) (g : G)
92     (hι : Function.Injective ι) :
93     H.comap (left ι g) ⊓ H.comap (right ι g) =
94       (scalarIntersection ι H g).comap (left ι g) := by
95   ext x
96   constructor
97   · intro hx
98     exact ⟨hx.1, ⟨right ι g x, hx.2, x.property⟩⟩
99   · intro hx
100     rcases hx.2 with ⟨b, hb, he⟩
101     have hbr : b = right ι g x := hι (he.trans x.property.symm)
102     exact ⟨hx.1, show right ι g x ∈ H from hbr ▸ hb⟩
103 
104 /-- The exact transport from the pair-support index to `[I:C]`.
105 It also holds when one of the indices is infinite (represented by zero). -/
106 theorem pairSupport_index (ι : K →* G) (H : Subgroup K) (g : G)
107     (hι : Function.Injective ι) :
108     (H.comap (left ι g) ⊓ H.comap (right ι g)).index =
109       (scalarIntersection ι H g).relIndex (intersection ι g) := by
110   rw [pairSupport_eq_comap ι H g hι, Subgroup.index_comap, left_range]
111 
112 /-- The same index may be expressed in the literal ambient intersections. -/
113 theorem pairSupport_index_ambient (ι : K →* G) (H : Subgroup K) (g : G)
114     (hι : Function.Injective ι) :
115     (H.comap (left ι g) ⊓ H.comap (right ι g)).index =
116       (H.map ι ⊓ (H.map ι).comap (MulAut.conj g).toMonoidHom).relIndex
117         (ι.range ⊓ ι.range.comap (MulAut.conj g).toMonoidHom) := by
118   rw [pairSupport_index ι H g hι, ← scalarIntersection_image,
119     ← intersection_image]
120   exact (Subgroup.relIndex_map_map_of_injective _ _ hι).symm
121 
122 end PaperXI.PairIndex110

Back to source controls