CompletedTensorUniversal.lean

1 import PaperXII.FiniteTensorLocality
2 
3 /-! The actual completed tensor has the required continuous local-map universal
4 property. The extension is constructed by uniform completion, with uniqueness
5 proved by density and finite tensor extensionality. -/
6 noncomputable section
7 open UniformSpace
8 set_option autoImplicit false
9 namespace PaperXII.FiniteTensor
10 
11 variable {O ι : Type*} [CommRing O] [Fintype ι] [DecidableEq ι]
12 variable (R : ι → Type*) [∀ i, CommRing (R i)] [∀ i, Algebra O (R i)]
13 variable (mO : Ideal O) (m : ∀ i, Ideal (R i))
14 variable {P : Type*} [CommRing P] [Algebra O P] [UniformSpace P] [IsUniformAddGroup P]
15   [IsTopologicalRing P] [CompleteSpace P] [T2Space P]
16 variable (mP : Ideal P) (hP : IsAdic mP) (f : ∀ i, R i →ₐ[O] P)
17   (hO : mO.map (algebraMap O P) ≤ mP) (hf : ∀ i, (m i).map (f i).toRingHom ≤ mP)
18 
19 omit [UniformSpace P] [IsUniformAddGroup P] [IsTopologicalRing P] [CompleteSpace P] [T2Space P] in
20 include hO hf in
21 /-- Local ideal control extends from the factors to the actual algebraic tensor. -/
22 theorem liftFamily_definingIdeal : (definingIdeal R mO m).map (liftFamily R f).toRingHom ≤ mP := by
23   rw [definingIdeal, Ideal.map_sup, sup_le_iff, Ideal.map_map]
24   constructor
25   · have he : (liftFamily R f).toRingHom.comp (algebraMap O (Raw (O := O) R)) =
26         algebraMap O P := by ext a; exact (liftFamily R f).commutes a
27     rw [he]
28     exact hO
29   · rw [conditions, Ideal.map_iSup, iSup_le_iff]
30     intro i
31     rw [Ideal.map_map]
32     have he : (liftFamily R f).toRingHom.comp (includeFactor R i).toRingHom = (f i).toRingHom := by
33       ext x; exact liftFamily_include R f i x
34     rw [he]
35     exact hf i
36 
37 omit [IsUniformAddGroup P] [CompleteSpace P] [T2Space P] in
38 include hP hO hf in
39 /-- The raw universal map is continuous for the literal ideal-adic topology. -/
40 theorem liftFamily_continuous :
41     Continuous ((liftFamily R f).toRingHom.comp (AdicModel.rawEquiv _ _).toRingHom :
42       AdicModel.Carrier (Raw (O := O) R) (definingIdeal R mO m) →+* P) := by
43   apply AdicModel.continuous_of_map_le (AdicModel.carrier_isAdic _ _) hP
44   exact liftFamily_definingIdeal R mO m mP f hO hf
45 
46 /-- The actual continuous extension of the factor algebra maps. -/
47 def completedLift : CompletedTensor R mO m →ₐ[O] P where
48   __ := Completion.extensionHom
49     ((liftFamily R f).toRingHom.comp (AdicModel.rawEquiv _ _).toRingHom)
50       (liftFamily_continuous R mO m mP hP f hO hf)
51   commutes' a := by
52     change Completion.extensionHom _ _
53       (AdicModel.embed _ _ (algebraMap O (Raw (O := O) R) a)) = _
54     exact (Completion.extensionHom_coe _ _ ((AdicModel.rawEquiv _ _).symm
55       (algebraMap O (Raw (O := O) R) a))).trans ((liftFamily R f).commutes a)
56 
57 theorem completedLift_continuous : Continuous (completedLift R mO m mP hP f hO hf) :=
58   Completion.continuous_extension
59 
60 @[simp] theorem completedLift_embed (x : Raw (O := O) R) :
61     completedLift R mO m mP hP f hO hf (tensorEmbed R mO m x) = liftFamily R f x :=
62   Completion.extensionHom_coe
63     ((liftFamily R f).toRingHom.comp (AdicModel.rawEquiv _ _).toRingHom)
64     (liftFamily_continuous R mO m mP hP f hO hf) ((AdicModel.rawEquiv _ _).symm x)
65 
66 @[simp] theorem completedLift_factor (i : ι) (x : R i) :
67     completedLift R mO m mP hP f hO hf (completedInclude R mO m i x) = f i x := by
68   change completedLift R mO m mP hP f hO hf (tensorEmbed R mO m (includeFactor R i x)) = _
69   rw [completedLift_embed, liftFamily_include]
70 
71 omit [IsUniformAddGroup P] [IsTopologicalRing P] [CompleteSpace P] in
72 /-- Uniqueness follows on the actual completion, rather than being an input interface. -/
73 theorem completedTensor_hom_ext {g h : CompletedTensor R mO m →ₐ[O] P}
74     (hg : Continuous g) (hh : Continuous h)
75     (he : ∀ i, g.comp (completedInclude R mO m i) = h.comp (completedInclude R mO m i)) : g = h := by
76   have hr : g.comp (tensorEmbed R mO m) = h.comp (tensorEmbed R mO m) := by
77     apply hom_ext
78     exact he
79   apply AlgHom.ext
80   intro x
81   refine Completion.induction_on x (isClosed_eq hg hh) ?_
82   intro r
83   exact DFunLike.congr_fun hr (AdicModel.rawEquiv _ _ r)
84 
85 include hP hO hf in
86 /-- Existence and uniqueness of the continuous algebra map specified by the local factors. -/
87 theorem exists_unique_completedLift :
88     ∃! g : CompletedTensor R mO m →ₐ[O] P,
89       Continuous g ∧ ∀ i, g.comp (completedInclude R mO m i) = f i := by
90   refine ⟨completedLift R mO m mP hP f hO hf, ⟨completedLift_continuous .., ?_⟩, ?_⟩
91   · intro i; ext x; exact completedLift_factor R mO m mP hP f hO hf i x
92   · intro g hg
93     apply completedTensor_hom_ext R mO m hg.1 (completedLift_continuous ..)
94     intro i
95     rw [hg.2 i]
96     ext x
97     exact (completedLift_factor R mO m mP hP f hO hf i x).symm
98 
99 end PaperXII.FiniteTensor

Back to source controls