CentralProductMap.lean

1 import PaperXI.CentralProduct
2 
3 /-! Actual maps and isomorphisms of the central quotients induced by compatible factor maps. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.CentralProduct
7 
8 variable {S Z : Type*} [Fintype S] [CommGroup Z]
9 variable {H A H' A' : S → Type*}
10 variable [∀ s, _root_.Group (H s)] [∀ s, CommGroup (A s)]
11 variable [∀ s, _root_.Group (H' s)] [∀ s, CommGroup (A' s)]
12 variable (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
13 variable (E : ∀ s, CentralExtension.Datum Z (H' s) (A' s))
14 
15 def ambientMap (f : ∀ s, H s →* H' s) :
16     Ambient (Z := Z) (H := H) →* Ambient (Z := Z) (H := H') where
17   toFun x := (x.1, fun s => f s (x.2 s))
18   map_one' := by ext <;> simp
19   map_mul' x y := by ext <;> simp
20 
21 def map (f : ∀ s, H s →* H' s)
22     (hf : ∀ s z, f s ((D s).i z) = (E s).i z) : Group D →* Group E :=
23   descend D ((mk E).comp (ambientMap f)) (by
24     intro z
25     change mk E ((∏ s, z s)⁻¹, fun s => f s ((D s).i (z s))) = 1
26     simp_rw [hf]
27     exact mk_balanced E z)
28 
29 @[simp] theorem map_mk (f : ∀ s, H s →* H' s)
30     (hf : ∀ s z, f s ((D s).i z) = (E s).i z)
31     (x : Ambient (Z := Z) (H := H)) :
32     map D E f hf (mk D x) = mk E (x.1, fun s => f s (x.2 s)) := rfl
33 
34 @[simp] theorem map_center (f : ∀ s, H s →* H' s)
35     (hf : ∀ s z, f s ((D s).i z) = (E s).i z) (z : Z) :
36     map D E f hf (center D z) = center E z := by
37   simp [center_apply]
38   rfl
39 
40 def congr (f : ∀ s, H s ≃* H' s)
41     (hf : ∀ s z, f s ((D s).i z) = (E s).i z) : Group D ≃* Group E where
42   toFun := map D E (fun s => (f s).toMonoidHom) hf
43   invFun := map E D (fun s => (f s).symm.toMonoidHom) (by
44     intro s z
45     apply (f s).injective
46     simpa using (hf s z).symm)
47   left_inv x := by
48     obtain ⟨x, rfl⟩ := mk_surjective D x
49     simp
50   right_inv x := by
51     obtain ⟨x, rfl⟩ := mk_surjective E x
52     simp
53   map_mul' x y := (map D E (fun s => (f s).toMonoidHom) hf).map_mul x y
54 
55 @[simp] theorem congr_mk (f : ∀ s, H s ≃* H' s)
56     (hf : ∀ s z, f s ((D s).i z) = (E s).i z)
57     (x : Ambient (Z := Z) (H := H)) :
58     congr D E f hf (mk D x) = mk E (x.1, fun s => f s (x.2 s)) := rfl
59 
60 @[simp] theorem congr_center (f : ∀ s, H s ≃* H' s)
61     (hf : ∀ s z, f s ((D s).i z) = (E s).i z) (z : Z) :
62     congr D E f hf (center D z) = center E z := map_center D E _ hf z
63 
64 end PaperXI.CentralProduct

Back to source controls