AdicQuotientTopology.lean

1 import PaperXII.AdicModel
2 
3 /-! The quotient topology of an adic ring is the mapped-ideal adic topology. -/
4 noncomputable section
5 open Filter Topology UniformSpace
6 open scoped Uniformity
7 set_option autoImplicit false
8 namespace PaperXII.AdicModel
9 
10 /-- Continuity from control of the actual defining ideals. -/
11 theorem continuous_of_map_le {R S : Type*} [CommRing R] [CommRing S]
12     [TopologicalSpace R] [TopologicalSpace S] [IsTopologicalRing R] [IsTopologicalRing S]
13     {I : Ideal R} {J : Ideal S} (hR : IsAdic I) (hS : IsAdic J)
14     (f : R →+* S) (h : I.map f ≤ J) : Continuous f := by
15   apply continuous_of_continuousAt_zero f
16   rw [ContinuousAt, map_zero, hR.hasBasis_nhds_zero.tendsto_iff hS.hasBasis_nhds_zero]
17   refine fun n _ ↦ ⟨n, trivial, ?_⟩
18   exact Ideal.map_le_iff_le_comap.mp (by simpa [Ideal.map_pow] using Ideal.pow_right_mono h n)
19 
20 /-- Actual quotient neighborhoods have the expected adic basis. -/
21 theorem quotient_isAdic {R : Type*} [CommRing R] [TopologicalSpace R]
22     [IsTopologicalRing R] {I : Ideal R} (hR : IsAdic I) (J : Ideal R) :
23     IsAdic (I.map (Ideal.Quotient.mk J)) := by
24   rw [isAdic_iff]
25   constructor
26   · intro n
27     rw [← Ideal.map_pow, Ideal.map_eq_image_of_surjective _ Ideal.Quotient.mk_surjective]
28     exact (QuotientRing.isOpenMap_coe J) _ ((isAdic_iff.mp hR).1 n)
29   · intro V hV
30     have hb := hR.hasBasis_nhds_zero.map (Ideal.Quotient.mk J)
31     rw [(QuotientRing.isOpenQuotientMap_mk J).map_nhds_eq, map_zero] at hb
32     obtain ⟨n, _, hn⟩ := hb.mem_iff.mp hV
33     refine ⟨n, ?_⟩
34     rw [← Ideal.map_pow, Ideal.map_eq_image_of_surjective _ Ideal.Quotient.mk_surjective]
35     exact hn
36 
37 /-- Retag an ideal on the carrier without changing its elements. -/
38 def carrierIdeal {R : Type*} [CommRing R] (I J : Ideal R) : Ideal (Carrier R I) :=
39   J.map (rawEquiv R I).symm.toRingHom
40 
41 @[simp] theorem carrierIdeal_mem {R : Type*} [CommRing R] (I J : Ideal R) (x : Carrier R I) :
42     x ∈ carrierIdeal I J ↔ rawEquiv R I x ∈ J := by
43   change x ∈ J.map (RingHom.id R) ↔ x ∈ J
44   simp
45 
46 /-- The ring quotient of the actual adic carrier and the adic quotient carrier agree. -/
47 def quotientCarrierEquiv {R : Type*} [CommRing R] (I J : Ideal R) :
48     (Carrier R I ⧸ carrierIdeal I J) ≃+* Carrier (R ⧸ J) (I.map (Ideal.Quotient.mk J)) :=
49   (Ideal.quotientEquiv _ _ (rawEquiv R I) (by simp [carrierIdeal, Ideal.map_map])).trans
50     (rawEquiv (R ⧸ J) (I.map (Ideal.Quotient.mk J))).symm
51 
52 /-- The quotient carrier equivalence preserves the ideal controlling its topology. -/
53 theorem quotientCarrierEquiv_map {R : Type*} [CommRing R] (I J : Ideal R) :
54     ((WithIdeal.i : Ideal (Carrier R I)).map (Ideal.Quotient.mk (carrierIdeal I J))).map
55       (quotientCarrierEquiv I J).toRingHom =
56       (WithIdeal.i : Ideal (Carrier (R ⧸ J) (I.map (Ideal.Quotient.mk J)))) := by
57   rw [Ideal.map_map]
58   rfl
59 
60 theorem quotientCarrierEquiv_continuous {R : Type*} [CommRing R] (I J : Ideal R) :
61     Continuous (quotientCarrierEquiv I J) :=
62   continuous_of_map_le (quotient_isAdic (carrier_isAdic R I) _)
63     (carrier_isAdic _ _) (quotientCarrierEquiv I J).toRingHom
64     (quotientCarrierEquiv_map I J).le
65 
66 theorem quotientCarrierEquiv_symm_continuous {R : Type*} [CommRing R] (I J : Ideal R) :
67     Continuous (quotientCarrierEquiv I J).symm := by
68   apply continuous_of_map_le (carrier_isAdic _ _)
69     (quotient_isAdic (carrier_isAdic R I) _) (quotientCarrierEquiv I J).symm.toRingHom
70   rw [← quotientCarrierEquiv_map I J, Ideal.map_map]
71   simp
72 
73 @[simp] theorem quotientCarrierEquiv_mk {R : Type*} [CommRing R] (I J : Ideal R) (x : R) :
74     quotientCarrierEquiv I J (Ideal.Quotient.mk _ ((rawEquiv R I).symm x)) =
75       (rawEquiv (R ⧸ J) (I.map (Ideal.Quotient.mk J))).symm (Ideal.Quotient.mk J x) := rfl
76 
77 attribute [local instance] CompletionQuotient.quotientUniformSpace
78 
79 /-- Quotienting commutes with actual adic completion, including both topologies. -/
80 def quotientCompletionEquiv {R : Type*} [CommRing R] (I J : Ideal R) :
81     (Completed R I ⧸ CompletionQuotient.closedExtension (carrierIdeal I J)) ≃+*
82       Completed (R ⧸ J) (I.map (Ideal.Quotient.mk J)) :=
83   (CompletionQuotient.equiv (carrierIdeal I J)).trans
84     (Completion.mapRingEquiv (quotientCarrierEquiv I J)
85       (quotientCarrierEquiv_continuous I J) (quotientCarrierEquiv_symm_continuous I J))
86 
87 theorem quotientCompletionEquiv_continuous {R : Type*} [CommRing R] (I J : Ideal R) :
88     Continuous (quotientCompletionEquiv I J) :=
89   Completion.continuous_extension.comp (CompletionQuotient.equiv_continuous _)
90 
91 theorem quotientCompletionEquiv_symm_continuous {R : Type*} [CommRing R] (I J : Ideal R) :
92     Continuous (quotientCompletionEquiv I J).symm :=
93   (CompletionQuotient.equiv_symm_continuous _).comp Completion.continuous_extension
94 
95 @[simp] theorem quotientCompletionEquiv_mk_embed {R : Type*} [CommRing R]
96     (I J : Ideal R) (x : R) :
97     quotientCompletionEquiv I J (Ideal.Quotient.mk _ (embed R I x)) =
98       embed (R ⧸ J) (I.map (Ideal.Quotient.mk J)) (Ideal.Quotient.mk J x) := by
99   change Completion.mapRingEquiv (quotientCarrierEquiv I J)
100     (quotientCarrierEquiv_continuous I J) (quotientCarrierEquiv_symm_continuous I J)
101     (CompletionQuotient.equiv _ (Ideal.Quotient.mk _ ((rawEquiv R I).symm x : Completed R I))) = _
102   rw [CompletionQuotient.equiv_mk_coe]
103   exact Completion.mapRingHom_coe (quotientCarrierEquiv_continuous I J) _
104 
105 end PaperXII.AdicModel

Back to source controls