ProCGroups.GroupTheory.Subgroups
This module studies subgroups for pro cgroups. H is normal in K as an ambient subgroup relation. The transitive closure of the ambient normal-subgroup relation.
import
- Mathlib.GroupTheory.QuotientGroup.Basic
- Mathlib.Topology.Algebra.OpenSubgroup
def IsNormalIn (H K : Subgroup G) : Prop :=
H ≤ K ∧ ∀ ⦃k h : G⦄, k ∈ K → h ∈ H → k * h * k⁻¹ ∈ HH is normal in K as an ambient subgroup relation.
inductive IsSubnormalSubgroupOf : Subgroup G → Subgroup G → Prop
| refl (H : Subgroup G) : IsSubnormalSubgroupOf H H
| step {H K L : Subgroup G} :
IsNormalIn H K → IsSubnormalSubgroupOf K L → IsSubnormalSubgroupOf H LThe transitive closure of the ambient normal-subgroup relation.
def IsOpenSubnormalSubgroup [TopologicalSpace G] (H : OpenSubgroup G) : Prop :=
IsSubnormalSubgroupOf (G := G) (H : Subgroup G) ⊤An open subgroup is open subnormal if it is subnormal in the ambient group.
noncomputable def quotientKerEmbedding
{G T : Type u} [Group G] [Group T] (φ : G →* T) :
G ⧸ φ.ker →* T :=
φ.range.subtype.comp (QuotientGroup.quotientKerEquivRange φ).toMonoidHomThe canonical embedding of a kernel quotient into the target range, viewed in the target.
theorem quotientKerEmbedding_injective
{G T : Type u} [Group G] [Group T] (φ : G →* T) :
Function.Injective (quotientKerEmbedding φ)The quotient-kernel embedding is injective.
Show proof
by
exact
φ.range.subtype_injective.comp
(QuotientGroup.quotientKerEquivRange φ).injectiveProof. 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. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. 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.
□theorem quotientKerEmbedding_mk
{G T : Type u} [Group G] [Group T] (φ : G →* T) (x : G) :
quotientKerEmbedding φ (QuotientGroup.mk' φ.ker x) = φ xThe quotient-kernel embedding sends a representative to the corresponding kernel coset.
Show proof
by
rflProof. 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. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. 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.
□