AdicModel.lean

1 import PaperXII.CompletionQuotient
2 import Mathlib.RingTheory.AdicCompletion.Topology
3 
4 /-! Actual uniform completion of a ring equipped with one ideal-adic topology. -/
5 noncomputable section
6 open Filter Topology UniformSpace
7 open scoped Uniformity
8 set_option autoImplicit false
9 namespace PaperXII.AdicModel
10 
11 /-- A type synonym isolating the specified ideal-adic topology. -/
12 def Carrier (R : Type*) [CommRing R] (_I : Ideal R) := R
13 
14 instance carrierCommRing (R : Type*) [CommRing R] (I : Ideal R) : CommRing (Carrier R I) :=
15   inferInstanceAs (CommRing R)
16 
17 /-- Forget the type synonym, without asserting continuity into an arbitrary topology. -/
18 def rawEquiv (R : Type*) [CommRing R] (I : Ideal R) : Carrier R I ≃+* R := RingEquiv.refl R
19 
20 instance carrierWithIdeal (R : Type*) [CommRing R] (I : Ideal R) : WithIdeal (Carrier R I) :=
21   ⟨I⟩
22 
23 theorem carrier_isAdic (R : Type*) [CommRing R] (I : Ideal R) :
24     IsAdic (WithIdeal.i : Ideal (Carrier R I)) := rfl
25 
26 instance carrier_countablyGenerated (R : Type*) [CommRing R] (I : Ideal R) :
27     Filter.IsCountablyGenerated (𝓤 (Carrier R I)) := by
28   have := (carrier_isAdic R I).hasBasis_nhds_zero.isCountablyGenerated
29   exact IsUniformAddGroup.uniformity_countably_generated
30 
31 /-- This is an actual completion, not a supplied completion-interface object. -/
32 abbrev Completed (R : Type*) [CommRing R] (I : Ideal R) := Completion (Carrier R I)
33 
34 def embed (R : Type*) [CommRing R] (I : Ideal R) : R →+* Completed R I :=
35   Completion.coeRingHom.comp (rawEquiv R I).symm.toRingHom
36 
37 @[simp] theorem embed_apply (R : Type*) [CommRing R] (I : Ideal R) (x : R) :
38     embed R I x = ((rawEquiv R I).symm x : Completed R I) := rfl
39 
40 /-- A ring map carrying the defining ideal into the target ideal is uniformly continuous. -/
41 theorem map_continuous {R S : Type*} [CommRing R] [CommRing S]
42     (I : Ideal R) (J : Ideal S) (f : R →+* S) (h : I.map f ≤ J) :
43     Continuous (((rawEquiv S J).symm.toRingHom.comp f).comp (rawEquiv R I).toRingHom) := by
44   exact (WithIdeal.uniformContinuous_of_map_le
45     (f := ((rawEquiv S J).symm.toRingHom.comp f).comp (rawEquiv R I).toRingHom) h).continuous
46 
47 /-- Uniform equivalence of the actual adic carriers under an ideal-preserving ring equivalence. -/
48 def uniformEquiv {R S : Type*} [CommRing R] [CommRing S]
49     (I : Ideal R) (J : Ideal S) (e : R ≃+* S) (h : I.map e.toRingHom = J) :
50     Carrier R I ≃ᵤ Carrier S J :=
51   WithIdeal.uniformEquiv ((rawEquiv R I).trans (e.trans (rawEquiv S J).symm)) h
52 
53 /-- Extend an ideal-preserving ring equivalence to the actual adic completions. -/
54 def completedEquiv {R S : Type*} [CommRing R] [CommRing S]
55     (I : Ideal R) (J : Ideal S) (e : R ≃+* S) (h : I.map e.toRingHom = J) :
56     Completed R I ≃+* Completed S J :=
57   Completion.mapRingEquiv ((rawEquiv R I).trans (e.trans (rawEquiv S J).symm))
58     (uniformEquiv I J e h).continuous (uniformEquiv I J e h).symm.continuous
59 
60 theorem completedEquiv_continuous {R S : Type*} [CommRing R] [CommRing S]
61     (I : Ideal R) (J : Ideal S) (e : R ≃+* S) (h : I.map e.toRingHom = J) :
62     Continuous (completedEquiv I J e h) := Completion.continuous_extension
63 
64 theorem completedEquiv_symm_continuous {R S : Type*} [CommRing R] [CommRing S]
65     (I : Ideal R) (J : Ideal S) (e : R ≃+* S) (h : I.map e.toRingHom = J) :
66     Continuous (completedEquiv I J e h).symm := Completion.continuous_extension
67 
68 @[simp] theorem completedEquiv_embed {R S : Type*} [CommRing R] [CommRing S]
69     (I : Ideal R) (J : Ideal S) (e : R ≃+* S) (h : I.map e.toRingHom = J) (x : R) :
70     completedEquiv I J e h (embed R I x) = embed S J (e x) :=
71   Completion.mapRingHom_coe (uniformEquiv I J e h).continuous ((rawEquiv R I).symm x)
72 
73 end PaperXII.AdicModel

Back to source controls