ProCGroups.FreeProC.Criteria.AbstractResidual
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.
import
- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
- ProCGroups.FiniteGroups.StandardClasses
def EmbedsInFinitePower
(S : Type u) [Group S]
(G : Type u) [Group G] : Prop :=
Finite G ∧ ∃ ι : Type u, Finite ι ∧ ∃ f : G →* (ι → S), Function.Injective fdef ContainsAllFiniteSGroups
(C : ProCGroups.FiniteGroupClass.{u})
(S : Type u) [Group S] : Prop :=
∀ {G : Type u} [Group G], EmbedsInFinitePower S G → C Gdef HasGeneratorRankAtMost
(G : Type u) [Group G] (κ : Cardinal) : Prop :=
∃ X : Type u, Cardinal.mk X ≤ κ ∧ ∃ φ : FreeGroup X →* G, Function.Surjective φAn abstract group has generator rank at most \(\kappa\) if it is a quotient of a free group on a set of cardinality at most \(\kappa\).
def IsResiduallyFiniteGroupClass
(C : ProCGroups.FiniteGroupClass.{u})
(G : Type u) [Group G] : Prop :=
∀ g : G, g ≠ 1 →
∃ Q : Type u, ∃ _ : Group Q, C Q ∧ ∃ φ : G →* Q, φ g ≠ 1Residual \(C\)-ness for an abstract group, written directly in terms of separating nontrivial elements by finite \(C\)-quotients.
def IsResiduallyFiniteSGroups
(S : Type u) [Group S]
(G : Type u) [Group G] : Prop :=
∀ g : G, g ≠ 1 →
∃ Q : Type u, ∃ _ : Group Q, EmbedsInFinitePower S Q ∧ ∃ φ : G →* Q, φ g ≠ 1theorem embedsInFinitePower_pi
(S : Type u) [Group S] [Finite S]
(ι : Type u) [Finite ι] :
EmbedsInFinitePower S (ι → S)Show proof
by
refine ⟨inferInstance, ι, inferInstance, MonoidHom.id (ι → S), ?_⟩
exact fun _ _ h => hProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem embedsInFinitePower_self
(S : Type u) [Group S] [Finite S] :
EmbedsInFinitePower S SShow proof
by
let f : S →* (PUnit.{u + 1} → S) :=
{ toFun := fun s _ => s
map_one' := by
funext _
rfl
map_mul' := by
intro _ _
funext _
rfl }
refine ⟨inferInstance, PUnit.{u + 1}, inferInstance, f, ?_⟩
intro a b h
exact congrFun h PUnit.unitProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem EmbedsInFinitePower.of_injective
{S : Type u} [Group S] {G H : Type u} [Group G] [Group H]
[Finite G] (hH : EmbedsInFinitePower S H) (f : G →* H)
(hf : Function.Injective f) :
EmbedsInFinitePower S GShow proof
by
rcases hH with ⟨_, ι, hι, e, he⟩
exact ⟨inferInstance, ι, hι, e.comp f, he.comp hf⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem EmbedsInFinitePower.subgroup
{S : Type u} [Group S] {G : Type u} [Group G]
(hG : EmbedsInFinitePower S G) (H : Subgroup G) :
EmbedsInFinitePower S HShow proof
by
rcases hG with ⟨hfinite, ι, hι, f, hf⟩
haveI : Finite G := hfinite
haveI : Finite H := Finite.of_injective ((↑) : H → G) Subtype.coe_injective
exact ⟨inferInstance, ι, hι, f.comp H.subtype, hf.comp Subtype.coe_injective⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 EmbedsInFinitePower.prod
{S : Type u} [Group S] {G H : Type u} [Group G] [Group H]
(hG : EmbedsInFinitePower S G) (hH : EmbedsInFinitePower S H) :
EmbedsInFinitePower S (G × H)Show proof
by
rcases hG with ⟨hfiniteG, ιG, hιG, fG, hfG⟩
rcases hH with ⟨hfiniteH, ιH, hιH, fH, hfH⟩
haveI : Finite G := hfiniteG
haveI : Finite H := hfiniteH
haveI : Finite ιG := hιG
haveI : Finite ιH := hιH
let f : G × H →* (Sum ιG ιH → S) :=
{ toFun := fun gh i =>
match i with
| Sum.inl iG => fG gh.1 iG
| Sum.inr iH => fH gh.2 iH
map_one' := by
funext i
cases i
· simp only [Prod.fst_one, map_one, Pi.one_apply]
· simp only [Prod.snd_one, map_one, Pi.one_apply]
map_mul' := by
intro a b
funext i
cases i
· simp only [Prod.fst_mul, map_mul, Pi.mul_apply]
· simp only [Prod.snd_mul, map_mul, Pi.mul_apply] }
refine ⟨inferInstance, Sum ιG ιH, inferInstance, f, ?_⟩
intro a b hab
apply Prod.ext
· apply hfG
funext i
exact congrFun hab (Sum.inl i)
· apply hfH
funext i
exact congrFun hab (Sum.inr i)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem EmbedsInFinitePower.pow_exponent_eq_one
{S : Type u} [Group S] {G : Type u} [Group G]
(hG : EmbedsInFinitePower S G) (g : G) :
g ^ Monoid.exponent S = 1Every finite \(S\)-group is killed by the exponent of \(S\).
Show proof
by
rcases hG with ⟨_, ι, _, f, hf⟩
apply hf
funext i
rw [map_pow, map_one]
exact Monoid.pow_exponent_eq_one (f g i)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem EmbedsInFinitePower.map_pow_exponent_eq_one
{S : Type u} [Group S] {G Q : Type u} [Group G] [Group Q]
(hQ : EmbedsInFinitePower S Q) (φ : G →* Q) (g : G) :
φ (g ^ Monoid.exponent S) = 1Homomorphisms into finite \(S\)-groups kill every \(S\)-exponent power.
Show proof
by
rw [map_pow]
exact hQ.pow_exponent_eq_one (φ g)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem not_isResiduallyFiniteSGroups_of_pow_exponent_ne_one
{S : Type u} [Group S] {G : Type u} [Group G] {g : G}
(hg : g ^ Monoid.exponent S ≠ 1) :
¬ IsResiduallyFiniteSGroups S GIf some \(S\)-exponent power is nontrivial, finite \(S\)-groups cannot separate all nontrivial elements.
Show proof
by
intro hres
rcases hres (g ^ Monoid.exponent S) hg with ⟨Q, hQGroup, hQ, φ, hφ⟩
letI : Group Q := hQGroup
exact hφ (hQ.map_pow_exponent_eq_one φ g)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem freeGroup_of_pow_ne_one
{X : Type u} (x : X) {n : ℕ} (hn : n ≠ 0) :
(FreeGroup.of x : FreeGroup X) ^ n ≠ 1A nonzero power of a free generator is nontrivial.
Show proof
by
intro hpow
have hx : (FreeGroup.of x : FreeGroup X) = 1 :=
(pow_eq_one_iff_left (M := FreeGroup X) hn).mp hpow
exact FreeGroup.of_ne_one x hxProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem not_isResiduallyFiniteSGroups_freeGroup_of_nonempty
(S : Type u) [Group S] [Finite S] {X : Type u} (x : X) :
¬ IsResiduallyFiniteSGroups S (FreeGroup X)Finite \(S\)-groups alone cannot make a nonempty free group residually \(S\).
Show proof
not_isResiduallyFiniteSGroups_of_pow_exponent_ne_one
(S := S) (G := FreeGroup X) (g := FreeGroup.of x)
(freeGroup_of_pow_ne_one x (Monoid.exponent_ne_zero_of_finite (G := S)))Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem ContainsAllFiniteSGroups.pi_mem
{C : ProCGroups.FiniteGroupClass.{u}} {S : Type u} [Group S] [Finite S]
(hcontains : ContainsAllFiniteSGroups C S)
(ι : Type u) [Finite ι] :
C (ι → S)Show proof
hcontains (embedsInFinitePower_pi S ι)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem ContainsAllFiniteSGroups.self_mem
{C : ProCGroups.FiniteGroupClass.{u}} {S : Type u} [Group S] [Finite S]
(hcontains : ContainsAllFiniteSGroups C S) :
C SA class containing all finite \(S\)-groups contains \(S\) itself.
Show proof
hcontains (embedsInFinitePower_self S)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□