CompletedFiniteTensor.lean

1 import PaperXII.AdicQuotientTopology
2 import PaperXII.FiniteTensorQuotient
3 
4 /-!
5 # Completed tensor products of finite families and quotients
6 
7 The objects are the actual Hausdorff completions of the actual finite algebraic
8 tensor products, with the topology defined by the base ideal and the factor ideals.
9 The base term includes the empty family without replacing the base-adic topology
10 by the discrete topology. No completeness or quotient-comparison interface is assumed.
11 -/
12 noncomputable section
13 open Filter Topology UniformSpace
14 open scoped Uniformity
15 set_option autoImplicit false
16 namespace PaperXII.FiniteTensor
17 
18 variable {O ι : Type*} [CommRing O] [Fintype ι] [DecidableEq ι]
19 variable (R : ι → Type*) [∀ i, CommRing (R i)] [∀ i, Algebra O (R i)]
20 variable (mO : Ideal O) (m : ∀ i, Ideal (R i))
21 
22 /-- The actual finite completed tensor product. -/
23 abbrev CompletedTensor := AdicModel.Completed (Raw (O := O) R) (definingIdeal R mO m)
24 
25 /-- The algebra structure is induced by the canonical dense embedding. -/
26 instance completedTensorAlgebra : Algebra O (CompletedTensor R mO m) :=
27   ((AdicModel.embed (Raw (O := O) R) (definingIdeal R mO m)).comp
28     (algebraMap O (Raw (O := O) R))).toAlgebra
29 
30 /-- Actual dense tensor inclusion, as an algebra homomorphism. -/
31 def tensorEmbed : Raw (O := O) R →ₐ[O] CompletedTensor R mO m where
32   __ := AdicModel.embed (Raw (O := O) R) (definingIdeal R mO m)
33   commutes' _ := rfl
34 
35 /-- Actual completed factor map. -/
36 def completedInclude (i : ι) : R i →ₐ[O] CompletedTensor R mO m :=
37   (tensorEmbed R mO m).comp (includeFactor R i)
38 
39 /-- The closed ideal generated by all the supplied local condition ideals. -/
40 def closedConditions (J : ∀ i, Ideal (R i)) : Ideal (CompletedTensor R mO m) :=
41   CompletionQuotient.closedExtension
42     (AdicModel.carrierIdeal (definingIdeal R mO m) (conditions R J))
43 
44 omit [Fintype ι] in
45 /-- This is precisely the literal closed ideal of the completed factor images. -/
46 theorem closedConditions_eq (J : ∀ i, Ideal (R i)) :
47     closedConditions R mO m J =
48       (⨆ i, (J i).map (completedInclude R mO m i).toRingHom).closure := by
49   simp only [closedConditions, CompletionQuotient.closedExtension, AdicModel.carrierIdeal,
50     conditions, Ideal.map_iSup, Ideal.map_map]
51   rfl
52 
53 instance closedConditions_isClosed (J : ∀ i, Ideal (R i)) :
54     IsClosed (closedConditions R mO m J : Set (CompletedTensor R mO m)) := isClosed_closure
55 
56 variable (J : ∀ i, Ideal (R i))
57 
58 /-- The full actual completed tensor quotient comparison, in the construction direction. -/
59 def completedQuotientEquiv :
60     (CompletedTensor R mO m ⧸ closedConditions R mO m J) ≃+*
61       CompletedTensor (fun i ↦ R i ⧸ J i) mO
62         (fun i ↦ (m i).map (Ideal.Quotient.mk (J i))) :=
63   (AdicModel.quotientCompletionEquiv (definingIdeal R mO m) (conditions R J)).trans
64     (AdicModel.completedEquiv _ _ (quotientEquiv R J).toRingEquiv
65       (quotientEquiv_definingIdeal R J mO m))
66 
67 theorem completedQuotientEquiv_continuous :
68     Continuous (completedQuotientEquiv R mO m J) :=
69   (AdicModel.completedEquiv_continuous _ _ (quotientEquiv R J).toRingEquiv
70     (quotientEquiv_definingIdeal R J mO m)).comp
71     (AdicModel.quotientCompletionEquiv_continuous (definingIdeal R mO m) (conditions R J))
72 
73 theorem completedQuotientEquiv_symm_continuous :
74     Continuous (completedQuotientEquiv R mO m J).symm :=
75   (AdicModel.quotientCompletionEquiv_symm_continuous (definingIdeal R mO m) (conditions R J)).comp
76     (AdicModel.completedEquiv_symm_continuous _ _ (quotientEquiv R J).toRingEquiv
77       (quotientEquiv_definingIdeal R J mO m))
78 
79 @[simp] theorem completedQuotientEquiv_mk_embed (x : Raw (O := O) R) :
80     completedQuotientEquiv R mO m J (Ideal.Quotient.mk _ (tensorEmbed R mO m x)) =
81       tensorEmbed (fun i ↦ R i ⧸ J i) mO
82         (fun i ↦ (m i).map (Ideal.Quotient.mk (J i))) (quotientMap R J x) := by
83   change AdicModel.completedEquiv _ _ (quotientEquiv R J).toRingEquiv
84     (quotientEquiv_definingIdeal R J mO m)
85       (AdicModel.quotientCompletionEquiv _ _ (Ideal.Quotient.mk _ (AdicModel.embed _ _ x))) = _
86   rw [AdicModel.quotientCompletionEquiv_mk_embed, AdicModel.completedEquiv_embed]
87   rfl
88 
89 /-- Claim 3.1 with the source's displayed direction and its coefficient-algebra structure. -/
90 def completed_tensor_quotient :
91     CompletedTensor (fun i ↦ R i ⧸ J i) mO
92       (fun i ↦ (m i).map (Ideal.Quotient.mk (J i))) ≃ₐ[O]
93       (CompletedTensor R mO m ⧸ closedConditions R mO m J) :=
94   (show (CompletedTensor R mO m ⧸ closedConditions R mO m J) ≃ₐ[O]
95       CompletedTensor (fun i ↦ R i ⧸ J i) mO
96         (fun i ↦ (m i).map (Ideal.Quotient.mk (J i))) from
97     { __ := completedQuotientEquiv R mO m J
98       commutes' r := by
99         change completedQuotientEquiv R mO m J
100           (Ideal.Quotient.mk _ (tensorEmbed R mO m (algebraMap O (Raw (O := O) R) r))) = _
101         rw [completedQuotientEquiv_mk_embed, (quotientMap R J).commutes]
102         rfl }).symm
103 
104 /-- Both maps of the completed tensor quotient equivalence are continuous. -/
105 theorem completed_tensor_quotient_continuous :
106     Continuous (completed_tensor_quotient R mO m J) ∧
107       Continuous (completed_tensor_quotient R mO m J).symm :=
108   ⟨completedQuotientEquiv_symm_continuous R mO m J,
109     completedQuotientEquiv_continuous R mO m J⟩
110 
111 /-- The isomorphism respects every actual canonical factor map. -/
112 @[simp] theorem completed_tensor_quotient_factor (i : ι) (x : R i) :
113     completed_tensor_quotient R mO m J
114       (completedInclude (fun i ↦ R i ⧸ J i) mO
115         (fun i ↦ (m i).map (Ideal.Quotient.mk (J i))) i (Ideal.Quotient.mk (J i) x)) =
116       Ideal.Quotient.mk _ (completedInclude R mO m i x) := by
117   apply (completedQuotientEquiv R mO m J).injective
118   change completedQuotientEquiv R mO m J
119     ((completedQuotientEquiv R mO m J).symm _) = _
120   rw [RingEquiv.apply_symm_apply]
121   symm
122   simpa only [quotientMap_include, completedInclude, AlgHom.comp_apply] using
123     completedQuotientEquiv_mk_embed R mO m J (includeFactor R i x)
124 
125 attribute [local instance] CompletionQuotient.quotientUniformSpace
126 
127 omit [Fintype ι] in
128 /-- The right-hand quotient is itself a genuine complete Hausdorff ring. -/
129 theorem completed_tensor_quotient_complete :
130     CompleteSpace (CompletedTensor R mO m ⧸ closedConditions R mO m J) ∧
131       T2Space (CompletedTensor R mO m ⧸ closedConditions R mO m J) :=
132   ⟨CompletionQuotient.quotient_complete _, inferInstance⟩
133 
134 end PaperXII.FiniteTensor

Back to source controls