Yamaguchi Lean 4 Library
CompletedGroupAlgebra/Basic/InClass/System.lean
CompletedGroupAlgebra/Basic/InClass/System/Source

CompletedGroupAlgebra/Basic/InClass/System.lean

1import CompletedGroupAlgebra.Basic.InClass.Stage
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/InClass/System.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Class-Indexed Completed Group Algebras
14Finite-class-indexed inverse systems and inverse limits for completed group algebras.
15-/
17open scoped Topology
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
27universe u v w
29variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
33/-- The `C`-indexed inverse system `U ↦ R[G/U]`. The hypothesis says that `C` really is a
34finite quotient class, so every stage carries the finite-product topology. -/
35def completedGroupAlgebraSystemInClass
36 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
37 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
38 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
39 ProCGroups.InverseSystems.InverseSystem (I := CompletedGroupAlgebraIndexInClass G C) where
40 X := CompletedGroupAlgebraStageInClass C R G
41 topologicalSpace := fun U => by
42 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
44 exact finiteGroupAlgebraTopology R (CompletedGroupAlgebraQuotientInClass G C U)
45 map := fun {U V} hUV => completedGroupAlgebraTransitionInClass C R G hUV
46 continuous_map := by
47 intro U V hUV
48 letI : Finite (CompletedGroupAlgebraQuotientInClass G C V) :=
50 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
53 (CompletedGroupAlgebraQuotientInClass G C V) (CompletedGroupAlgebraQuotientInClass G C U)
54 (OpenNormalSubgroupInClass.map
55 (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
56 map_id := by
57 intro U
58 funext x
59 exact congrFun
60 (congrArg DFunLike.coe
61 (completedGroupAlgebraTransitionInClass_id (R := R) (G := G) C U)) x
62 map_comp := by
63 intro U V W hUV hVW
64 funext x
65 exact congrFun
66 (congrArg DFunLike.coe
67 (completedGroupAlgebraTransitionInClass_comp (R := R) (G := G) C hUV hVW)) x
70 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
71 (U : CompletedGroupAlgebraIndexInClass G C) :
72 Ring ((completedGroupAlgebraSystemInClass C hC R G).X U) := by
73 dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass,
74 CompletedGroupAlgebraQuotientInClass]
75 infer_instance
78 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
79 IsRingSystem (completedGroupAlgebraSystemInClass C hC R G) where
80 map_zero := by
81 intro U V hUV
82 exact map_zero (completedGroupAlgebraTransitionInClass C R G hUV)
83 map_one := by
84 intro U V hUV
85 exact map_one (completedGroupAlgebraTransitionInClass C R G hUV)
86 map_add := by
87 intro U V hUV x y
88 exact map_add (completedGroupAlgebraTransitionInClass C R G hUV) x y
89 map_mul := by
90 intro U V hUV x y
91 exact map_mul (completedGroupAlgebraTransitionInClass C R G hUV) x y
94end