FoxDifferential/Completed/DifferentialModule/Map/Limit.lean
1import FoxDifferential.Completed.DifferentialModule.Map.Stage
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/DifferentialModule/Map/Limit.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed differential modules
14The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups
21open ProCGroups.ProC
23universe u v
25variable (ℓ : ℕ)
26variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
29/-- Definition of primePowerCompletedGroupAlgebraMap. -/
31 (ψ : ContinuousMonoidHom G H) :
32 PrimePowerCompletedGroupAlgebra ℓ G →+* PrimePowerCompletedGroupAlgebra ℓ H where
33 toFun x := ⟨fun i =>
34 primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
35 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
36 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x), by
37 intro i j hij
38 let hsource :
39 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) ≤
40 (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) :=
41 ⟨hij.1, completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2⟩
42 have hx := x.2
43 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
44 (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2)
45 hsource
46 change
47 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hsource
48 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
49 (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) x) =
50 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
51 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x at hx
52 have hcompat := congrFun
53 (congrArg DFunLike.coe
55 (ℓ := ℓ) (G := G) (H := H) ψ hij))
56 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
57 (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) x)
58 rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
59 rw [hx] at hcompat
60 simpa [primePowerCompletedGroupAlgebraSystem] using hcompat⟩
61 map_one' := by
62 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
63 intro i
64 simp only [primePowerCompletedGroupAlgebraMapStage, InverseSystems.InverseSystem.projection_apply,
65 coe_one_primePowerCompletedGroupAlgebra, Pi.one_apply, MonoidAlgebra.mapDomainRingHom_apply,
66 MonoidAlgebra.mapDomain_one]
67 map_mul' := by
68 intro x y
69 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
70 intro i
71 simp only [InverseSystems.InverseSystem.projection_apply, coe_mul_primePowerCompletedGroupAlgebra,
73 map_zero' := by
74 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
75 intro i
76 simp only [primePowerCompletedGroupAlgebraMapStage, InverseSystems.InverseSystem.projection_apply,
77 coe_zero_primePowerCompletedGroupAlgebra, Pi.zero_apply, MonoidAlgebra.mapDomainRingHom_apply,
78 Finsupp.mapDomain_zero]
79 map_add' := by
80 intro x y
81 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
82 intro i
83 simp only [InverseSystems.InverseSystem.projection_apply, coe_add_primePowerCompletedGroupAlgebra,
86/-- 素冪係数で定めた 有限段階射影が関手的写像が有限段階射影と両立することを述べる。 -/
87@[simp]
89 (ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
90 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
91 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
92 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x) =
93 primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
94 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
95 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x) := rfl
98/-- The completed group-algebra map induced by a continuous homomorphism is continuous for the
99inverse-limit topologies. -/
101 (ψ : ContinuousMonoidHom G H) :
102 Continuous (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ) := by
103 let S := primePowerCompletedGroupAlgebraSystem ℓ H
104 let T := primePowerCompletedGroupAlgebraSystem ℓ G
105 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, TopologicalSpace (S.X i) :=
106 fun i => S.topologicalSpace i
107 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, TopologicalSpace (T.X i) :=
108 fun i => T.topologicalSpace i
109 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun x =>
110 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x).2)
111 let sourceIndex : PrimePowerCompletedGroupAlgebraIndex G :=
112 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
113 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G sourceIndex) :=
114 T.topologicalSpace sourceIndex
115 letI : DiscreteTopology (PrimePowerCompletedGroupAlgebraStage ℓ G sourceIndex) := ⟨rfl⟩
116 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ H i) :=
117 S.topologicalSpace i
118 have hstage :
119 Continuous
120 (primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i) :=
121 continuous_of_discreteTopology
122 change Continuous (fun x : PrimePowerCompletedGroupAlgebra ℓ G =>
123 primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
124 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) sourceIndex x))
125 exact hstage.comp (T.continuous_projection sourceIndex)
127end
129end FoxDifferential