CompletedLocalConditions.lean

1 import PaperXII.CompletedTensorUniversal
2 import PaperXII.CompletedBaseChangeTransport
3 
4 /-!
5 # The completed local-to-global quotient theorem
6 
7 The local-condition ring is the actual finite completed tensor of the factor
8 quotients. Its action by the local tensor ring is constructed from the proved
9 Claim 3.1 equivalence, not supplied as an identification hypothesis.
10 -/
11 noncomputable section
12 open UniformSpace
13 set_option autoImplicit false
14 namespace PaperXII.CompletedLocalConditions
15 
16 variable {O ι : Type*} [CommRing O] [Fintype ι] [DecidableEq ι]
17 variable (R : ι → Type*) [∀ i, CommRing (R i)] [∀ i, Algebra O (R i)]
18 variable (mO : Ideal O) (m : ∀ i, Ideal (R i)) (I : ∀ i, Ideal (R i))
19 
20 abbrev LocalTensor := FiniteTensor.CompletedTensor R mO m
21 abbrev Conditions := FiniteTensor.CompletedTensor (fun i ↦ R i ⧸ I i) mO
22   (fun i ↦ (m i).map (Ideal.Quotient.mk (I i)))
23 abbrev closedIdeal := FiniteTensor.closedConditions R mO m I
24 abbrev localIdeal := (FiniteTensor.definingIdeal R mO m).map
25   (FiniteTensor.tensorEmbed R mO m).toRingHom
26 
27 /-- The actual condition tensor receives the canonical local quotient action. -/
28 instance conditionAlgebra : Algebra (LocalTensor R mO m) (Conditions R mO m I) :=
29   ((FiniteTensor.completedQuotientEquiv R mO m I).toRingHom.comp
30     (Ideal.Quotient.mk (closedIdeal R mO m I))).toAlgebra
31 
32 /-- Claim 3.1 upgraded to the local-tensor coefficient algebra. -/
33 def quotientIdentification : (LocalTensor R mO m ⧸ closedIdeal R mO m I) ≃ₐ[LocalTensor R mO m]
34     Conditions R mO m I where
35   __ := FiniteTensor.completedQuotientEquiv R mO m I
36   commutes' _ := rfl
37 
38 /-- The transported ideal is exactly the one defining the actual condition tensor topology. -/
39 theorem quotientIdentification_ideal :
40     ((localIdeal R mO m).map (Ideal.Quotient.mk (closedIdeal R mO m I))).map
41       (quotientIdentification R mO m I).toRingHom =
42         (FiniteTensor.definingIdeal (fun i ↦ R i ⧸ I i) mO
43           (fun i ↦ (m i).map (Ideal.Quotient.mk (I i)))).map
44             (FiniteTensor.tensorEmbed (fun i ↦ R i ⧸ I i) mO
45               (fun i ↦ (m i).map (Ideal.Quotient.mk (I i)))).toRingHom := by
46   simp only [localIdeal, Ideal.map_map]
47   have hcomp : (quotientIdentification R mO m I).toRingHom.comp
48       ((Ideal.Quotient.mk (closedIdeal R mO m I)).comp (FiniteTensor.tensorEmbed R mO m).toRingHom) =
49         (FiniteTensor.tensorEmbed (fun i ↦ R i ⧸ I i) mO
50           (fun i ↦ (m i).map (Ideal.Quotient.mk (I i)))).toRingHom.comp
51             (FiniteTensor.quotientMap R I).toRingHom := by
52     ext x
53     exact FiniteTensor.completedQuotientEquiv_mk_embed R mO m I x
54   rw [hcomp, ← Ideal.map_map, FiniteTensor.quotientMap_definingIdeal]
55 
56 variable {B : Type*} [CommRing B] [Algebra (LocalTensor R mO m) B]
57   (mB : Ideal B)
58 
59 /-- The actual completed global tensor with the independently constructed condition tensor. -/
60 abbrev GlobalRing := CompletedBaseChange.Transported (localIdeal R mO m) mB
61   (closedIdeal R mO m I) (quotientIdentification R mO m I)
62 
63 def globalMap : B →+* GlobalRing R mO m I mB :=
64   CompletedBaseChange.transportedGlobalMap (localIdeal R mO m) mB
65     (closedIdeal R mO m I) (quotientIdentification R mO m I)
66 
67 /-- The defining construction provides genuine completeness and separation. -/
68 theorem globalRing_complete : CompleteSpace (GlobalRing R mO m I mB) ∧
69     T2Space (GlobalRing R mO m I mB) := ⟨inferInstance, inferInstance⟩
70 
71 variable [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B]
72 variable {P : Type*} [CommRing P] [UniformSpace P] [IsUniformAddGroup P]
73   [IsTopologicalRing P] [CompleteSpace P] [T2Space P]
74 
75 omit [IsUniformAddGroup B] in
76 /-- Full Claim 3.3: the named completed base change imposes exactly all local conditions. -/
77 theorem global_base_change (fgO : mO.FG) (fg : ∀ i, (m i).FG) (hB : IsAdic mB)
78     (h : (localIdeal R mO m).map (algebraMap (LocalTensor R mO m) B) ≤ mB)
79     (p : B →+* P) (hp : Continuous p) :
80     (∃! g : GlobalRing R mO m I mB →+* P,
81       Continuous g ∧ g.comp (globalMap R mO m I mB) = p) ↔
82         ∀ i, I i ≤ RingHom.ker ((p.comp (algebraMap (LocalTensor R mO m) B)).comp
83           (FiniteTensor.completedInclude R mO m i).toRingHom) := by
84   have hp' : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom) :=
85     hp.comp (AdicModel.continuous_of_map_le (AdicModel.carrier_isAdic B mB) hB
86       (AdicModel.rawEquiv B mB).toRingHom (by
87         change mB.map (RingHom.id B) ≤ mB
88         simp))
89   refine (CompletedBaseChange.transported_exists_unique_factor_iff (localIdeal R mO m) mB
90     (closedIdeal R mO m I) (quotientIdentification R mO m I) h p hp').trans ?_
91   change FiniteTensor.closedConditions R mO m I ≤ RingHom.ker
92     (p.comp (algebraMap (LocalTensor R mO m) B)) ↔ _
93   rw [FiniteTensor.closedConditions_eq]
94   apply LocalQuotients.closed_conditions_iff R
95     (fun i ↦ (FiniteTensor.completedInclude R mO m i).toRingHom) I
96   exact hp.comp (AdicModel.continuous_of_map_le
97     (FiniteTensor.completedTensor_isAdic R mO m fgO fg) hB
98       (algebraMap (LocalTensor R mO m) B) h)
99 
100 end PaperXII.CompletedLocalConditions

Back to source controls