CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients
abbrev CompletedGroupAlgebraOpenIdeal
(R : Type u) [CommRing R] [TopologicalSpace R] : Type u :=
{I : Ideal R // IsOpen (I : Set R)}The open coefficient ideals used in the kernel-neighborhood topology of Ribes--Zalesskii Section \(5.3\).
theorem profiniteRing_eq_zero_of_forall_openIdeal_quotient_eq_zero
(hR : IsProfiniteRing R) {r : R}
(hr : ∀ I : CompletedGroupAlgebraOpenIdeal R, Ideal.Quotient.mk I.1 r = 0) :
r = 0In a profinite coefficient ring, the open-ideal quotients separate points. This is the coefficient part of the kernel-intersection statement in Lemma 5.3.5(a).
Show proof
by
by_contra hne
letI : T2Space R := hR.2.2.1
letI : T1Space R := inferInstance
have h0 : (0 : R) ∈ ({r}ᶜ : Set R) := by
exact fun h0r => hne h0r.symm
have hU : ({r}ᶜ : Set R) ∈ 𝓝 (0 : R) :=
isOpen_compl_singleton.mem_nhds h0
rcases profiniteRing_hasOpenIdealBasisAtZero R hR ({r}ᶜ) hU with
⟨I, hIopen, hIU⟩
have hrI : r ∈ I := by
exact Ideal.Quotient.eq_zero_iff_mem.1 (hr ⟨I, hIopen⟩)
exact (hIU hrI) rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□abbrev CompletedGroupAlgebraOpenQuotientIndex
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] : Type (max u v) :=
OrderDual (CompletedGroupAlgebraOpenIdeal R) × CompletedGroupAlgebraIndex GThe two-parameter index set for the kernel-neighborhood quotients \((R/I)[G/U]\), with open ideals in the coefficient direction and finite group quotients in the group direction.
instance instNonemptyCompletedGroupAlgebraOpenIdeal
(R : Type u) [CommRing R] [TopologicalSpace R] :
Nonempty (CompletedGroupAlgebraOpenIdeal R) :=
⟨⟨⊤, isOpen_univ⟩⟩theorem directed_completedGroupAlgebraOpenQuotientIndex
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] :
Directed (α := CompletedGroupAlgebraOpenQuotientIndex R G) (· ≤ ·) fun K => KThe family of completed-group-algebra open quotient indices is directed under refinement.
Show proof
by
intro K L
rcases directed_openNormalSubgroupInClass
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) ProCGroups.FiniteGroupClass.allFinite_formation
K.2 L.2 with
⟨W, hKW, hLW⟩
let I : CompletedGroupAlgebraOpenIdeal R :=
⟨(OrderDual.ofDual K.1).1 ⊓ (OrderDual.ofDual L.1).1, by
simpa using (OrderDual.ofDual K.1).2.inter (OrderDual.ofDual L.1).2⟩
refine ⟨(OrderDual.toDual I, W), ?_, ?_⟩
· constructor
· change (I.1 : Ideal R) ≤ (OrderDual.ofDual K.1).1
exact inf_le_left
· exact hKW
· constructor
· change (I.1 : Ideal R) ≤ (OrderDual.ofDual L.1).1
exact inf_le_right
· exact hLWProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□abbrev CompletedGroupAlgebraOpenFiniteQuotientStage
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
Type (max u v) :=
CompletedGroupAlgebraCoeffQuotientStage R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2The stage \((R/I)[G/U]\) attached to an open-ideal/finite-group quotient index.
def groupAlgebraOpenFiniteQuotientMap
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
MonoidAlgebra R G →+* CompletedGroupAlgebraOpenFiniteQuotientStage R G K :=
groupAlgebraFiniteQuotientMap R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2The quotient map \(R[G] \to (R/I)[G/U]\) for an open-ideal/finite-group quotient index.
def groupAlgebraOpenFiniteQuotientKernel
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
Ideal (MonoidAlgebra R G) :=
groupAlgebraFiniteQuotientKernel R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2
@[simp]The kernel neighborhood attached to an open-ideal/finite-group quotient index.
theorem mem_groupAlgebraOpenFiniteQuotientKernel_iff
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : MonoidAlgebra R G) :
x ∈ groupAlgebraOpenFiniteQuotientKernel R G K ↔
groupAlgebraOpenFiniteQuotientMap R G K x = 0Membership in the named kernel is equivalent to vanishing under its defining quotient or augmentation map.
Show proof
Iff.rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. For augmentation claims, the finite-stage augmentation sends every group-like basis element to \(1\) and a singleton coefficient to that coefficient, so the augmentation ideal is exactly the kernel described by the equation \(\varepsilon(x)=0\). Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. For the all-finite and \(C\)-indexed comparisons, both composites have the same finite-stage coordinates; hence inverse-limit extensionality proves the ring, algebra, or topological equivalence. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. For the augmentation part, each finite group-algebra augmentation sends a group-like basis element to \(1\) and a singleton coefficient to that coefficient. Therefore membership in the augmentation ideal is rewritten as a vanishing condition under \(\varepsilon\), and the kernel computation becomes the two inclusions between that vanishing locus and the image or subtype described in the statement.
□def completedGroupAlgebraOpenFiniteQuotientTransition
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
{K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
CompletedGroupAlgebraOpenFiniteQuotientStage R G L →+*
CompletedGroupAlgebraOpenFiniteQuotientStage R G K :=
completedGroupAlgebraFiniteQuotientTransition R G
(show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1)
hKL.2
@[simp]The transition \((R/I_L)[G/U]_L \to (R/I_K)[G/U]_K\) for \(K \leq L\).
theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp_map
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
{K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
(completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
(groupAlgebraOpenFiniteQuotientMap R G L) =
groupAlgebraOpenFiniteQuotientMap R G KThe finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
exact completedGroupAlgebraFiniteQuotientTransition_comp_finiteQuotientMap
(R := R) (G := G)
(hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
(hUV := hKL.2)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def completedGroupAlgebraOpenFiniteQuotientProjection
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
Carrier R G →+* CompletedGroupAlgebraOpenFiniteQuotientStage R G K :=
completedGroupAlgebraFiniteQuotientProjection R G
((OrderDual.ofDual K.1).1 : Ideal R) K.2
@[simp]The projection \(\widehat{R[G]} \to (R/I)[G/U]\) for an open-ideal/finite-group quotient index.
theorem completedGroupAlgebraOpenFiniteQuotientProjection_toCompletedGroupAlgebra
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
(completedGroupAlgebraOpenFiniteQuotientProjection R G K).comp
(toCompletedGroupAlgebraRingHom R G) =
groupAlgebraOpenFiniteQuotientMap R G KProjecting the canonical dense map to a finite quotient stage gives the corresponding stage map.
Show proof
by
rfl
@[simp]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp_projection
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
{K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
(completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
(completedGroupAlgebraOpenFiniteQuotientProjection R G L) =
completedGroupAlgebraOpenFiniteQuotientProjection R G KThe finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
exact completedGroupAlgebraFiniteQuotientTransition_comp_projection
(R := R) (G := G)
(hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
(hUV := hKL.2)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem groupAlgebraOpenFiniteQuotientKernel_antitone
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
{K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
groupAlgebraOpenFiniteQuotientKernel R G L ≤
groupAlgebraOpenFiniteQuotientKernel R G KThe open-finite quotient kernel is antitone with respect to quotient refinement.
Show proof
by
intro x hx
rw [mem_groupAlgebraOpenFiniteQuotientKernel_iff] at hx ⊢
have hcomp := congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraOpenFiniteQuotientTransition_comp_map (R := R) (G := G) hKL))
x
rw [RingHom.comp_apply, hx, map_zero] at hcomp
exact hcomp.symmProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def completedGroupAlgebraOpenFiniteQuotientStageTopology
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
⊥The discrete topology on each kernel-neighborhood quotient \((R/I)[G/U]\). This is the topology used in the construction of the abstract group-algebra topology.
theorem completedGroupAlgebraOpenFiniteQuotientStage_discrete
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K)Show proof
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) := by
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
exact ⟨rfl⟩Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem continuous_completedGroupAlgebraStageCoeffQuotientMap_openIdeal
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2)The coefficient quotient from the finite stage \(R[G/U]\) to the kernel-neighborhood quotient \((R/I)[G/U]\) is continuous when the target carries the discrete quotient topology.
Show proof
(completedGroupAlgebraSystem R G).topologicalSpace K.2
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
Continuous (completedGroupAlgebraStageCoeffQuotientMap R G
((OrderDual.ofDual K.1).1 : Ideal R) K.2) := by
let Iopen : CompletedGroupAlgebraOpenIdeal R := OrderDual.ofDual K.1
let Q := CompletedGroupAlgebraQuotient G K.2
letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
(completedGroupAlgebraSystem R G).topologicalSpace K.2
letI : TopologicalSpace (R ⧸ (Iopen.1 : Ideal R)) := ⊥
haveI : DiscreteTopology (R ⧸ (Iopen.1 : Ideal R)) := ⟨rfl⟩
have hmk : Continuous (Ideal.Quotient.mk (Iopen.1 : Ideal R)) :=
continuous_idealQuotient_mk_openIdeal_discrete
(R := R) (I := Iopen.1) Iopen.2
have hcont :
letI : TopologicalSpace (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) :=
finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
Continuous (completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 K.2) := by
dsimp [CompletedGroupAlgebraStage, CompletedGroupAlgebraCoeffQuotientStage, Q]
exact finiteGroupAlgebra_mapRangeRingHom_continuous
(R := R) (S := R ⧸ (Iopen.1 : Ideal R)) Q
(Ideal.Quotient.mk (Iopen.1 : Ideal R)) hmk
have hdisc :
letI : TopologicalSpace (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) :=
finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
DiscreteTopology (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) := by
dsimp [CompletedGroupAlgebraCoeffQuotientStage, Q]
exact finiteGroupAlgebraTopology_discrete_of_discrete_coeff
(S := R ⧸ (Iopen.1 : Ideal R)) Q
let tfin : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
let tdisc : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
have ht : tfin = tdisc := by
dsimp [tfin, tdisc, completedGroupAlgebraOpenFiniteQuotientStageTopology]
exact hdisc.eq_bot
change @Continuous (CompletedGroupAlgebraStage R G K.2)
(CompletedGroupAlgebraOpenFiniteQuotientStage R G K)
((completedGroupAlgebraSystem R G).topologicalSpace K.2) tdisc
(completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 K.2)
rw [← ht]
exact hcontProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem continuous_completedGroupAlgebraOpenFiniteQuotientProjection
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K)The projection \(\widehat{R[G]} \to (R/I)[G/U]\) to any two-parameter finite quotient is continuous.
Show proof
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
Continuous (completedGroupAlgebraOpenFiniteQuotientProjection R G K) := by
letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
(completedGroupAlgebraSystem R G).topologicalSpace K.2
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
exact (continuous_completedGroupAlgebraStageCoeffQuotientMap_openIdeal
(R := R) (G := G) K).comp ((completedGroupAlgebraSystem R G).continuous_projection K.2)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def groupAlgebraOpenFiniteQuotientProductMap
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] :
MonoidAlgebra R G →
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
CompletedGroupAlgebraOpenFiniteQuotientStage R G K :=
fun x K => groupAlgebraOpenFiniteQuotientMap R G K xThe product of all open-finite quotient maps \(R[G] \to (R/I)[G/U]\).
def groupAlgebraOpenFiniteQuotientKernelTopology
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] :
TopologicalSpace (MonoidAlgebra R G) :=
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
TopologicalSpace.induced (groupAlgebraOpenFiniteQuotientProductMap R G) inferInstanceThe kernel-neighborhood topology on \(R[G]\), induced by all maps \(R[G] \to (R/I)[G/U]\) with \(I\) open and \(U\) open normal with finite quotient.
theorem continuous_groupAlgebraOpenFiniteQuotientProductMap_kernelTopology
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G] :
letI : TopologicalSpace (MonoidAlgebra R G)The product of the finite quotient maps is continuous for the kernel-neighborhood topology.
Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
Continuous (groupAlgebraOpenFiniteQuotientProductMap R G) := by
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
exact continuous_induced_domProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem continuous_groupAlgebraOpenFiniteQuotientMap_kernelTopology
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
letI : TopologicalSpace (MonoidAlgebra R G)The finite quotient map \(R[G]\to (R/I)[G/U]\) is continuous for the kernel-neighborhood topology.
Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
Continuous (groupAlgebraOpenFiniteQuotientMap R G K) := by
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
change Continuous fun x : MonoidAlgebra R G =>
groupAlgebraOpenFiniteQuotientProductMap R G x K
exact (continuous_apply K).comp
(continuous_groupAlgebraOpenFiniteQuotientProductMap_kernelTopology R G)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem groupAlgebraOpenFiniteQuotientKernel_isOpen_kernelTopology
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
letI : TopologicalSpace (MonoidAlgebra R G)Each open-finite quotient kernel is open in the kernel topology.
Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
IsOpen (groupAlgebraOpenFiniteQuotientKernel R G K : Set (MonoidAlgebra R G)) := by
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
haveI : DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
change IsOpen ((groupAlgebraOpenFiniteQuotientMap R G K) ⁻¹'
({0} : Set (CompletedGroupAlgebraOpenFiniteQuotientStage R G K)))
exact (isOpen_discrete ({0} : Set (CompletedGroupAlgebraOpenFiniteQuotientStage R G K))).preimage
(continuous_groupAlgebraOpenFiniteQuotientMap_kernelTopology R G K)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem groupAlgebraOpenFiniteQuotientKernel_mem_nhds_zero_kernelTopology
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
letI : TopologicalSpace (MonoidAlgebra R G)Show proof
groupAlgebraOpenFiniteQuotientKernelTopology R G
(groupAlgebraOpenFiniteQuotientKernel R G K : Set (MonoidAlgebra R G)) ∈
𝓝 (0 : MonoidAlgebra R G) := by
letI : TopologicalSpace (MonoidAlgebra R G) :=
groupAlgebraOpenFiniteQuotientKernelTopology R G
apply IsOpen.mem_nhds
(groupAlgebraOpenFiniteQuotientKernel_isOpen_kernelTopology R G K)
change (0 : MonoidAlgebra R G) ∈ groupAlgebraOpenFiniteQuotientKernel R G K
rw [mem_groupAlgebraOpenFiniteQuotientKernel_iff]
exact map_zero (groupAlgebraOpenFiniteQuotientMap R G K)
@[simp]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraOpenFiniteQuotientTransition_single
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
{K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L)
(q : CompletedGroupAlgebraQuotient G L.2)
(r : R ⧸ ((OrderDual.ofDual L.1).1 : Ideal R)) :
completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(MonoidAlgebra.single q r) =
MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual K.2) (V := OrderDual.ofDual L.2) hKL.2) q)
(Ideal.Quotient.factor
(show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1) r)The finite-stage transition sends a singleton basis function to the singleton supported at its image in the coarser quotient.
Show proof
by
exact completedGroupAlgebraFiniteQuotientTransition_single (R := R) (G := G)
(hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
(hUV := hKL.2) q r
@[simp]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraOpenFiniteQuotientTransition_id
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
completedGroupAlgebraOpenFiniteQuotientTransition R G (le_rfl : K ≤ K) =
RingHom.id (CompletedGroupAlgebraOpenFiniteQuotientStage R G K)The finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
apply MonoidAlgebra.ringHom_ext
· intro r
rw [completedGroupAlgebraOpenFiniteQuotientTransition_single]
simp only [map_one, Ideal.Quotient.factor_eq, RingHom.id_apply]
· intro q
rw [completedGroupAlgebraOpenFiniteQuotientTransition_single]
change MonoidAlgebra.single
((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual K.2) (V := OrderDual.ofDual K.2)
(le_rfl : K.2 ≤ K.2)) q) 1 =
MonoidAlgebra.single q 1
rw [OpenNormalSubgroupInClass.map_id]
simp only [MonoidHom.id_apply]
@[simp 900]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
{K L M : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) (hLM : L ≤ M) :
(completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
(completedGroupAlgebraOpenFiniteQuotientTransition R G hLM) =
completedGroupAlgebraOpenFiniteQuotientTransition R G (hKL.trans hLM)The finite-stage transition maps compose compatibly along chains of quotient refinements.
Show proof
by
apply MonoidAlgebra.ringHom_ext
· intro r
rw [RingHom.comp_apply, completedGroupAlgebraOpenFiniteQuotientTransition_single,
completedGroupAlgebraOpenFiniteQuotientTransition_single,
completedGroupAlgebraOpenFiniteQuotientTransition_single]
simp only [map_one, Ideal.Quotient.factor_comp_apply]
· intro q
rw [RingHom.comp_apply, completedGroupAlgebraOpenFiniteQuotientTransition_single,
completedGroupAlgebraOpenFiniteQuotientTransition_single,
completedGroupAlgebraOpenFiniteQuotientTransition_single]
have hmap := congrFun
(congrArg DFunLike.coe
(OpenNormalSubgroupInClass.map_comp
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual K.2) (V := OrderDual.ofDual L.2) (W := OrderDual.ofDual M.2)
hKL.2 hLM.2))
q
exact congrArg
(fun t => MonoidAlgebra.single t
(1 : R ⧸ ((OrderDual.ofDual K.1).1 : Ideal R)))
hmapProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem completedGroupAlgebraOpenFiniteQuotientTransition_surjective
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
[TopologicalSpace G] [IsTopologicalGroup G]
{K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
Function.Surjective (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)The finite-stage transition map is surjective, with preimages obtained by lifting quotient representatives.
Show proof
completedGroupAlgebraFiniteQuotientTransition_surjective
(R := R) (G := G)
(hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
(hUV := hKL.2)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Surjectivity is obtained by lifting a representative through the underlying surjective quotient or group homomorphism and then checking the defining finite-stage formula. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□