CompletedGroupAlgebra.UniversalProperty.FiniteQuotient
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
def completedGroupAlgebraLiftOfFiniteQuotient
(U : CompletedGroupAlgebraIndex G) (N : Type (max u v))
[AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N]
[ContinuousSMul R N] (f : CompletedGroupAlgebraQuotient G U → N) :
Carrier R G →L[R] N := by
letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
(completedGroupAlgebraSystem R G).topologicalSpace U
exact (finiteGroupAlgebraLift R (CompletedGroupAlgebraQuotient G U) N f).comp
(completedGroupAlgebraProjectionContinuousLinearMap R G U)theorem completedGroupAlgebraLiftOfFiniteQuotient_apply_of
(U : CompletedGroupAlgebraIndex G) (N : Type (max u v))
[AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N]
[ContinuousSMul R N] (f : CompletedGroupAlgebraQuotient G U → N) (g : G) :
completedGroupAlgebraLiftOfFiniteQuotient (R := R) (G := G) U N f
(completedGroupAlgebraOf R G g) =
f (openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)The finite-quotient lift has the prescribed value on completed group-like elements.
Show proof
by
letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
(completedGroupAlgebraSystem R G).topologicalSpace U
change finiteGroupAlgebraLift R (CompletedGroupAlgebraQuotient G U) N f
(completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g)) =
f (openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)
rw [completedGroupAlgebraProjection_of]
exact finiteGroupAlgebraLift_apply_of R (CompletedGroupAlgebraQuotient G U) N f
(openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U 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. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. 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 quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem completedGroupAlgebra_existsUnique_lift_of_factors
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
[ContinuousAdd N] [ContinuousSMul R N] [T2Space N]
(U : CompletedGroupAlgebraIndex G) (f : G → N)
(fbar : CompletedGroupAlgebraQuotient G U → N)
(hfac : ∀ g : G,
fbar (openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = f g) :
∃! F : Carrier R G →L[R] N,
∀ g : G, F (completedGroupAlgebraOf R G g) = f gShow proof
by
let F := completedGroupAlgebraLiftOfFiniteQuotient (R := R) (G := G) U N fbar
refine ⟨F, ?_, ?_⟩
· intro g
rw [completedGroupAlgebraLiftOfFiniteQuotient_apply_of, hfac]
· intro K hK
apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G) hG
intro g
rw [completedGroupAlgebraLiftOfFiniteQuotient_apply_of, hfac, hK]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. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. 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 exists_completedGroupAlgebraIndex_factor_continuous_discrete
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [TopologicalSpace N] [DiscreteTopology N]
(f : G → N) (hf : Continuous f) :
∃ U : CompletedGroupAlgebraIndex G, ∃ fbar : CompletedGroupAlgebraQuotient G U → N,
∀ g : G,
fbar (openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = f gA continuous map from a profinite group to a discrete space is unchanged on the cosets of some finite open normal quotient. This is the topological factorization input in the book proof of Lemma 5.3.5(d).
Show proof
by
letI : CompactSpace G := ProCGroups.IsProfiniteGroup.compactSpace hG
let T : Set (G × G) := {p | f p.1 = f p.2}
have hTopen : IsOpen T := by
have hpair : Continuous fun p : G × G => (f p.1, f p.2) :=
(hf.comp continuous_fst).prodMk (hf.comp continuous_snd)
change IsOpen ((fun p : G × G => (f p.1, f p.2)) ⁻¹'
{q : N × N | q.1 = q.2})
exact hpair.isOpen_preimage _ (isOpen_discrete _)
let A : Set (G × G) := {p | f p.1 = f (p.1 * p.2)}
have hAopen : IsOpen A := by
have hmul : Continuous fun p : G × G => (p.1, p.1 * p.2) :=
continuous_fst.prodMk (continuous_fst.mul continuous_snd)
change IsOpen ((fun p : G × G => (p.1, p.1 * p.2)) ⁻¹' T)
exact hTopen.preimage hmul
have hcontains : (Set.univ : Set G) ×ˢ ({1} : Set G) ⊆ A := by
rintro ⟨g, u⟩ ⟨_hg, hu⟩
change u = 1 at hu
change f g = f (g * u)
rw [hu, mul_one]
rcases generalized_tube_lemma (s := (Set.univ : Set G)) isCompact_univ
(t := ({1} : Set G)) isCompact_singleton hAopen hcontains with
⟨W, V, _hWopen, hVopen, hWuniv, h1V, hWV⟩
have hVone : (1 : G) ∈ V := h1V (by simp only [Set.mem_singleton_iff])
have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
(isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
rcases hProC.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hVopen hVone with
⟨U0, hU0V⟩
let U : CompletedGroupAlgebraIndex G := OrderDual.toDual U0
let fbar : CompletedGroupAlgebraQuotient G U → N := Quotient.lift f (by
intro a b hab
have habU : a⁻¹ * b ∈ (U0.1 : Subgroup G) :=
(QuotientGroup.leftRel_apply).1 hab
have habV : a⁻¹ * b ∈ V := hU0V habU
have hA : (a, a⁻¹ * b) ∈ A :=
hWV ⟨hWuniv (Set.mem_univ a), habV⟩
simpa [A, mul_assoc] using hA)
refine ⟨U, fbar, ?_⟩
intro g
rflProof. Use compactness of the profinite group and discreteness of the target. Continuity makes the map locally constant; a finite clopen cover of the compact source gives a finite partition on which the map is constant. Refining by the open-normal neighborhood basis at the identity gives an open normal subgroup whose cosets lie inside those constant pieces, so the map factors through the finite quotient by that subgroup.
□theorem completedGroupAlgebra_existsUnique_lift_to_discreteModule
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
[ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
(f : G → N) (hf : Continuous f) :
∃! F : Carrier R G →L[R] N,
∀ g : G, F (completedGroupAlgebraOf R G g) = f gDiscrete-target form of Lemma 5.3.5(d): a continuous map from the profinite group \(G\) to a discrete \(R\)-module extends uniquely to a continuous \(R\)-linear map out of \(\widehat{R[G]}\).
Show proof
by
letI : T2Space N := inferInstance
rcases exists_completedGroupAlgebraIndex_factor_continuous_discrete
(G := G) hG N f hf with
⟨U, fbar, hfac⟩
exact completedGroupAlgebra_existsUnique_lift_of_factors (R := R) (G := G) hG N
U f fbar hfacProof. 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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□def completedGroupAlgebraLiftToDiscreteModule
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
[ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
(f : G → N) (hf : Continuous f) :
Carrier R G →L[R] N :=
Classical.choose
(completedGroupAlgebra_existsUnique_lift_to_discreteModule
(R := R) (G := G) hG N f hf)The discrete-target extension used in Lemma 5.3.5(d).
theorem completedGroupAlgebraLiftToDiscreteModule_apply_of
(hG : ProCGroups.IsProfiniteGroup G)
(N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
[ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
(f : G → N) (hf : Continuous f) (g : G) :
completedGroupAlgebraLiftToDiscreteModule
(R := R) (G := G) hG N f hf
(completedGroupAlgebraOf R G g) = f gThe chosen discrete-target lift has the prescribed value on completed group-like elements.
Show proof
by
exact (Classical.choose_spec
(completedGroupAlgebra_existsUnique_lift_to_discreteModule
(R := R) (G := G) hG N f hf)).1 gProof. 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, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Coefficient-change assertions hold because each singleton coefficient is transported by the chosen ring homomorphism and the quotient support is left unchanged. 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 quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□