ProCGroups.ProC.Kernels
This module develops finite quotient, subgroup, free pro-\(C\), generation, and cardinal-invariant constructions for profinite and pro-\(C\) groups.
import
- Mathlib.GroupTheory.Abelianization.Defs
- ProCGroups.Abelian.TopologicalAbelianization
- ProCGroups.ProC.Subgroups.Closed
abbrev ProfiniteKernelSubgroup (psi : ContinuousMonoidHom G H) : Subgroup G :=
psi.toMonoidHom.kerThe kernel subgroup of a continuous homomorphism.
theorem isClosed_profiniteKernelSubgroup [T1Space H] (psi : ContinuousMonoidHom G H) :
IsClosed ((ProfiniteKernelSubgroup psi : Subgroup G) : Set G)The kernel of a continuous homomorphism into a \(T_1\) topological group is closed.
Show proof
by
simpa [ProfiniteKernelSubgroup, MonoidHom.mem_ker] using
(isClosed_singleton (x := (1 : H))).preimage psi.continuous_toFunProof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□abbrev ProfiniteKernelAbelianization (psi : ContinuousMonoidHom G H) : Type u :=
TopologicalAbelianization (ProfiniteKernelSubgroup psi)abbrev ProfiniteKernelAbelianizationAdd (psi : ContinuousMonoidHom G H) : Type u :=
Additive (ProfiniteKernelAbelianization psi)Additive notation for the topological kernel abelianization.
abbrev ProCKernelAbelianization
(ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H) : Type u :=
let _proCMarker : ProCGroupPredicate.{u} := ProC
ProfiniteKernelAbelianization psiThis declaration introduces the pro-\(C\) notation for the topological kernel abelianization. The ProC parameter records the ambient pro-\(C\) theory in theorem statements; the underlying type is the ordinary topological abelianization of the closed kernel.
abbrev ProCKernelAbelianizationAdd
(ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H) : Type u :=
Additive (ProCKernelAbelianization ProC psi)Additive notation for the pro-\(C\) kernel abelianization.
def kernelAbelianizationToProfiniteKernelAbelianizationHom
(psi : ContinuousMonoidHom G H) :
Abelianization (ProfiniteKernelSubgroup psi) →*
ProfiniteKernelAbelianization psi :=
QuotientGroup.lift
(commutator (ProfiniteKernelSubgroup psi))
(QuotientGroup.mk'
(Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)))
(by
intro x hx
exact
(QuotientGroup.eq_one_iff
(N := Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) x).2
(Subgroup.commutator_le_closedCommutator (ProfiniteKernelSubgroup psi) hx))The canonical quotient map from the algebraic kernel abelianization to the topological kernel abelianization.
def kernelAbelianizationToProfiniteKernelAbelianization
(psi : ContinuousMonoidHom G H) :
Additive (Abelianization (ProfiniteKernelSubgroup psi)) →+
ProfiniteKernelAbelianizationAdd psi :=
(kernelAbelianizationToProfiniteKernelAbelianizationHom
(G := G) (H := H) psi).toAdditiveAdditive form of the quotient from \((\ker \psi)^{ab}\) to the topological kernel abelianization.
theorem kernelAbelianizationToProfiniteKernelAbelianization_of
(psi : ContinuousMonoidHom G H) (n : ProfiniteKernelSubgroup psi) :
kernelAbelianizationToProfiniteKernelAbelianization
(G := G) (H := H) psi (Additive.ofMul (Abelianization.of n)) =
Additive.ofMul
(QuotientGroup.mk'
(Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) n)The canonical quotient map sends the class of a kernel element to its class modulo the topological closure of the commutator subgroup.
Show proof
by
rflProof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□theorem kernelAbelianizationToProfiniteKernelAbelianization_surjective
(psi : ContinuousMonoidHom G H) :
Function.Surjective
(kernelAbelianizationToProfiniteKernelAbelianization
(G := G) (H := H) psi)The canonical map from the algebraic kernel abelianization to the topological one is surjective.
Show proof
by
intro x
change ∃ y : Additive (Abelianization (ProfiniteKernelSubgroup psi)),
Additive.ofMul
(kernelAbelianizationToProfiniteKernelAbelianizationHom
(G := G) (H := H) psi (Additive.toMul y)) = x
rcases QuotientGroup.mk'_surjective
(Subgroup.closedCommutator (ProfiniteKernelSubgroup psi))
(Additive.toMul x) with
⟨n, hn⟩
refine ⟨Additive.ofMul (Abelianization.of n), ?_⟩
apply Additive.toMul.injective
simpa using hnProof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□theorem proCGroup_profiniteKernelSubgroup
(ProC : ProCGroupPredicate.{u})
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients] [ProCGroup ProC G]
[T1Space H] (psi : ContinuousMonoidHom G H) :
ProCGroup ProC (ProfiniteKernelSubgroup psi)The closed kernel of a morphism out of a pro-\(C\) group is pro-\(C\).
Show proof
ProCGroup.of_isClosed_subgroup ProC (ProfiniteKernelSubgroup psi)
(isClosed_profiniteKernelSubgroup psi)Proof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□theorem proCGroup_profiniteKernelSubgroup_of_proCGroupTarget
(ProC : ProCGroupPredicate.{u})
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients] [ProCGroup ProC G]
{H0 : Type u} [Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
[ProCGroup ProC H0] (psi : ContinuousMonoidHom G H0) :
ProCGroup ProC (ProfiniteKernelSubgroup psi)The closed kernel of a morphism between pro-\(C\) groups is pro-\(C\). This form avoids a separate public \(T_1\)-space assumption because the pro-\(C\) target is Hausdorff.
Show proof
by
letI : T1Space H0 := ProCGroup.t1Space ProC H0
exact proCGroup_profiniteKernelSubgroup (G := G) (H := H0) ProC psiProof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□theorem ProCGroup.profiniteKernelSubgroup
(ProC : ProCGroupPredicate.{u})
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients]
{G H0 : Type u}
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
[ProCGroup ProC G] [ProCGroup ProC H0]
(psi : ContinuousMonoidHom G H0) :
ProCGroup ProC (ProfiniteKernelSubgroup psi)Public namespace form: the kernel of a morphism of pro-\(C\) groups is pro-\(C\).
Show proof
proCGroup_profiniteKernelSubgroup_of_proCGroupTarget
(G := G) (H0 := H0) ProC psiProof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□theorem proCGroup_profiniteKernelAbelianization
(ProC : ProCGroupPredicate.{u})
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients] [ProCGroup ProC G]
[T1Space H] (psi : ContinuousMonoidHom G H) :
ProCGroup ProC (ProCKernelAbelianization ProC psi)The topological kernel abelianization of a morphism out of a pro-\(C\) group is pro-\(C\).
Show proof
by
let N : Subgroup G := ProfiniteKernelSubgroup psi
letI : ProCGroup ProC N :=
proCGroup_profiniteKernelSubgroup (G := G) (H := H) ProC psi
change ProCGroup ProC (N ⧸ Subgroup.closedCommutator N)
exact ProCGroup.quotient_closedNormalSubgroup ProC
(Subgroup.closedCommutator N)
(Subgroup.isClosed_closedCommutator N)Proof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□theorem proCGroup_profiniteKernelAbelianization_of_proCGroupTarget
(ProC : ProCGroupPredicate.{u})
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients] [ProCGroup ProC G]
{H0 : Type u} [Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
[ProCGroup ProC H0] (psi : ContinuousMonoidHom G H0) :
ProCGroup ProC (ProCKernelAbelianization ProC psi)The topological kernel abelianization of a morphism between pro-\(C\) groups is pro-\(C\), without requiring a separate public \(T_1\)-space assumption on the target.
Show proof
by
letI : T1Space H0 := ProCGroup.t1Space ProC H0
exact proCGroup_profiniteKernelAbelianization (G := G) (H := H0) ProC psiProof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□theorem ProCGroup.profiniteKernelAbelianization
(ProC : ProCGroupPredicate.{u})
[ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
[ProC.DeterminedByFiniteQuotients]
{G H0 : Type u}
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[Group H0] [TopologicalSpace H0] [IsTopologicalGroup H0]
[ProCGroup ProC G] [ProCGroup ProC H0]
(psi : ContinuousMonoidHom G H0) :
ProCGroup ProC (ProCKernelAbelianization ProC psi)Public namespace form: the topological N^ab(C) of a morphism of pro-\(C\) groups is pro-\(C\).
Show proof
proCGroup_profiniteKernelAbelianization_of_proCGroupTarget
(G := G) (H0 := H0) ProC psiProof. Unfold the kernel as the closed subgroup of elements mapped to \(1\). Closedness follows from continuity and the \(T_1\) target, and the topological kernel abelianization is the quotient of that closed kernel by the closure of its commutator subgroup. The canonical maps are checked on representatives, surjectivity follows from quotient construction, and pro-\(C\) membership follows from permanence under closed subgroups and quotients.
□