CompletedBaseChangeTransport.lean

1 import PaperXII.CompletedGlobalBaseChange
2 import Mathlib.RingTheory.TensorProduct.Maps
3 
4 /-! Transport to a separately constructed local-condition ring, using an actual
5 proved quotient equivalence. The final object is the completion of B ⊗[A] C. -/
6 noncomputable section
7 open UniformSpace
8 open scoped TensorProduct
9 set_option autoImplicit false
10 namespace PaperXII.CompletedBaseChange
11 
12 variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
13   [Algebra A B] [Algebra A C]
14 variable (mA : Ideal A) (mB : Ideal B) (J : Ideal A) (e : (A ⧸ J) ≃ₐ[A] C)
15 
16 def transportedIdeal : Ideal (B ⊗[A] C) :=
17   mB.map (algebraMap B (B ⊗[A] C)) ⊔
18     ((mA.map (Ideal.Quotient.mk J)).map e.toRingHom).map
19       (Algebra.TensorProduct.includeRight : C →ₐ[A] B ⊗[A] C).toRingHom
20 
21 abbrev Transported := AdicModel.Completed (B ⊗[A] C) (transportedIdeal mA mB J e)
22 
23 def transportedGlobalMap : B →+* Transported mA mB J e :=
24   (AdicModel.embed _ _).comp (algebraMap B (B ⊗[A] C))
25 
26 def rawTransport : Raw (B := B) J ≃ₐ[B] B ⊗[A] C :=
27   Algebra.TensorProduct.congr (AlgEquiv.refl : B ≃ₐ[B] B) e
28 
29 @[simp] theorem rawTransport_left (b : B) :
30     rawTransport (B := B) J e (algebraMap B (Raw (B := B) J) b) =
31       algebraMap B (B ⊗[A] C) b := AlgEquiv.commutes _ b
32 
33 @[simp] theorem rawTransport_right (a : A ⧸ J) :
34     rawTransport (B := B) J e
35       ((Algebra.TensorProduct.includeRight : A ⧸ J →ₐ[A] Raw (B := B) J) a) =
36         (Algebra.TensorProduct.includeRight : C →ₐ[A] B ⊗[A] C) (e a) := by
37   simp [rawTransport, Algebra.TensorProduct.includeRight_apply]
38 
39 theorem rawTransport_ideal :
40     (tensorIdeal mA mB J).map (rawTransport (B := B) J e).toRingHom =
41       transportedIdeal mA mB J e := by
42   have hl : (rawTransport (B := B) J e).toRingHom.comp (algebraMap B (Raw (B := B) J)) =
43       algebraMap B (B ⊗[A] C) := by ext b; exact rawTransport_left J e b
44   have hr : (rawTransport (B := B) J e).toRingHom.comp
45       (Algebra.TensorProduct.includeRight : A ⧸ J →ₐ[A] Raw (B := B) J).toRingHom =
46         (Algebra.TensorProduct.includeRight : C →ₐ[A] B ⊗[A] C).toRingHom.comp e.toRingHom := by
47     ext a; exact rawTransport_right J e a
48   simp only [tensorIdeal, transportedIdeal, Ideal.map_sup, Ideal.map_map]
49   rw [hl, ← RingHom.comp_assoc, hr]
50   rfl
51 
52 /-- The actual complete base changes are equivalent under the literal quotient identification. -/
53 def completedTransport : Completed mA mB J ≃+* Transported mA mB J e :=
54   AdicModel.completedEquiv _ _ (rawTransport (B := B) J e).toRingEquiv
55     (rawTransport_ideal mA mB J e)
56 
57 theorem completedTransport_continuous : Continuous (completedTransport mA mB J e) :=
58   AdicModel.completedEquiv_continuous _ _ _ (rawTransport_ideal mA mB J e)
59 
60 theorem completedTransport_symm_continuous : Continuous (completedTransport mA mB J e).symm :=
61   AdicModel.completedEquiv_symm_continuous _ _ _ (rawTransport_ideal mA mB J e)
62 
63 @[simp] theorem completedTransport_globalMap (b : B) :
64     completedTransport mA mB J e (globalMap mA mB J b) = transportedGlobalMap mA mB J e b := by
65   change AdicModel.completedEquiv _ _ _ (rawTransport_ideal mA mB J e)
66     (AdicModel.embed _ _ (algebraMap B (Raw (B := B) J) b)) = _
67   rw [AdicModel.completedEquiv_embed]
68   exact congrArg (AdicModel.embed _ _) (rawTransport_left J e b)
69 
70 variable {P : Type*} [CommRing P] [UniformSpace P] [IsUniformAddGroup P]
71   [IsTopologicalRing P] [CompleteSpace P] [T2Space P]
72 
73 /-- Transported factorization, including continuity and uniqueness, for the named local ring. -/
74 theorem transported_exists_unique_factor_iff (h : mA.map (algebraMap A B) ≤ mB)
75     (p : B →+* P) (hp : Continuous (p.comp (AdicModel.rawEquiv B mB).toRingHom)) :
76     (∃! g : Transported mA mB J e →+* P,
77       Continuous g ∧ g.comp (transportedGlobalMap mA mB J e) = p) ↔
78         J ≤ RingHom.ker (p.comp (algebraMap A B)) := by
79   constructor
80   · rintro ⟨g, ⟨_, hp'⟩, _⟩
81     change J ≤ (RingHom.ker p).comap (algebraMap A B)
82     rw [← Ideal.map_le_iff_le_comap]
83     intro b hb
84     change p b = 0
85     rw [← hp']
86     change g (transportedGlobalMap mA mB J e b) = 0
87     rw [← completedTransport_globalMap, show globalMap mA mB J b = 0 from
88       globalMap_kills mA mB J hb, map_zero, map_zero]
89   · intro hJ
90     obtain ⟨g, ⟨hg, hgp⟩, hgu⟩ :=
91       (exists_unique_factor_iff_restriction mA mB J h p hp).mpr hJ
92     refine ⟨g.comp (completedTransport mA mB J e).symm.toRingHom, ⟨?_, ?_⟩, ?_⟩
93     · exact hg.comp (completedTransport_symm_continuous mA mB J e)
94     · ext b
95       change g ((completedTransport mA mB J e).symm (transportedGlobalMap mA mB J e b)) = p b
96       rw [← completedTransport_globalMap, RingEquiv.symm_apply_apply]
97       exact DFunLike.congr_fun hgp b
98     · intro g' hg'
99       have heq : g'.comp (completedTransport mA mB J e).toRingHom = g := by
100         apply hgu
101         refine ⟨hg'.1.comp (completedTransport_continuous mA mB J e), ?_⟩
102         ext b
103         change g' (completedTransport mA mB J e (globalMap mA mB J b)) = p b
104         rw [completedTransport_globalMap]
105         exact DFunLike.congr_fun hg'.2 b
106       ext x
107       obtain ⟨y, rfl⟩ := (completedTransport mA mB J e).surjective x
108       change g' (completedTransport mA mB J e y) = g ((completedTransport mA mB J e).symm
109         (completedTransport mA mB J e y))
110       rw [RingEquiv.symm_apply_apply]
111       exact DFunLike.congr_fun heq y
112 
113 end PaperXII.CompletedBaseChange

Back to source controls