FenchelNielsenZomorrodian.Discrete.GroupTheory.Basic
This module studies basic for fenchel nielsen zomorrodian. A group is torsion-free when every element of finite order is trivial. A group is perfect when its commutator subgroup is the whole group.
import
- Mathlib.Tactic.NormNum.LegendreSymbol
def IsTorsionFreeGroup (G : Type*) [Group G] : Prop :=
∀ g : G, IsOfFinOrder g → g = 1A group is torsion-free when every element of finite order is trivial.
def IsPerfectGroup (G : Type*) [Group G] : Prop :=
derivedSeries G 1 = ⊤A group is perfect when its commutator subgroup is the whole group.
theorem isTorsionFreeGroup_of_mulEquiv
{G H : Type*} [Group G] [Group H] (e : G ≃* H)
(hTF : IsTorsionFreeGroup G) :
IsTorsionFreeGroup HTorsion-freeness is preserved across a multiplicative equivalence of groups.
Show proof
by
intro h hfin
have hpre :
e.symm h = 1 :=
hTF (e.symm h) (MonoidHom.isOfFinOrder e.symm.toMonoidHom hfin)
simpa using congrArg e hpreProof. 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. 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps. For equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously.
□theorem orderOf_map_eq_of_torsionFree_ker
{G H : Type*} [Group G] [Group H] (φ : G →* H)
(hker : IsTorsionFreeGroup φ.ker) {x : G} (hx : IsOfFinOrder x) :
orderOf (φ x) = orderOf xIf the kernel is torsion-free, the order of an element after mapping to the quotient is the same as its order modulo the kernel.
Show proof
by
apply Nat.dvd_antisymm
· exact orderOf_map_dvd φ x
· have hpowMap : φ (x ^ orderOf (φ x)) = 1 := by
rw [map_pow, pow_orderOf_eq_one]
let k : φ.ker := ⟨x ^ orderOf (φ x), hpowMap⟩
have hkfin : IsOfFinOrder k := by
have hxpow : IsOfFinOrder (x ^ orderOf (φ x)) := hx.pow
simpa [k] using
(Submonoid.isOfFinOrder_coe
(H := φ.ker.toSubmonoid) (x := k)).1 hxpow
have hkone : k = 1 := hker k hkfin
have hxpowOne : x ^ orderOf (φ x) = 1 := by
simpa [k] using congrArg Subtype.val hkone
exact orderOf_dvd_of_pow_eq_one hxpowOneProof. 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. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□