Documentation

TauCeti.Combinatorics.PermutationTriple.Regular

Regular permutation triples #

A connected permutation triple is regular when its automorphism group — the simultaneous centralizer of its components — acts transitively on the sheets. These are the triples of the regular (Galois, normal) three-point covers: those whose deck group acts transitively on a fiber.

For a connected triple the automorphism group always acts freely on the sheets (TauCeti.PermutationTriple.eq_one_of_mem_automorphismGroup_of_apply_eq), so a regular triple is one whose automorphism group acts simply transitively. Dually, a triple is regular exactly when its monodromy group acts freely: an element of the monodromy group fixing one sheet fixes every translate of it by an automorphism, and conversely a free transitive monodromy action on Fin n identifies the sheets with the monodromy group, on which right multiplications are automorphisms. Counting then turns both characterisations into equalities of orders with the degree.

Main definitions #

Main results #

References #

source
def TauCeti.PermutationTriple.IsRegular {n : ℕ} (t : PermutationTriple n) :
Prop

A permutation triple is regular when it is connected and its automorphism group acts transitively on the sheets. The connectedness clause is not redundant: the automorphism group of the trivial triple is the whole symmetric group, which is transitive in every degree.

Equations
Instances For
    source
    theorem TauCeti.PermutationTriple.isRegular_iff {n : ℕ} {t : PermutationTriple n} :
    t.IsRegular ↔ t.IsConnected ∧ MulAction.IsPretransitive (↥t.automorphismGroup) (Fin n)
    source
    theorem TauCeti.PermutationTriple.IsRegular.isConnected {n : ℕ} {t : PermutationTriple n} (ht : t.IsRegular) :
    t.IsConnected
    source
    theorem TauCeti.PermutationTriple.IsRegular.isPretransitive {n : ℕ} {t : PermutationTriple n} (ht : t.IsRegular) :
    MulAction.IsPretransitive (↥t.automorphismGroup) (Fin n)
    source
    theorem TauCeti.PermutationTriple.IsRegular.isCancelSMul {n : ℕ} {t : PermutationTriple n} (ht : t.IsRegular) :
    IsCancelSMul (↥t.monodromyGroup) (Fin n)

    The monodromy group of a regular triple acts freely on the sheets.

    source
    theorem TauCeti.PermutationTriple.IsConnected.isRegular {n : ℕ} {t : PermutationTriple n} [IsCancelSMul (↥t.monodromyGroup) (Fin n)] (ht : t.IsConnected) :
    t.IsRegular

    A connected triple whose monodromy group acts freely on the sheets is regular: the monodromy group is then in bijection with the sheets, and right multiplications are automorphisms.

    source
    theorem TauCeti.PermutationTriple.isRegular_iff_isCancelSMul {n : ℕ} {t : PermutationTriple n} :
    t.IsRegular ↔ t.IsConnected ∧ IsCancelSMul (↥t.monodromyGroup) (Fin n)

    A triple is regular exactly when it is connected and its monodromy group acts freely on the sheets.

    source
    theorem TauCeti.PermutationTriple.isRegular_iff_card_monodromyGroup {n : ℕ} {t : PermutationTriple n} :
    t.IsRegular ↔ t.IsConnected ∧ Nat.card ↥t.monodromyGroup = n

    A triple is regular exactly when it is connected and its monodromy group has order equal to the degree.

    source
    theorem TauCeti.PermutationTriple.isRegular_iff_card_automorphismGroup {n : ℕ} {t : PermutationTriple n} :
    t.IsRegular ↔ t.IsConnected ∧ Nat.card ↥t.automorphismGroup = n

    A triple is regular exactly when it is connected and its automorphism group has order equal to the degree.

    source
    @[simp]
    theorem TauCeti.PermutationTriple.isRegular_smul_iff {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) :
    (τ • t).IsRegular ↔ t.IsRegular

    Regularity only depends on the isomorphism class of a triple.

    source
    theorem TauCeti.PermutationTriple.isRegular_iff_of_equivalent {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') :
    t.IsRegular ↔ t'.IsRegular

    Isomorphic triples are regular together.

    The automorphism group of a regular triple #

    source
    noncomputable def TauCeti.PermutationTriple.automorphismGroupMulEquivMonodromyGroupMulOpposite {n : ℕ} {t : PermutationTriple n} (ht : t.IsRegular) (i : Fin n) :
    ↥t.automorphismGroup ≃* (↥t.monodromyGroup)ᵐᵒᵖ

    The automorphism group of a regular triple is isomorphic to the opposite of its monodromy group. Both act simply transitively on the sheets, and an automorphism τ goes to the unique element of the monodromy group moving the base sheet i to τ i (TauCeti.PermutationTriple.unop_automorphismGroupMulEquivMonodromyGroupMulOpposite_smul). The opposite occurs because automorphisms act on the right of the monodromy action.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.PermutationTriple.unop_automorphismGroupMulEquivMonodromyGroupMulOpposite_smul {n : ℕ} {t : PermutationTriple n} (ht : t.IsRegular) (i : Fin n) (τ : ↥t.automorphismGroup) :
      MulOpposite.unop ((automorphismGroupMulEquivMonodromyGroupMulOpposite ht i) τ) • i = τ • i

      The characteristic property of TauCeti.PermutationTriple.automorphismGroupMulEquivMonodromyGroupMulOpposite: the element of the monodromy group that an automorphism τ goes to moves the base sheet i to τ i.