FenchelNielsenZomorrodian.Profinite.CharacteristicClosure
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
noncomputable def openNormalAutComap (φ : G ≃ₜ* G)
(U : OpenNormalSubgroup G) : OpenNormalSubgroup G :=
ProCGroups.OpenNormalSubgroup.comap φ.toContinuousMonoidHom.toMonoidHom
φ.continuous_toFun U
@[local simp]Pull an open normal subgroup back along a continuous automorphism.
theorem mem_openNormalAutComap {φ : G ≃ₜ* G}
{U : OpenNormalSubgroup G} {x : G} :
x ∈ openNormalAutComap φ U ↔ φ x ∈ UMembership in the automorphism comap of an open normal subgroup is characterized by applying the automorphism.
Show proof
Iff.rflProof. Unfold the arithmetic, signature, quotient, or subgroup definition named in the statement. The result is a direct numerical, topological, or kernel-property calculation rather than a generic presentation-relator check.
□noncomputable def openNormalAutComapOrbitSubgroups
(U : OpenNormalSubgroup G) : Set (Subgroup G) :=
Set.range fun φ : G ≃ₜ* G =>
((openNormalAutComap φ U : OpenNormalSubgroup G) : Subgroup G)The automorphic orbit of an open normal subgroup is viewed as a set of ordinary subgroups.
theorem openNormalAutComapOrbitSubgroups_finite
(hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
(openNormalAutComapOrbitSubgroups U).FiniteShow proof
by
classical
let n := Nat.card (G ⧸ (U : Subgroup G))
refine (finite_openSubgroupsOfIndexLE_of_hasFiniteOpenSubgroupsOfIndex
(G := G) hfin n).subset ?_
intro V hV
rcases hV with ⟨φ, hφ⟩
rw [← hφ]
have hopen :
IsOpen
(((openNormalAutComap φ U : OpenNormalSubgroup G) : Subgroup G) :
Set G) :=
ProCGroups.openNormalSubgroup_isOpen (G := G) (openNormalAutComap φ U)
have hfinite :
Finite
(G ⧸ ((openNormalAutComap φ U : OpenNormalSubgroup G) :
Subgroup G)) :=
Subgroup.quotient_finite_of_isOpen _ hopen
refine ⟨hopen, hfinite, ?_⟩
simpa [openNormalAutComap, Subgroup.index_eq_card, n] using
(Subgroup.index_comap_of_surjective
(H := (U : Subgroup G)) φ.surjective).leProof. 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. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup 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.
□theorem openNormalAutComapOrbitSubgroups_open
(hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
IsOpen ((sInf (openNormalAutComapOrbitSubgroups U) : Subgroup G) :
Set G)The intersection of the automorphic orbit of an open normal subgroup is open.
Show proof
by
apply ProCGroups.FiniteGeneration.Subgroup.isOpen_sInf_of_finite
· exact openNormalAutComapOrbitSubgroups_finite (G := G) hfin U
· intro V hV
rcases hV with ⟨φ, hφ⟩
rw [← hφ]
exact ProCGroups.openNormalSubgroup_isOpen (G := G) (openNormalAutComap φ U)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. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup 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.
□theorem openNormalAutComapOrbitSubgroups_normal (U : OpenNormalSubgroup G) :
(sInf (openNormalAutComapOrbitSubgroups U)).NormalThe intersection of the automorphic orbit of an open normal subgroup is normal.
Show proof
by
rw [sInf_eq_iInf']
exact Subgroup.normal_iInf_normal fun V : openNormalAutComapOrbitSubgroups U => by
rcases V.2 with ⟨φ, hφ⟩
rw [← hφ]
exact (openNormalAutComap φ U).isNormal'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. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. 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.
□noncomputable def openNormalCharacteristicClosure
(hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
OpenNormalSubgroup G where
toOpenSubgroup :=
{ toSubgroup := sInf (openNormalAutComapOrbitSubgroups U)
isOpen' := openNormalAutComapOrbitSubgroups_open (G := G) hfin U }
isNormal' := openNormalAutComapOrbitSubgroups_normal (G := G) UThe characteristic closure of an open normal subgroup in a finitely generated profinite group.
theorem openNormalCharacteristicClosure_le
(hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
(openNormalCharacteristicClosure (G := G) hfin U : Subgroup G) ≤
(U : Subgroup G)The characteristic closure of an open normal subgroup is contained in the original subgroup.
Show proof
by
intro x hx
have hx' : x ∈ sInf (openNormalAutComapOrbitSubgroups U) := hx
rw [Subgroup.mem_sInf] at hx'
exact hx' _ ⟨ContinuousMulEquiv.refl G, by ext y; simp only [openNormalAutComap, ContinuousMonoidHom.coe_toMonoidHom,
ProCGroups.OpenNormalSubgroup.toSubgroup_comap, Subgroup.mem_comap, MonoidHom.coe_coe,
ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.refl_apply, OpenSubgroup.mem_toSubgroup]⟩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 openNormalCharacteristicClosure_characteristic
(hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
IsTopologicallyCharacteristic G
(openNormalCharacteristicClosure (G := G) hfin U : Subgroup G)The characteristic closure is topologically characteristic.
Show proof
by
intro ψ g
constructor
· intro hg
change ψ g ∈ sInf (openNormalAutComapOrbitSubgroups U) at hg
change g ∈ sInf (openNormalAutComapOrbitSubgroups U)
rw [Subgroup.mem_sInf] at hg ⊢
intro V hV
rcases hV with ⟨φ, hφ⟩
rw [← hφ]
have hmem :
ψ g ∈ (openNormalAutComap (ψ.symm.trans φ) U :
OpenNormalSubgroup G) :=
hg _ ⟨ψ.symm.trans φ, rfl⟩
simpa [openNormalAutComap] using hmem
· intro hg
change g ∈ sInf (openNormalAutComapOrbitSubgroups U) at hg
change ψ g ∈ sInf (openNormalAutComapOrbitSubgroups U)
rw [Subgroup.mem_sInf] at hg ⊢
intro V hV
rcases hV with ⟨φ, hφ⟩
rw [← hφ]
have hmem :
g ∈ (openNormalAutComap (ψ.trans φ) U : OpenNormalSubgroup G) :=
hg _ ⟨ψ.trans φ, rfl⟩
simpa [openNormalAutComap] using hmemProof. 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.
□noncomputable def profiniteOpenCharacteristicClosure
(hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
ProfiniteOpenCharacteristicSubgroup G :=
⟨openNormalCharacteristicClosure (G := G) hfin U,
openNormalCharacteristicClosure_characteristic (G := G) hfin U⟩The same closure is bundled as a profinite open characteristic subgroup.
theorem profiniteOpenCharacteristicClosure_torsionFree
(hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G)
(htf : ProfiniteOpenNormalSubgroupTorsionFree G U) :
ProfiniteOpenNormalSubgroupTorsionFree G
(profiniteOpenCharacteristicClosure (G := G) hfin U).toOpenNormalSubgroupThe profinite open characteristic closure preserves the required torsion-freeness property.
Show proof
by
intro x hx hfinord
exact htf x (openNormalCharacteristicClosure_le (G := G) hfin U hx) hfinordProof. 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. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup 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. 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_torsionFree_openCharacteristicSubgroup_of_exists_torsionFree_openNormalSubgroup
(hfin : HasFiniteOpenSubgroupsOfIndex G)
(h : ∃ U : OpenNormalSubgroup G, ProfiniteOpenNormalSubgroupTorsionFree G U) :
∃ U : ProfiniteOpenCharacteristicSubgroup G,
ProfiniteOpenNormalSubgroupTorsionFree G U.toOpenNormalSubgroupCharacteristic-closure existence package: in a finitely generated profinite group, any torsion-free open normal subgroup can be replaced by a torsion-free open characteristic subgroup.
Show proof
by
rcases h with ⟨U, htf⟩
exact
⟨profiniteOpenCharacteristicClosure (G := G) hfin U,
profiniteOpenCharacteristicClosure_torsionFree (G := G) hfin U htf⟩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 profiniteOpenCharacteristicClosure_derivedLength
(hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) {m : ℕ}
(hquot : ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U m) :
ProfiniteOpenCharacteristicQuotientHasDerivedLengthAtMost G
(profiniteOpenCharacteristicClosure (G := G) hfin U) mThe profinite open characteristic closure has the stated derived-length bound.
Show proof
by
have hDleU : profiniteDerivedSeries G m ≤ (U : Subgroup G) :=
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.topDerived_le U hquot
apply ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.of_topDerived_le
intro x hx
change x ∈ sInf (openNormalAutComapOrbitSubgroups U)
rw [Subgroup.mem_sInf]
intro V hV
rcases hV with ⟨φ, hφ⟩
rw [← hφ]
change φ x ∈ U
exact hDleU ((topDerivedTop_le_comap (f := φ.toContinuousMonoidHom) (m := m)) hx)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. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup 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. 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 hasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost_of_normal
(hfin : HasFiniteOpenSubgroupsOfIndex G) {m : ℕ}
(h :
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost G m) :
HasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost G mA torsion-free open characteristic subgroup can be chosen so that the corresponding quotient has the required derived-length bound.
Show proof
by
rcases h with ⟨U, htf, hquot⟩
refine
⟨profiniteOpenCharacteristicClosure (G := G) hfin U,
profiniteOpenCharacteristicClosure_torsionFree (G := G) hfin U htf,
profiniteOpenCharacteristicClosure_derivedLength (G := G) hfin U hquot⟩Proof. Check the quotient data on the named elliptic, surface, cusp, and boundary generators. The period, power, and product relators follow from the displayed order and product calculations, so the presentation universal property supplies the quotient map; derived-length, smoothness, and profinite fields are inherited from the finite or profinite quotient construction.
□