FenchelNielsenZomorrodian/Profinite/MainTheorem.lean
1import FenchelNielsenZomorrodian.Profinite.CharacteristicClosure
2import FenchelNielsenZomorrodian.Profinite.CuspedQuotient
3import FenchelNielsenZomorrodian.Profinite.DiscreteBridge
4import FenchelNielsenZomorrodian.Profinite.LowPeriodQuotient
5import FenchelNielsenZomorrodian.Profinite.PositiveGenusQuotient
6import FenchelNielsenZomorrodian.Profinite.TorsionFrontier
8/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/FenchelNielsenZomorrodian/Profinite/MainTheorem.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# Profinite Fenchel-Nielsen main theorems
19This file is the public theorem entry point for the profinite Fenchel-Nielsen-Zomorrodian
20formalization.
21-/
23namespace FenchelNielsen
25universe u
27namespace ProfiniteFGroup
29/-- Profinite Fenchel-Nielsen existence theorem, normal-subgroup form.
31Every profinite Fenchel group has a torsion-free open normal subgroup. This theorem is not
32restricted to non-perfect groups. -/
34 (Δ : ProfiniteFGroup.{u}) :
35 ∃ U : OpenNormalSubgroup Δ.carrier,
36 ProfiniteOpenNormalSubgroupTorsionFree Δ.carrier U :=
39/-- Profinite Fenchel-Nielsen existence theorem, characteristic-subgroup form.
41Every profinite Fenchel group has a torsion-free open characteristic subgroup. This is the
42existence-only theorem and does not assume non-perfectness. -/
44 (Δ : ProfiniteFGroup.{u}) :
45 ∃ U : ProfiniteOpenCharacteristicSubgroup Δ.carrier,
46 ProfiniteOpenNormalSubgroupTorsionFree Δ.carrier U.toOpenNormalSubgroup := by
47 letI : CompactSpace Δ.carrier := Δ.isProfinite.compactSpace
48 exact
50 (G := Δ.carrier) Δ.finiteOpenSubgroupsOfIndex
53private theorem threeStep_normal_of_isNonPerfect
54 (Δ : ProfiniteFGroup.{u}) :
55 Δ.IsNonPerfect →
57 Δ.carrier 3 := by
58 intro hNonPerfect
59 by_cases hCusps : Δ.signature.HasCusps
60 · exact
61 ProfiniteSmoothQuotientData.has_torsionFreeOpenNormal_quotient_derivedLength_le
62 (cuspedSmoothQuotientData Δ hCusps) (by decide : 1 ≤ 3)
63 · have hCompact : Δ.signature.IsCompact := by
64 dsimp [FenchelSignature.HasCusps, FenchelSignature.IsCompact] at hCusps ⊢
65 omega
66 by_cases hGenus : 1 ≤ Δ.signature.orbitGenus
67 · exact
68 ProfiniteSmoothQuotientData.has_torsionFreeOpenNormal_quotient_derivedLength_le
69 (positiveGenusSmoothQuotientData Δ hGenus) (by decide : 2 ≤ 3)
70 · have hZero : Δ.signature.orbitGenus = 0 := by omega
71 by_cases hPeriods : 3 ≤ Δ.signature.numPeriods
72 · exact
74 Δ hNonPerfect hCompact hZero hPeriods
75 · have hTwo :
76 Δ.signature.numPeriods = 2 :=
78 Δ hNonPerfect hZero hCompact hPeriods
79 exact
80 ProfiniteSmoothQuotientData.has_torsionFreeOpenNormal_quotient_derivedLength_le
81 (twoPeriodCyclicSmoothQuotientData Δ hCompact hZero hTwo) (by decide : 1 ≤ 3)
83/-- Normal-subgroup form of the non-perfect three-step Fenchel-Nielsen theorem. -/
85 (Δ : ProfiniteFGroup.{u}) :
86 Δ.IsNonPerfect →
88 Δ.carrier 3 :=
91/-- Characteristic-subgroup form of the non-perfect three-step Fenchel-Nielsen theorem. -/
93 (Δ : ProfiniteFGroup.{u}) :
94 Δ.IsNonPerfect →
96 Δ.carrier 3 := by
97 intro hNonPerfect
98 letI : CompactSpace Δ.carrier := Δ.isProfinite.compactSpace
99 exact
101 (G := Δ.carrier) Δ.finiteOpenSubgroupsOfIndex
102 (threeStep_normal_of_isNonPerfect Δ hNonPerfect)
106end FenchelNielsen