CompletedPaperCapstone.lean

1 import PaperXII.CompletedLocalConditions
2 import PaperXII.CompletedGlobalQuotient
3 
4 /-!
5 # Manuscript-level completion of Claims 3.1 and 3.3
6 
7 Noetherian hypotheses supply finite generation, and the local global map
8 supplies the ideal bound. Neither is a new arithmetic existence input.
9 The scalar and local-point conclusions are retained explicitly.
10 -/
11 noncomputable section
12 set_option autoImplicit false
13 namespace PaperXII.CompletedLocalConditions
14 
15 variable {O ι k : Type*} [CommRing O] [Fintype ι] [DecidableEq ι]
16   [Field k] [Algebra O k]
17 variable (R : ι → Type*) [∀ i, CommRing (R i)] [∀ i, Algebra O (R i)]
18 variable (res : ∀ i, R i →ₐ[O] k) (hO : Function.Surjective (algebraMap O k))
19 variable [IsNoetherianRing O] [∀ i, IsNoetherianRing (R i)]
20 
21 include hO in
22 /-- The ideal defining the actual local tensor topology is its maximal ideal. -/
23 theorem localIdeal_eq_maximalIdeal :
24     haveI := FiniteTensor.completedTensor_isLocalRing_noetherian R res hO
25     localIdeal R (RingHom.ker (algebraMap O k)) (fun i ↦ RingHom.ker (res i)) =
26       IsLocalRing.maximalIdeal (LocalTensor R (RingHom.ker (algebraMap O k))
27         (fun i ↦ RingHom.ker (res i))) := by
28   have hm := FiniteTensor.residueIdeal_isMaximal R res hO
29   exact (AdicModel.completed_maximalIdeal _ (FiniteTensor.definingIdeal_fg R _ _
30     (Ideal.fg_of_isNoetherianRing _) (fun _i ↦ Ideal.fg_of_isNoetherianRing _))).symm
31 
32 variable (I : ∀ i, Ideal (R i))
33 variable {B : Type*} [CommRing B]
34   [Algebra (LocalTensor R (RingHom.ker (algebraMap O k)) (fun i ↦ RingHom.ker (res i))) B]
35   [IsLocalRing B]
36   [IsLocalHom (algebraMap (LocalTensor R (RingHom.ker (algebraMap O k))
37     (fun i ↦ RingHom.ker (res i))) B)]
38 
39 include hO in
40 /-- A local global coefficient map automatically respects the required adic ideals. -/
41 theorem local_map_ideal_bound :
42     (localIdeal R (RingHom.ker (algebraMap O k)) (fun i ↦ RingHom.ker (res i))).map
43       (algebraMap (LocalTensor R (RingHom.ker (algebraMap O k))
44         (fun i ↦ RingHom.ker (res i))) B) ≤ IsLocalRing.maximalIdeal B := by
45   have := FiniteTensor.completedTensor_isLocalRing_noetherian R res hO
46   rw [localIdeal_eq_maximalIdeal R res hO]
47   exact IsLocalRing.map_maximalIdeal_le _
48 
49 variable [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B]
50 variable {P : Type*} [CommRing P] [UniformSpace P] [IsUniformAddGroup P]
51   [IsTopologicalRing P] [CompleteSpace P] [T2Space P]
52 
53 omit [IsUniformAddGroup B] in
54 include hO in
55 /-- Claim 3.3 at the manuscript's Noetherian and local-map boundary. -/
56 theorem global_base_change_noetherian (hB : IsAdic (IsLocalRing.maximalIdeal B))
57     (p : B →+* P) (hp : Continuous p) :
58     (∃! g : GlobalRing R (RingHom.ker (algebraMap O k))
59       (fun i ↦ RingHom.ker (res i)) I (IsLocalRing.maximalIdeal B) →+* P,
60       Continuous g ∧ g.comp (globalMap R (RingHom.ker (algebraMap O k))
61         (fun i ↦ RingHom.ker (res i)) I (IsLocalRing.maximalIdeal B)) = p) ↔
62       ∀ i, I i ≤ RingHom.ker ((p.comp (algebraMap (LocalTensor R
63         (RingHom.ker (algebraMap O k)) (fun i ↦ RingHom.ker (res i))) B)).comp
64           (FiniteTensor.completedInclude R (RingHom.ker (algebraMap O k))
65             (fun i ↦ RingHom.ker (res i)) i).toRingHom) :=
66   global_base_change R _ _ I _ (Ideal.fg_of_isNoetherianRing _)
67     (fun _i ↦ Ideal.fg_of_isNoetherianRing _) hB (local_map_ideal_bound R res hO) p hp
68 
69 end PaperXII.CompletedLocalConditions

Back to source controls