ProCGroups/GroupTheory/Subgroups.lean

1import Mathlib.GroupTheory.QuotientGroup.Basic

2import Mathlib.Topology.Algebra.OpenSubgroup

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/ProCGroups/GroupTheory/Subgroups.lean

8translation_root: data/translation

9purpose: identifies the local data snapshot used to build pages/

10placement: after imports, never before imports

12/-!

13# Subgroup relation helpers

15Group-theoretic normal-in-subgroup and subnormal-subgroup predicates used by

16profinite applications.

19namespace ProCGroups.GroupTheory

21universe u

23variable {G : Type u} [Group G]

25/-- `H` is normal in `K` as an ambient subgroup relation. -/

26def IsNormalIn (H K : Subgroup G) : Prop :=

27 H ≤ K ∧ ∀ ⦃k h : G⦄, k ∈ K → h ∈ H → k * h * k⁻¹ ∈ H

29/-- The transitive closure of the ambient normal-subgroup relation. -/

30inductive IsSubnormalSubgroupOf : Subgroup G → Subgroup G → Prop

31 | refl (H : Subgroup G) : IsSubnormalSubgroupOf H H

32 | step {H K L : Subgroup G} :

35/-- An open subgroup is open subnormal if it is subnormal in the ambient group. -/

36def IsOpenSubnormalSubgroup [TopologicalSpace G] (H : OpenSubgroup G) : Prop :=

37 IsSubnormalSubgroupOf (G := G) (H : Subgroup G) ⊤

39/-- The canonical embedding of a kernel quotient into the target range, viewed in the target. -/

41 {G T : Type u} [Group G] [Group T] (φ : G →* T) :

42 G ⧸ φ.ker →* T :=

43 φ.range.subtype.comp (QuotientGroup.quotientKerEquivRange φ).toMonoidHom

46 {G T : Type u} [Group G] [Group T] (φ : G →* T) :

47 Function.Injective (quotientKerEmbedding φ) := by

48 exact

49 φ.range.subtype_injective.comp

50 (QuotientGroup.quotientKerEquivRange φ).injective

53 {G T : Type u} [Group G] [Group T] (φ : G →* T) (x : G) :

54 quotientKerEmbedding φ (QuotientGroup.mk' φ.ker x) = φ x := by

55 rfl

57end ProCGroups.GroupTheory