FenchelNielsenZomorrodian.Profinite.TorsionFrontier
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
def finiteSubgroupLeConjInertia
(Δ : ProfiniteFGroup.{u}) (K : Subgroup Δ.carrier) : Prop :=
∃ i : Fin Δ.signature.numPeriods, ∃ c : Δ.carrier,
∀ k : K, ∃ n : ℤ,
(k : Δ.carrier) = c * Δ.inertia i ^ n * c⁻¹
/- FRONTIER `profinite-fgroup-torsion-theorem`.
This is the profinite torsion theorem allowed by the user: finite subgroups of
a profinite F-group are controlled by the stack inertia groups. It is kept
separate from the discrete Fuchsian torsion frontier.
-/A subgroup is contained in a conjugate of one inertia group, up to powers.
axiom finiteSubgroup_le_conj_inertia
(Δ : ProfiniteFGroup.{u})
(K : Subgroup Δ.carrier) [Finite K]
(hK : K ≠ ⊥) :
Δ.finiteSubgroupLeConjInertia KFinite nontrivial profinite \(F\)-subgroups lie in conjugates of inertia groups.
theorem finiteOrder_isConj_inertia_zpow_of_ne_one
(Δ : ProfiniteFGroup.{u}) (g : Δ.carrier)
(hg : IsOfFinOrder g) (hgne : g ≠ 1) :
∃ i : Fin Δ.signature.numPeriods, ∃ n : ℤ,
IsConj g (Δ.inertia i ^ n)Finite nontrivial profinite F-subgroups lie in conjugates of inertia groups.
Show proof
by
classical
let K : Subgroup Δ.carrier := Subgroup.zpowers g
letI : Fintype K := Fintype.ofEquiv (Fin (orderOf g)) (finEquivZPowers hg)
letI : Finite K := Finite.of_fintype K
have hKne : K ≠ ⊥ := by
intro hK
have hgmem : g ∈ K := Subgroup.mem_zpowers g
have hgbot : g ∈ (⊥ : Subgroup Δ.carrier) := by
simpa [K, hK] using hgmem
exact hgne (Subgroup.mem_bot.mp hgbot)
rcases finiteSubgroup_le_conj_inertia Δ K hKne with
⟨i, c, hcontain⟩
rcases hcontain ⟨g, Subgroup.mem_zpowers g⟩ with ⟨n, hn⟩
exact ⟨i, n, (isConj_iff.2 ⟨c, hn.symm⟩).symm⟩Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def avoidsNontrivialInertia
(Δ : ProfiniteFGroup.{u}) (U : OpenNormalSubgroup Δ.carrier) : Prop :=
∀ i : Fin Δ.signature.numPeriods, ∀ n : ℤ,
Δ.inertia i ^ n ∈ (U : Subgroup Δ.carrier) →
Δ.inertia i ^ n = 1An open normal subgroup avoids the nontrivial profinite inertia powers.
theorem torsionFree_of_avoidsNontrivialInertia
(Δ : ProfiniteFGroup.{u}) (U : OpenNormalSubgroup Δ.carrier)
(hAvoid : Δ.avoidsNontrivialInertia U) :
ProfiniteOpenNormalSubgroupTorsionFree Δ.carrier UAvoiding nontrivial inertia powers makes an open normal subgroup torsion-free.
Show proof
by
intro x hx hxfin
by_cases hx1 : x = 1
· exact hx1
· rcases finiteOrder_isConj_inertia_zpow_of_ne_one Δ x hxfin hx1 with
⟨i, n, hconj⟩
have hinU : Δ.inertia i ^ n ∈ (U : Subgroup Δ.carrier) := by
rcases isConj_iff.1 hconj with ⟨c, hc⟩
rw [← hc]
exact U.isNormal'.conj_mem x hx c
have hpow1 : Δ.inertia i ^ n = 1 := hAvoid i n hinU
exact isConj_one_left.mp (by simpa [hpow1] using hconj)Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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 exists_openNormal_avoidsNontrivialInertia
(Δ : ProfiniteFGroup.{u}) :
∃ U : OpenNormalSubgroup Δ.carrier,
Δ.avoidsNontrivialInertia UThere is an open normal subgroup avoiding all nontrivial inertia powers.
Show proof
by
classical
have hEach :
∀ i : Fin Δ.signature.numPeriods,
∃ U : OpenNormalSubgroup Δ.carrier,
((U : Subgroup Δ.carrier) ⊓
Subgroup.zpowers (Δ.inertia i)) = ⊥ := by
intro i
let K : Subgroup Δ.carrier := Subgroup.zpowers (Δ.inertia i)
have hfinord : IsOfFinOrder (Δ.inertia i) := by
rw [← orderOf_pos_iff]
rw [Δ.inertia_order i]
exact lt_of_lt_of_le (by decide : 0 < 2) (Δ.signature.period_ge_two i)
letI : Fintype K :=
Fintype.ofEquiv (Fin (orderOf (Δ.inertia i)))
(finEquivZPowers hfinord)
letI : Finite K := Finite.of_fintype K
exact
ProCGroups.Generation.exists_openNormalSubgroup_inf_eq_bot_of_finite
(G := Δ.carrier) Δ.isProfinite K
choose U hU using hEach
by_cases hnonempty :
(Finset.univ : Finset (Fin Δ.signature.numPeriods)).Nonempty
· let V : OpenNormalSubgroup Δ.carrier :=
(Finset.univ : Finset (Fin Δ.signature.numPeriods)).inf' hnonempty U
refine ⟨V, ?_⟩
intro i n hn
have hVle : V ≤ U i := by
dsimp [V]
exact Finset.inf'_le
(s := (Finset.univ : Finset (Fin Δ.signature.numPeriods)))
(f := U) (b := i) (by simp only [Finset.mem_univ])
have hmemU : Δ.inertia i ^ n ∈ (U i : Subgroup Δ.carrier) :=
hVle hn
have hmemZ : Δ.inertia i ^ n ∈ Subgroup.zpowers (Δ.inertia i) :=
Subgroup.mem_zpowers_iff.2 ⟨n, rfl⟩
have hbot :
Δ.inertia i ^ n ∈ (⊥ : Subgroup Δ.carrier) := by
have hInf :
Δ.inertia i ^ n ∈
((U i : Subgroup Δ.carrier) ⊓
Subgroup.zpowers (Δ.inertia i)) :=
⟨hmemU, hmemZ⟩
simpa [hU i] using hInf
exact Subgroup.mem_bot.mp hbot
· refine ⟨⊤, ?_⟩
intro i
exact False.elim (hnonempty ⟨i, by simp only [Finset.mem_univ]⟩)Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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 exists_torsionFreeOpenNormalSubgroup
(Δ : ProfiniteFGroup.{u}) :
∃ U : OpenNormalSubgroup Δ.carrier,
ProfiniteOpenNormalSubgroupTorsionFree Δ.carrier UEvery profinite F-group has a torsion-free open normal subgroup.
Show proof
by
rcases exists_openNormal_avoidsNontrivialInertia Δ with ⟨U, hU⟩
exact ⟨U, torsionFree_of_avoidsNontrivialInertia Δ U hU⟩Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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.
□