DirectSumEndomorphisms.lean

1 import RealizationBoundaries.DiagonalRealization
2 import RealizationBoundaries.CompletionConsequences
3 
4 /-! # The endomorphism ring of the original finite-support subgroup -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace RealizationBoundaries
8 
9 /-- Every coordinate family restricts to the actual finite-support subgroup. -/
10 def finiteSupportDiagonal (c : Ambient) : AddMonoid.End finiteSupport where
11   toFun x := ⟨diagonal c x.val, diagonal_finiteSupport c x.val x.property⟩
12   map_zero' := Subtype.ext (map_zero (diagonal c))
13   map_add' x y := Subtype.ext (map_add (diagonal c) x.val y.val)
14 
15 @[simp] theorem finiteSupportDiagonal_apply (c : Ambient) (x : finiteSupport) (p : Prime) :
16     (finiteSupportDiagonal c x).val p = c p * x.val p := rfl
17 
18 /-- Multiplication in the source is coordinatewise; multiplication in the target is composition. -/
19 def finiteSupportDiagonalRing : Ambient →+* AddMonoid.End finiteSupport where
20   toFun := finiteSupportDiagonal
21   map_zero' := by
22     apply AddMonoidHom.ext
23     intro x
24     apply Subtype.ext
25     funext p
26     exact zero_mul (x.val p)
27   map_one' := by
28     apply AddMonoidHom.ext
29     intro x
30     apply Subtype.ext
31     funext p
32     exact one_mul (x.val p)
33   map_add' c d := by
34     apply AddMonoidHom.ext
35     intro x
36     apply Subtype.ext
37     exact diagonal_add c d x.val
38   map_mul' c d := by
39     apply AddMonoidHom.ext
40     intro x
41     apply Subtype.ext
42     exact diagonal_mul c d x.val
43 
44 theorem finiteSupportDiagonalRing_bijective : Function.Bijective finiteSupportDiagonalRing := by
45   constructor
46   · intro c d h
47     funext p
48     have he := congrArg (fun f : AddMonoid.End finiteSupport => (f (primeSeed p)).val p) h
49     classical
50     change c p * (primeSeed p).val p = d p * (primeSeed p).val p at he
51     simpa [primeSeed, cut] using he
52   · intro f
53     let e := bottomFiniteSupportEquiv
54     let g : preimage (⊥ : Submodule ℚ TailSpace) →+
55         preimage (⊥ : Submodule ℚ TailSpace) :=
56       e.symm.toAddMonoidHom.comp (f.comp e.toAddMonoidHom)
57     refine ⟨homDiagonal ⊥ ⊥ g, ?_⟩
58     apply AddMonoidHom.ext
59     intro x
60     apply Subtype.ext
61     exact (hom_eq_diagonal ⊥ ⊥ g (e.symm x)).symm
62 
63 /-- Monograph Proposition 2.2: the original direct-sum endomorphism ring, not a proxy. -/
64 def finiteSupportEndomorphismRingEquiv : AddMonoid.End finiteSupport ≃+* Ambient :=
65   (RingEquiv.ofBijective finiteSupportDiagonalRing finiteSupportDiagonalRing_bijective).symm
66 
67 /-- No arbitrary endomorphism of D can introduce a missing prime coordinate. -/
68 theorem finiteSupport_endomorphism_coordinate (f : AddMonoid.End finiteSupport)
69     (x : finiteSupport) (p : Prime) :
70     (f x).val p = finiteSupportEndomorphismRingEquiv f p * x.val p := by
71   have he : finiteSupportDiagonalRing (finiteSupportEndomorphismRingEquiv f) = f :=
72     (RingEquiv.ofBijective finiteSupportDiagonalRing
73       finiteSupportDiagonalRing_bijective).apply_symm_apply f
74   exact (congrArg (fun g : AddMonoid.End finiteSupport => (g x).val p) he).symm
75 
76 theorem finiteSupport_endomorphism_preserves_zero (f : AddMonoid.End finiteSupport)
77     (x : finiteSupport) (p : Prime) (hx : x.val p = 0) : (f x).val p = 0 := by
78   rw [finiteSupport_endomorphism_coordinate, hx, mul_zero]
79 
80 end RealizationBoundaries

Back to source controls