CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Algebra
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
instance instZeroCompletedGroupAlgebraOpenFiniteQuotientLimit :
Zero (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
zero := ⟨fun K => (0 : CompletedGroupAlgebraOpenFiniteQuotientStage R G K), by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(0 : CompletedGroupAlgebraOpenFiniteQuotientStage R G L) = 0
exact map_zero (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)⟩The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.
instance instAddCompletedGroupAlgebraOpenFiniteQuotientLimit :
Add (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
add x y := ⟨fun K =>
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) +
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K), by
intro K L hKL
calc
completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
((show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) +
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L))
=
completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) +
completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L) := by
rw [map_add]
_ = (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) +
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K) := by
exact congrArg₂ HAdd.hAdd (x.2 K L hKL) (y.2 K L hKL)⟩instance instNegCompletedGroupAlgebraOpenFiniteQuotientLimit :
Neg (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
neg x := ⟨fun K => -(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K), by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(-(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L)) =
-(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K)
rw [map_neg]
exact congrArg Neg.neg (x.2 K L hKL)⟩instance instSubCompletedGroupAlgebraOpenFiniteQuotientLimit :
Sub (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
sub x y := ⟨fun K =>
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) -
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K), by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
((show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) -
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L)) =
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) -
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K)
rw [map_sub]
exact congrArg₂ HSub.hSub (x.2 K L hKL) (y.2 K L hKL)⟩Subtraction on the completed group algebra is defined coordinatewise through the finite-stage group-algebra subtractions.
instance instSMulNatCompletedGroupAlgebraOpenFiniteQuotientLimit :
SMul ℕ (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
smul n x := ⟨fun K => n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K), by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L)) =
n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K)
rw [map_nsmul]
exact congrArg (n • ·) (x.2 K L hKL)⟩The open-finite quotient completed group algebra carries natural-number scalar multiplication coordinatewise.
instance instSMulIntCompletedGroupAlgebraOpenFiniteQuotientLimit :
SMul ℤ (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
smul n x := ⟨fun K => n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K), by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L)) =
n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K)
rw [map_zsmul]
exact congrArg (n • ·) (x.2 K L hKL)⟩The completed group algebra carries integer scalar multiplication by applying the scalar action at every finite quotient stage.
instance instAddCommGroupCompletedGroupAlgebraOpenFiniteQuotientStage
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
AddCommGroup ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
dsimp [completedGroupAlgebraOpenFiniteQuotientSystem,
CompletedGroupAlgebraOpenFiniteQuotientStage, CompletedGroupAlgebraCoeffQuotientStage]
infer_instanceinstance instAddCommGroupCompletedGroupAlgebraOpenFiniteQuotientFamily :
AddCommGroup
((K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
inferInstancetheorem coe_zero_completedGroupAlgebraOpenFiniteQuotientLimit :
((0 : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) = 0Show proof
by
funext K
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. 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. 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 coe_add_completedGroupAlgebraOpenFiniteQuotientLimit
(x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
((x + y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
x + yThe coercion of a sum in the open-finite quotient limit is computed coordinatewise.
Show proof
by
funext K
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. 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. 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 coe_neg_completedGroupAlgebraOpenFiniteQuotientLimit
(x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
((-x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
-xThe coercion of a negation in the open-finite quotient limit is computed coordinatewise.
Show proof
by
funext K
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. 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. 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 coe_sub_completedGroupAlgebraOpenFiniteQuotientLimit
(x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
((x - y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
x - yThe coercion of a subtraction in the open-finite quotient limit is computed coordinatewise.
Show proof
by
funext K
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. 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. 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 coe_nsmul_completedGroupAlgebraOpenFiniteQuotientLimit
(n : ℕ) (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
((n • x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
n • xThe coercion of a natural scalar multiple in the open-finite quotient limit is coordinatewise.
Show proof
by
funext K
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. 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. 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 coe_zsmul_completedGroupAlgebraOpenFiniteQuotientLimit
(n : ℤ) (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
((n • x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
n • xThe coercion of an integer scalar multiple in the open-finite quotient limit is coordinatewise.
Show proof
by
funext K
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. 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. 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.
□instance instAddCommGroupCompletedGroupAlgebraOpenFiniteQuotientLimit :
AddCommGroup (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
Function.Injective.addCommGroup
(fun x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G =>
(x : (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K))
Subtype.val_injective
(coe_zero_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(coe_add_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(coe_neg_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(coe_sub_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(fun x n => coe_nsmul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n x)
(fun x n => coe_zsmul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n x)instance instOneCompletedGroupAlgebraOpenFiniteQuotientLimit :
One (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
one := ⟨fun K => (1 : CompletedGroupAlgebraOpenFiniteQuotientStage R G K), by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(1 : CompletedGroupAlgebraOpenFiniteQuotientStage R G L) = 1
exact map_one (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)⟩The open-finite quotient limit has a coordinatewise multiplicative identity.
instance instMulCompletedGroupAlgebraOpenFiniteQuotientLimit :
Mul (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
mul x y := ⟨fun K =>
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) *
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K), by
intro K L hKL
calc
completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
((show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) *
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L))
=
completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) *
completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L) := by
rw [map_mul]
_ = (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) *
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K) := by
exact congrArg₂ HMul.hMul (x.2 K L hKL) (y.2 K L hKL)⟩Multiplication on the completed group algebra is defined coordinatewise through the finite-stage group-algebra products.
instance instNatCastCompletedGroupAlgebraOpenFiniteQuotientLimit :
NatCast (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
natCast n := ⟨fun K => (n : CompletedGroupAlgebraOpenFiniteQuotientStage R G K), by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(n : CompletedGroupAlgebraOpenFiniteQuotientStage R G L) = n
exact map_natCast (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) n⟩Natural number casts in the open-finite quotient limit are computed coordinatewise.
instance instIntCastCompletedGroupAlgebraOpenFiniteQuotientLimit :
IntCast (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
intCast n := ⟨fun K => (n : CompletedGroupAlgebraOpenFiniteQuotientStage R G K), by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
(n : CompletedGroupAlgebraOpenFiniteQuotientStage R G L) = n
exact map_intCast (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) n⟩Integer casts in the open-finite quotient limit are computed coordinatewise.
instance instRingCompletedGroupAlgebraOpenFiniteQuotientStage
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
dsimp [completedGroupAlgebraOpenFiniteQuotientSystem,
CompletedGroupAlgebraOpenFiniteQuotientStage, CompletedGroupAlgebraCoeffQuotientStage]
infer_instanceThe completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
instance instRingCompletedGroupAlgebraOpenFiniteQuotientFamily :
Ring ((K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
inferInstanceThe completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
instance instPowCompletedGroupAlgebraOpenFiniteQuotientLimit :
Pow (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) ℕ where
pow x n := ⟨fun K => (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) ^ n, by
intro K L hKL
change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
((show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) ^ n) =
(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) ^ n
rw [map_pow]
exact congrArg (fun t => t ^ n) (x.2 K L hKL)⟩Powers in the open-finite quotient limit are computed coordinatewise.
theorem coe_one_completedGroupAlgebraOpenFiniteQuotientLimit :
((1 : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) = 1Show proof
by
funext K
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. 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. 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 coe_mul_completedGroupAlgebraOpenFiniteQuotientLimit
(x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
((x * y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
x * yThe coercion of a product in the open-finite quotient limit is computed coordinatewise.
Show proof
by
funext K
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. 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. 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 coe_natCast_completedGroupAlgebraOpenFiniteQuotientLimit (n : ℕ) :
((n : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
nNatural number casts into the open-finite quotient limit are computed coordinatewise.
Show proof
by
funext K
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. 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. 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 coe_intCast_completedGroupAlgebraOpenFiniteQuotientLimit (n : ℤ) :
((n : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
nInteger casts into the open-finite quotient limit are computed coordinatewise.
Show proof
by
funext K
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. 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. 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 coe_pow_completedGroupAlgebraOpenFiniteQuotientLimit
(x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) (n : ℕ) :
((x ^ n : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
(K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
x ^ nPowers in the open-finite quotient limit are computed coordinatewise.
Show proof
by
funext K
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. 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. 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.
□instance instRingCompletedGroupAlgebraOpenFiniteQuotientLimit :
Ring (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
Function.Injective.ring
(fun x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G =>
(x : (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
(completedGroupAlgebraOpenFiniteQuotientSystem R G).X K))
Subtype.val_injective
(coe_zero_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(coe_one_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(coe_add_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(coe_mul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(coe_neg_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(coe_sub_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
(fun n x => coe_nsmul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n x)
(fun n x => coe_zsmul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n x)
(fun x n => coe_pow_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) x n)
(by intro n; exact coe_natCast_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n)
(by intro n; exact coe_intCast_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n)The completed group algebra is a ring because all ring operations and ring axioms are inherited coordinatewise from the finite-stage group algebras.
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_zero
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
(0 : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) = 0The projection from the open-finite quotient limit sends \(0\) to \(0\).
Show proof
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. 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. 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 completedGroupAlgebraOpenFiniteQuotientLimitProjection_add
(K : CompletedGroupAlgebraOpenQuotientIndex R G)
(x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K (x + y) =
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x +
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K yThe projection from the open-finite quotient limit preserves addition.
Show proof
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. 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. 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 completedGroupAlgebraOpenFiniteQuotientLimitProjection_neg
(K : CompletedGroupAlgebraOpenQuotientIndex R G)
(x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K (-x) =
-completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K xThe projection from the open-finite quotient limit preserves negation.
Show proof
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. 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. 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 completedGroupAlgebraOpenFiniteQuotientLimitProjection_sub
(K : CompletedGroupAlgebraOpenQuotientIndex R G)
(x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K (x - y) =
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x -
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K yThe projection from the open-finite quotient limit preserves subtraction.
Show proof
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. 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. 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 completedGroupAlgebraOpenFiniteQuotientLimitProjection_one
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
(1 : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) = 1The projection from the open-finite quotient limit sends \(1\) to \(1\).
Show proof
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. 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. 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 completedGroupAlgebraOpenFiniteQuotientLimitProjection_mul
(K : CompletedGroupAlgebraOpenQuotientIndex R G)
(x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K (x * y) =
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x *
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K yThe projection from the open-finite quotient limit preserves multiplication.
Show proof
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. 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. 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 completedGroupAlgebraOpenFiniteQuotientLimitProjectionRingHom
(R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(K : CompletedGroupAlgebraOpenQuotientIndex R G) :
CompletedGroupAlgebraOpenFiniteQuotientLimit R G →+*
CompletedGroupAlgebraOpenFiniteQuotientStage R G K where
toFun := completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
map_zero' := completedGroupAlgebraOpenFiniteQuotientLimitProjection_zero (R := R) (G := G) K
map_one' := completedGroupAlgebraOpenFiniteQuotientLimitProjection_one (R := R) (G := G) K
map_add' := completedGroupAlgebraOpenFiniteQuotientLimitProjection_add (R := R) (G := G) K
map_mul' := completedGroupAlgebraOpenFiniteQuotientLimitProjection_mul (R := R) (G := G) KThe projection from the two-parameter limit to one quotient is bundled as a ring homomorphism.
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjectionRingHom_apply
[IsTopologicalRing R]
(K : CompletedGroupAlgebraOpenQuotientIndex R G)
(x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
completedGroupAlgebraOpenFiniteQuotientLimitProjectionRingHom R G K x =
completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K xThe ring-homomorphism projection has the same underlying coordinate map as the finite-stage projection.
Show proof
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. 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.
□