CompletedPointCategory.lean

1 import PaperXII.CompletedPaperCapstone
2 
3 /-! The point equivalence respects both locality and the base coefficient algebra. -/
4 noncomputable section
5 set_option autoImplicit false
6 namespace PaperXII.CompletedLocalConditions
7 
8 variable {O ι : Type*} [CommRing O] [Fintype ι] [DecidableEq ι]
9 variable (R : ι → Type*) [∀ i, CommRing (R i)] [∀ i, Algebra O (R i)]
10 variable (mO : Ideal O) (m : ∀ i, Ideal (R i)) (I : ∀ i, Ideal (R i))
11 variable {B : Type*} [CommRing B] [Algebra (LocalTensor R mO m) B] (mB : Ideal B)
12 variable [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B] [CompleteSpace B]
13 
14 /-- The actual global map is surjective for a complete global coefficient ring. -/
15 theorem globalMap_surjective (hB : IsAdic mB)
16     (h : (localIdeal R mO m).map (algebraMap (LocalTensor R mO m) B) ≤ mB) :
17     Function.Surjective (globalMap R mO m I mB) :=
18   CompletedBaseChange.transportedGlobalMap_surjective _ _ _ hB h
19     (quotientIdentification R mO m I)
20 
21 /-- The nonzero global completed tensor is a genuine local ring. -/
22 theorem globalRing_isLocalRing [IsLocalRing B] [Nontrivial (GlobalRing R mO m I mB)]
23     (hB : IsAdic mB)
24     (h : (localIdeal R mO m).map (algebraMap (LocalTensor R mO m) B) ≤ mB) :
25     IsLocalRing (GlobalRing R mO m I mB) :=
26   IsLocalRing.of_surjective' (globalMap R mO m I mB) (globalMap_surjective R mO m I mB hB h)
27 
28 /-- Every factor of a local point is local; no extra local-lifting datum is assumed. -/
29 theorem point_factor_isLocal {P : Type*} [CommRing P] (hB : IsAdic mB)
30     (h : (localIdeal R mO m).map (algebraMap (LocalTensor R mO m) B) ≤ mB)
31     (p : B →+* P) [IsLocalHom p] (g : GlobalRing R mO m I mB →+* P)
32     (hg : g.comp (globalMap R mO m I mB) = p) : IsLocalHom g :=
33   CompletedBaseChange.transported_factor_isLocal _ _ _ hB h
34     (quotientIdentification R mO m I) p g hg
35 
36 variable [Algebra O B]
37 
38 /-- The canonical coefficient algebra is the actual composite through the global map. -/
39 @[instance_reducible] def globalCoefficientAlgebra : Algebra O (GlobalRing R mO m I mB) :=
40   ((globalMap R mO m I mB).comp (algebraMap O B)).toAlgebra
41 attribute [local instance] globalCoefficientAlgebra
42 
43 /-- The canonical global map respects the chosen coefficient algebra. -/
44 def globalAlgMap : B →ₐ[O] GlobalRing R mO m I mB where
45   __ := globalMap R mO m I mB
46   commutes' _ := rfl
47 
48 variable {P : Type*} [CommRing P] [Algebra O P] [UniformSpace P]
49   [IsUniformAddGroup P] [IsTopologicalRing P] [CompleteSpace P] [T2Space P]
50 
51 /-- Claim 3.3 as an equivalence of continuous local algebra points. -/
52 theorem local_algebra_point_iff (fgO : mO.FG) (fg : ∀ i, (m i).FG)
53     (hB : IsAdic mB)
54     (h : (localIdeal R mO m).map (algebraMap (LocalTensor R mO m) B) ≤ mB)
55     (p : B →ₐ[O] P) [IsLocalHom p.toRingHom] (hp : Continuous p) :
56     (∃! g : GlobalRing R mO m I mB →ₐ[O] P,
57       Continuous g ∧ IsLocalHom g.toRingHom ∧ g.comp (globalAlgMap R mO m I mB) = p) ↔
58         ∀ i, I i ≤ RingHom.ker ((p.toRingHom.comp (algebraMap (LocalTensor R mO m) B)).comp
59           (FiniteTensor.completedInclude R mO m i).toRingHom) := by
60   constructor
61   · rintro ⟨g, ⟨hg, _, hgp⟩, _⟩
62     apply (global_base_change R mO m I mB fgO fg hB h p.toRingHom hp).mp
63     refine ⟨g.toRingHom, ⟨hg, ?_⟩, ?_⟩
64     · exact congrArg AlgHom.toRingHom hgp
65     · intro g' hg'
66       ext x
67       obtain ⟨b, rfl⟩ := globalMap_surjective R mO m I mB hB h x
68       exact (DFunLike.congr_fun hg'.2 b).trans
69         (DFunLike.congr_fun (congrArg AlgHom.toRingHom hgp) b).symm
70   · intro hI
71     obtain ⟨g, ⟨hg, hgp⟩, hu⟩ :=
72       (global_base_change R mO m I mB fgO fg hB h p.toRingHom hp).mpr hI
73     let ga : GlobalRing R mO m I mB →ₐ[O] P :=
74       { __ := g
75         commutes' := fun a ↦ (DFunLike.congr_fun hgp (algebraMap O B a)).trans (p.commutes a) }
76     refine ⟨ga, ⟨hg, point_factor_isLocal R mO m I mB hB h p.toRingHom g hgp, ?_⟩, ?_⟩
77     · exact AlgHom.ext (fun b ↦ DFunLike.congr_fun hgp b)
78     · intro g' hg'
79       apply AlgHom.ext
80       intro x
81       exact DFunLike.congr_fun (hu g'.toRingHom ⟨hg'.1, congrArg AlgHom.toRingHom hg'.2.2⟩) x
82 
83 omit [UniformSpace P] [IsUniformAddGroup P] [IsTopologicalRing P] [CompleteSpace P] [T2Space P] in
84 /-- The point factorization is natural under coefficient-preserving target maps. -/
85 theorem algebra_factor_natural {Q : Type*} [CommRing Q] [Algebra O Q]
86     (hB : IsAdic mB)
87     (h : (localIdeal R mO m).map (algebraMap (LocalTensor R mO m) B) ≤ mB)
88     (p : B →ₐ[O] P) (u : P →ₐ[O] Q)
89     (g : GlobalRing R mO m I mB →ₐ[O] P)
90     (g' : GlobalRing R mO m I mB →ₐ[O] Q)
91     (hg : g.comp (globalAlgMap R mO m I mB) = p)
92     (hg' : g'.comp (globalAlgMap R mO m I mB) = u.comp p) :
93     u.comp g = g' := by
94   ext x
95   obtain ⟨b, rfl⟩ := globalMap_surjective R mO m I mB hB h x
96   change u (g (globalMap R mO m I mB b)) = g' (globalMap R mO m I mB b)
97   have hgb : g (globalMap R mO m I mB b) = p b := DFunLike.congr_fun hg b
98   have hg'b : g' (globalMap R mO m I mB b) = u (p b) := DFunLike.congr_fun hg' b
99   rw [hgb, hg'b]
100 
101 end PaperXII.CompletedLocalConditions

Back to source controls