Permutation triples

A permutation triple of degree n is a triple (σ0, σ1, σinf) of permutations of Fin n subject to σinf * σ1 * σ0 = 1. Such triples are the combinatorial shadow of a covering of the sphere branched over three points: σ0, σ1 and σinf are the monodromy permutations of the n sheets around the three branch points, and the relation records that the three loops compose to a nullhomotopic loop. They are the three-point case of Lando–Zvonkin's constellations, and the same data as a hypermap or a bipartite ribbon graph.

This file sets up the carrier and the symmetry attached to it.

• TauCeti.PermutationTriple: the carrier, with TauCeti.PermutationTriple.component accessing the component at any of the three branch points, TauCeti.PermutationTriple.ofTwo building a triple from its first two components — the third is determined — and TauCeti.PermutationTriple.equivPair recording that this is a bijection.
• TauCeti.PermutationTriple.equivOppositeConvention: componentwise inversion is a bijection onto the triples of the opposite composition convention σ0 * σ1 * σinf = 1. Sources differ on which of the two relations they impose, and this is the translation between them.
• the simultaneous conjugation MulAction of Equiv.Perm (Fin n): relabeling the n sheets. Two triples are isomorphic when they lie in one orbit, that is, when they are related by MulAction.orbitRel.
• TauCeti.PermutationTriple.monodromyGroup: the subgroup generated by the components. A function on the sheets unchanged by the first two components is unchanged by the whole group (TauCeti.PermutationTriple.apply_eq_of_mem_monodromyGroup).
• TauCeti.PermutationTriple.IsConnected: the monodromy group is transitive on the sheets, and there is at least one sheet. The degree hypothesis is part of the definition, since transitivity is vacuous on Fin 0.
• TauCeti.PermutationTriple.automorphismGroup: the stabilizer of a triple under relabeling, equivalently the centralizer of its monodromy group. For a connected triple it acts freely on the sheets, so its order divides the degree.
• TauCeti.PermutationTriple.mapMonodromy: the image of a triple under a homomorphism from its monodromy group to another symmetric group.

Implementation notes

The relation is imposed in the order σinf * σ1 * σ0 = 1, so that with Mathlib's convention (σ * τ) x = σ (τ x) the monodromy of a composite loop is the product of the monodromies in the same order. The reverse convention is common in the literature and in databases of such triples; TauCeti.PermutationTriple.equivOppositeConvention translates between the two, and Equiv.Perm.cycleType_inv says that the translation preserves cycle types.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.1 and §1.5 (constellations and hypermaps).
• E. Girondo, G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press 2012, §4.

structure TauCeti.PermutationTriple (n : ℕ) : Type

A permutation triple of degree n: three permutations of the n sheets, one for each of the three branch points, whose product in the order σinf * σ1 * σ0 is the identity.

• σ0 : Equiv.Perm (Fin n)

  The monodromy around the first branch point.

• σ1 : Equiv.Perm (Fin n)

  The monodromy around the second branch point.

• σinf : Equiv.Perm (Fin n)

  The monodromy around the third branch point.

• product_eq_one : self.σinf * self.σ1 * self.σ0 = 1

  The three monodromies compose to the identity.

The carrier

def TauCeti.PermutationTriple.component {n : ℕ} (t : PermutationTriple n) : Fin 3 → Equiv.Perm (Fin n)

The component of a permutation triple over the branch point numbered i, where 0, 1, 2 number the branch points 0, 1, ∞.

Equations

• t.component 0 = t.σ0
• t.component 1 = t.σ1
• t.component 2 = t.σinf

@[simp]

theorem TauCeti.PermutationTriple.component_zero {n : ℕ} (t : PermutationTriple n) : t.component 0 = t.σ0

@[simp]

theorem TauCeti.PermutationTriple.component_one {n : ℕ} (t : PermutationTriple n) : t.component 1 = t.σ1

@[simp]

theorem TauCeti.PermutationTriple.component_two {n : ℕ} (t : PermutationTriple n) : t.component 2 = t.σinf

def TauCeti.PermutationTriple.ofTwo {n : ℕ} (σ0 σ1 : Equiv.Perm (Fin n)) : PermutationTriple n

The triple with prescribed first two components, the third being forced.

Equations

• TauCeti.PermutationTriple.ofTwo σ0 σ1 = { σ0 := σ0, σ1 := σ1, σinf := (σ1 * σ0)⁻¹, product_eq_one := ⋯ }

@[simp]

theorem TauCeti.PermutationTriple.ofTwo_σ0 {n : ℕ} (σ0 σ1 : Equiv.Perm (Fin n)) : (ofTwo σ0 σ1).σ0 = σ0

@[simp]

theorem TauCeti.PermutationTriple.ofTwo_σ1 {n : ℕ} (σ0 σ1 : Equiv.Perm (Fin n)) : (ofTwo σ0 σ1).σ1 = σ1

@[simp]

theorem TauCeti.PermutationTriple.ofTwo_σinf {n : ℕ} (σ0 σ1 : Equiv.Perm (Fin n)) : (ofTwo σ0 σ1).σinf = (σ1 * σ0)⁻¹

theorem TauCeti.PermutationTriple.ofTwo_σinf_eq_of_product_eq_one {n : ℕ} (p : Equiv.Perm (Fin n) × Equiv.Perm (Fin n) × Equiv.Perm (Fin n)) (h : p.2.2 * p.2.1 * p.1 = 1) : (ofTwo p.1 p.2.1).σinf = p.2.2

The third component of a triple built from its first two is the third entry of a product-one triple of permutations, the relation determining it.

theorem TauCeti.PermutationTriple.σinf_eq_inv {n : ℕ} (t : PermutationTriple n) : t.σinf = (t.σ1 * t.σ0)⁻¹

The third component of a triple is determined by the first two.

theorem TauCeti.PermutationTriple.σinf_eq_inv_mul_inv {n : ℕ} (t : PermutationTriple n) : t.σinf = t.σ0⁻¹ * t.σ1⁻¹

theorem TauCeti.PermutationTriple.σ1_mul_σ0_eq_σinf_inv {n : ℕ} (t : PermutationTriple n) : t.σ1 * t.σ0 = t.σinf⁻¹

theorem TauCeti.PermutationTriple.σ0_mul_σinf_mul_σ1_eq_one {n : ℕ} (t : PermutationTriple n) : t.σ0 * t.σinf * t.σ1 = 1

The defining relation, rotated: the three components may be cycled, though not permuted arbitrarily.

theorem TauCeti.PermutationTriple.σ1_mul_σ0_mul_σinf_eq_one {n : ℕ} (t : PermutationTriple n) : t.σ1 * t.σ0 * t.σinf = 1

The defining relation, rotated the other way.

theorem TauCeti.PermutationTriple.ext_of_two {n : ℕ} {t t' : PermutationTriple n} (h0 : t.σ0 = t'.σ0) (h1 : t.σ1 = t'.σ1) : t = t'

Two triples agreeing in their first two components are equal: this is the extensionality principle for triples, the third component being determined by the first two.

theorem TauCeti.PermutationTriple.ext_of_two_iff {n : ℕ} {t t' : PermutationTriple n} : t = t' ↔ t.σ0 = t'.σ0 ∧ t.σ1 = t'.σ1

def TauCeti.PermutationTriple.equivPair (n : ℕ) : PermutationTriple n ≃ Equiv.Perm (Fin n) × Equiv.Perm (Fin n)

A permutation triple is the same thing as a pair of permutations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PermutationTriple.equivPair_apply {n : ℕ} (t : PermutationTriple n) : (equivPair n) t = (t.σ0, t.σ1)

@[simp]

theorem TauCeti.PermutationTriple.equivPair_symm_apply {n : ℕ} (p : Equiv.Perm (Fin n) × Equiv.Perm (Fin n)) : (equivPair n).symm p = ofTwo p.1 p.2

def TauCeti.PermutationTriple.transport {n m : ℕ} (e : Fin n ≃ Fin m) : PermutationTriple n ≃ PermutationTriple m

Transport a permutation triple along an equivalence of its sheet labels.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PermutationTriple.transport_apply_σ0 {n m : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).σ0 = e.permCongrHom t.σ0

@[simp]

theorem TauCeti.PermutationTriple.transport_apply_σ1 {n m : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).σ1 = e.permCongrHom t.σ1

@[simp]

theorem TauCeti.PermutationTriple.transport_apply_σinf {n m : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).σinf = e.permCongrHom t.σinf

@[instance_reducible]

instance TauCeti.PermutationTriple.instFintype {n : ℕ} : Fintype (PermutationTriple n)

Equations

• TauCeti.PermutationTriple.instFintype = Fintype.ofEquiv (Equiv.Perm (Fin n) × Equiv.Perm (Fin n)) (TauCeti.PermutationTriple.equivPair n).symm

@[instance_reducible]

instance TauCeti.PermutationTriple.instDecidableEq {n : ℕ} : DecidableEq (PermutationTriple n)

Equations

• TauCeti.PermutationTriple.instDecidableEq = (TauCeti.PermutationTriple.equivPair n).decidableEq

@[instance_reducible]

instance TauCeti.PermutationTriple.instOne {n : ℕ} : One (PermutationTriple n)

The trivial triple, with all three monodromies the identity: the n-sheeted trivial cover.

Equations

• TauCeti.PermutationTriple.instOne = { one := { σ0 := 1, σ1 := 1, σinf := 1, product_eq_one := ⋯ } }

@[simp]

theorem TauCeti.PermutationTriple.one_σ0 {n : ℕ} : σ0 1 = 1

@[simp]

theorem TauCeti.PermutationTriple.one_σ1 {n : ℕ} : σ1 1 = 1

@[simp]

theorem TauCeti.PermutationTriple.one_σinf {n : ℕ} : σinf 1 = 1

@[instance_reducible]

instance TauCeti.PermutationTriple.instInhabited {n : ℕ} : Inhabited (PermutationTriple n)

Equations

• TauCeti.PermutationTriple.instInhabited = { default := 1 }

instance TauCeti.PermutationTriple.instSubsingletonOfFin {n : ℕ} [Subsingleton (Fin n)] : Subsingleton (PermutationTriple n)

In degrees 0 and 1 there is nothing to choose.

def TauCeti.PermutationTriple.equivOppositeConvention (n : ℕ) : PermutationTriple n ≃ { p : Equiv.Perm (Fin n) × Equiv.Perm (Fin n) × Equiv.Perm (Fin n) // p.1 * p.2.1 * p.2.2 = 1 }

Componentwise inversion is a bijection from the triples of this file onto the triples for the opposite composition convention σ0 * σ1 * σinf = 1, which is the one imposed by sources that compose permutations from left to right.

It preserves cycle types componentwise, by Equiv.Perm.cycleType_inv, and it preserves the monodromy group, by TauCeti.PermutationTriple.closure_inv_pair_eq_monodromyGroup; connectedness and the automorphism group are read off the monodromy group, by TauCeti.PermutationTriple.automorphismGroup_eq_centralizer_monodromyGroup, so they are preserved too.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PermutationTriple.equivOppositeConvention_apply_coe {n : ℕ} {t : PermutationTriple n} : ↑((equivOppositeConvention n) t) = (t.σ0⁻¹, t.σ1⁻¹, t.σinf⁻¹)

Relabeling the sheets

@[instance_reducible]

instance TauCeti.PermutationTriple.instSMulPermFin {n : ℕ} : SMul (Equiv.Perm (Fin n)) (PermutationTriple n)

Relabeling the sheets by τ conjugates all three components simultaneously.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PermutationTriple.smul_σ0 {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).σ0 = τ * t.σ0 * τ⁻¹

@[simp]

theorem TauCeti.PermutationTriple.smul_σ1 {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).σ1 = τ * t.σ1 * τ⁻¹

@[simp]

theorem TauCeti.PermutationTriple.smul_σinf {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).σinf = τ * t.σinf * τ⁻¹

@[instance_reducible]

instance TauCeti.PermutationTriple.instMulActionPermFin {n : ℕ} : MulAction (Equiv.Perm (Fin n)) (PermutationTriple n)

Equations

• TauCeti.PermutationTriple.instMulActionPermFin = { toSMul := TauCeti.PermutationTriple.instSMulPermFin, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem TauCeti.PermutationTriple.smul_ofTwo {n : ℕ} (τ σ0 σ1 : Equiv.Perm (Fin n)) : τ • ofTwo σ0 σ1 = ofTwo (τ * σ0 * τ⁻¹) (τ * σ1 * τ⁻¹)

Relabeling commutes with constructing a triple from its first two components.

def TauCeti.PermutationTriple.relabelOppositeConvention {n : ℕ} (τ : Equiv.Perm (Fin n)) (p : { q : Equiv.Perm (Fin n) × Equiv.Perm (Fin n) × Equiv.Perm (Fin n) // q.1 * q.2.1 * q.2.2 = 1 }) : { q : Equiv.Perm (Fin n) × Equiv.Perm (Fin n) × Equiv.Perm (Fin n) // q.1 * q.2.1 * q.2.2 = 1 }

Relabel a triple satisfying the opposite composition convention.

Equations

• TauCeti.PermutationTriple.relabelOppositeConvention τ p = ⟨(τ * (↑p).1 * τ⁻¹, τ * (↑p).2.1 * τ⁻¹, τ * (↑p).2.2 * τ⁻¹), ⋯⟩

@[simp]

theorem TauCeti.PermutationTriple.equivOppositeConvention_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (equivOppositeConvention n) (τ • t) = relabelOppositeConvention τ ((equivOppositeConvention n) t)

The opposite-convention equivalence commutes with relabeling the sheets.

def TauCeti.PermutationTriple.Equivalent {n : ℕ} (t t' : PermutationTriple n) : Prop

Isomorphism of permutation triples is simultaneous conjugacy.

Equations

• t.Equivalent t' = (MulAction.orbitRel (Equiv.Perm (Fin n)) (TauCeti.PermutationTriple n)) t t'

theorem TauCeti.PermutationTriple.equivalent_iff_exists_smul_eq {n : ℕ} {t t' : PermutationTriple n} : t.Equivalent t' ↔ ∃ (τ : Equiv.Perm (Fin n)), τ • t = t'

Two permutation triples are isomorphic exactly when one is obtained from the other by a simultaneous relabeling.

theorem TauCeti.PermutationTriple.equivalent_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).Equivalent t

Every relabeling of a permutation triple is isomorphic to it.

@[instance_reducible]

instance TauCeti.PermutationTriple.instDecidableRelEquivalent {n : ℕ} : DecidableRel Equivalent

Isomorphism of triples — relabeling the sheets — is decidable, by searching the finitely many relabelings.

Equations

• t.instDecidableRelEquivalent t' = decidable_of_iff (∃ (τ : Equiv.Perm (Fin n)), τ • t' = t) ⋯

def TauCeti.PermutationTriple.IsoClass (n : ℕ) : Type

Isomorphism classes of degree-n permutation triples.

Equations

• TauCeti.PermutationTriple.IsoClass n = MulAction.orbitRel.Quotient (Equiv.Perm (Fin n)) (TauCeti.PermutationTriple n)

def TauCeti.PermutationTriple.IsoClass.mk {n : ℕ} (t : PermutationTriple n) : IsoClass n

The isomorphism class of a permutation triple.

Equations

• TauCeti.PermutationTriple.IsoClass.mk t = Quotient.mk'' t

@[simp]

theorem TauCeti.PermutationTriple.IsoClass.quotient_mk {n : ℕ} (t : PermutationTriple n) : ⟦t⟧ = mk t

The quotient constructor gives the isomorphism class of its representative.

@[simp]

theorem TauCeti.PermutationTriple.IsoClass.mk_eq_mk_iff {n : ℕ} {t t' : PermutationTriple n} : mk t = mk t' ↔ t.Equivalent t'

Two triples determine the same isomorphism class exactly when they are isomorphic.

theorem TauCeti.PermutationTriple.IsoClass.mk_surjective {n : ℕ} : Function.Surjective mk

Every isomorphism class is the class of some triple.

def TauCeti.PermutationTriple.IsoClass.lift {n : ℕ} {α : Sort u_1} (f : PermutationTriple n → α) (hf : ∀ (t t' : PermutationTriple n), t.Equivalent t' → f t = f t') : IsoClass n → α

A function on triples that is constant on isomorphism classes, as a function on classes.

Equations

• TauCeti.PermutationTriple.IsoClass.lift f hf = Quotient.lift f hf

@[simp]

theorem TauCeti.PermutationTriple.IsoClass.lift_mk {n : ℕ} {α : Sort u_1} (f : PermutationTriple n → α) (hf : ∀ (t t' : PermutationTriple n), t.Equivalent t' → f t = f t') (t : PermutationTriple n) : lift f hf (mk t) = f t

The monodromy group

def TauCeti.PermutationTriple.monodromyGroup {n : ℕ} (t : PermutationTriple n) : Subgroup (Equiv.Perm (Fin n))

The monodromy group of a triple: the subgroup of permutations of the sheets generated by the components. The third component is redundant, by TauCeti.PermutationTriple.closure_triple_eq_monodromyGroup.

Equations

• t.monodromyGroup = Subgroup.closure {t.σ0, t.σ1}

@[simp]

theorem TauCeti.PermutationTriple.σ0_mem_monodromyGroup {n : ℕ} (t : PermutationTriple n) : t.σ0 ∈ t.monodromyGroup

@[simp]

theorem TauCeti.PermutationTriple.σ1_mem_monodromyGroup {n : ℕ} (t : PermutationTriple n) : t.σ1 ∈ t.monodromyGroup

@[simp]

theorem TauCeti.PermutationTriple.σinf_mem_monodromyGroup {n : ℕ} (t : PermutationTriple n) : t.σinf ∈ t.monodromyGroup

theorem TauCeti.PermutationTriple.closure_pair_eq_monodromyGroup {n : ℕ} (t : PermutationTriple n) : Subgroup.closure {t.σ0, t.σ1} = t.monodromyGroup

The monodromy group of a triple is the subgroup generated by its first two components.

theorem TauCeti.PermutationTriple.apply_eq_of_mem_monodromyGroup {n : ℕ} (t : PermutationTriple n) {β : Type u_1} {f : Fin n → β} (h0 : ∀ (x : Fin n), f (t.σ0 x) = f x) (h1 : ∀ (x : Fin n), f (t.σ1 x) = f x) {g : Equiv.Perm (Fin n)} (hg : g ∈ t.monodromyGroup) (x : Fin n) : f (g x) = f x

A function on the sheets taking the same value at x, t.σ0 x and t.σ1 x for every sheet x is constant along the whole monodromy group, so it factors through the monodromy orbits.

theorem TauCeti.PermutationTriple.monodromyGroup_ofTwo_map {n : ℕ} {G : Type u_1} [Group G] (ρ : G →* Equiv.Perm (Fin n)) (g₀ g₁ : G) : (ofTwo (ρ g₀) (ρ g₁)).monodromyGroup = Subgroup.map ρ (Subgroup.closure {g₀, g₁})

The monodromy group of a triple built from the images of two group elements is the image of the subgroup they generate.

theorem TauCeti.PermutationTriple.closure_triple_eq_monodromyGroup {n : ℕ} (t : PermutationTriple n) : Subgroup.closure {t.σ0, t.σ1, t.σinf} = t.monodromyGroup

The subgroup generated by all three components equals the monodromy group.

theorem TauCeti.PermutationTriple.closure_inv_pair_eq_monodromyGroup {n : ℕ} {t : PermutationTriple n} : Subgroup.closure {t.σ0⁻¹, t.σ1⁻¹} = t.monodromyGroup

The two generators may be replaced by their inverses: this is the invariance of the monodromy group under the translation TauCeti.PermutationTriple.equivOppositeConvention of conventions.

theorem TauCeti.PermutationTriple.monodromyGroup_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).monodromyGroup = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) t.monodromyGroup

Relabeling the sheets conjugates the monodromy group. In particular isomorphic triples have conjugate monodromy groups.

theorem TauCeti.PermutationTriple.mem_normalizer_iff_monodromyGroup_smul_eq {n : ℕ} {t : PermutationTriple n} {τ : Equiv.Perm (Fin n)} : τ ∈ Subgroup.normalizer ↑t.monodromyGroup ↔ (τ • t).monodromyGroup = t.monodromyGroup

A relabeling normalizes the monodromy group of a triple exactly when it leaves that monodromy group unchanged.

Connectedness and automorphisms

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

A triple is connected when it has at least one sheet and its monodromy group is transitive on the sheets — the combinatorial form of connectedness of the associated cover. The degree hypothesis is not redundant: transitivity holds vacuously on Fin 0.

Equations

• t.IsConnected = (n ≠ 0 ∧ MulAction.IsPretransitive (↥t.monodromyGroup) (Fin n))

theorem TauCeti.PermutationTriple.isConnected_iff {n : ℕ} {t : PermutationTriple n} : t.IsConnected ↔ n ≠ 0 ∧ MulAction.IsPretransitive (↥t.monodromyGroup) (Fin n)

theorem TauCeti.PermutationTriple.IsConnected.ne_zero {n : ℕ} {t : PermutationTriple n} (ht : t.IsConnected) : n ≠ 0

theorem TauCeti.PermutationTriple.IsConnected.isPretransitive {n : ℕ} {t : PermutationTriple n} (ht : t.IsConnected) : MulAction.IsPretransitive (↥t.monodromyGroup) (Fin n)

@[simp]

theorem TauCeti.PermutationTriple.isConnected_smul_iff {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).IsConnected ↔ t.IsConnected

Connectedness only depends on the isomorphism class of a triple.

@[simp]

theorem TauCeti.PermutationTriple.monodromyGroup_one {n : ℕ} : monodromyGroup 1 = ⊥

The trivial triple has trivial monodromy.

@[simp]

theorem TauCeti.PermutationTriple.isConnected_one_iff {n : ℕ} : IsConnected 1 ↔ n = 1

The trivial triple is the disjoint union of n unbranched sheets, so it is connected exactly in degree one.

theorem TauCeti.PermutationTriple.isConnected_of_degree_one (t : PermutationTriple 1) : t.IsConnected

A triple of degree one is connected.

theorem TauCeti.PermutationTriple.isConnected_equivOppositeConvention_iff {n : ℕ} (t : PermutationTriple n) : n ≠ 0 ∧ MulAction.IsPretransitive (↥(Subgroup.closure {(↑((equivOppositeConvention n) t)).1, (↑((equivOppositeConvention n) t)).2.1})) (Fin n) ↔ t.IsConnected

Translating to the opposite convention preserves connectedness.

def TauCeti.PermutationTriple.automorphismGroup {n : ℕ} (t : PermutationTriple n) : Subgroup (Equiv.Perm (Fin n))

The automorphism group of a triple: the deck transformations of the associated cover, that is, the relabelings that fix the triple.

Equations

• t.automorphismGroup = MulAction.stabilizer (Equiv.Perm (Fin n)) t

theorem TauCeti.PermutationTriple.mem_automorphismGroup_iff {n : ℕ} {t : PermutationTriple n} {τ : Equiv.Perm (Fin n)} : τ ∈ t.automorphismGroup ↔ τ * t.σ0 * τ⁻¹ = t.σ0 ∧ τ * t.σ1 * τ⁻¹ = t.σ1

theorem TauCeti.PermutationTriple.automorphismGroup_eq_centralizer {n : ℕ} {t : PermutationTriple n} : t.automorphismGroup = Subgroup.centralizer {t.σ0, t.σ1}

The automorphism group is the simultaneous centralizer of the two generating components.

theorem TauCeti.PermutationTriple.automorphismGroup_eq_centralizer_monodromyGroup {n : ℕ} {t : PermutationTriple n} : t.automorphismGroup = Subgroup.centralizer ↑t.monodromyGroup

The automorphism group is the centralizer of the monodromy group. Together with TauCeti.PermutationTriple.isConnected_iff this says that a triple enters both notions only through its monodromy group.

@[simp]

theorem TauCeti.PermutationTriple.stabilizer_normalizer_eq_centralizer_subgroupOf {n : ℕ} {t : PermutationTriple n} : MulAction.stabilizer (↥(Subgroup.normalizer ↑t.monodromyGroup)) t = (Subgroup.centralizer ↑t.monodromyGroup).subgroupOf (Subgroup.normalizer ↑t.monodromyGroup)

The stabilizer of a triple under the normalizer of its monodromy group is the centralizer of that group, regarded as a subgroup of the normalizer.

theorem TauCeti.PermutationTriple.automorphismGroup_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).automorphismGroup = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) t.automorphismGroup

Relabeling the sheets conjugates the automorphism group.

theorem TauCeti.PermutationTriple.automorphismGroup_equivOppositeConvention {n : ℕ} (t : PermutationTriple n) : Subgroup.centralizer {(↑((equivOppositeConvention n) t)).1, (↑((equivOppositeConvention n) t)).2.1} = t.automorphismGroup

Translating to the opposite convention preserves the automorphism group, represented on the opposite side as the simultaneous centralizer of its first two components.

theorem TauCeti.PermutationTriple.eq_one_of_mem_automorphismGroup_of_apply_eq {n : ℕ} {t : PermutationTriple n} (ht : MulAction.IsPretransitive (↥t.monodromyGroup) (Fin n)) {τ : Equiv.Perm (Fin n)} (hτ : τ ∈ t.automorphismGroup) {i : Fin n} (hi : τ i = i) : τ = 1

An automorphism of a triple with pretransitive monodromy fixing a sheet is the identity.

theorem TauCeti.PermutationTriple.card_automorphismGroup_dvd {n : ℕ} {t : PermutationTriple n} (ht : MulAction.IsPretransitive (↥t.monodromyGroup) (Fin n)) : Nat.card ↥t.automorphismGroup ∣ n

The order of the automorphism group divides the degree when the monodromy action is pretransitive.

Images under representations of the monodromy group

def TauCeti.PermutationTriple.mapMonodromy {n m : ℕ} (t : PermutationTriple n) (f : ↥t.monodromyGroup →* Equiv.Perm (Fin m)) : PermutationTriple m

The image of a triple under a homomorphism from its monodromy group to the permutations of another set of sheets: the three components are sent to their images, and the relation σinf * σ1 * σ0 = 1 is preserved because f is multiplicative. Restricting a triple to a monodromy orbit and passing to its action on a system of blocks are both of this form.

Equations

• t.mapMonodromy f = { σ0 := f ⟨t.σ0, ⋯⟩, σ1 := f ⟨t.σ1, ⋯⟩, σinf := f ⟨t.σinf, ⋯⟩, product_eq_one := ⋯ }

@[simp]

theorem TauCeti.PermutationTriple.mapMonodromy_σ0 {n m : ℕ} (t : PermutationTriple n) (f : ↥t.monodromyGroup →* Equiv.Perm (Fin m)) : (t.mapMonodromy f).σ0 = f ⟨t.σ0, ⋯⟩

@[simp]

theorem TauCeti.PermutationTriple.mapMonodromy_σ1 {n m : ℕ} (t : PermutationTriple n) (f : ↥t.monodromyGroup →* Equiv.Perm (Fin m)) : (t.mapMonodromy f).σ1 = f ⟨t.σ1, ⋯⟩

@[simp]

theorem TauCeti.PermutationTriple.mapMonodromy_σinf {n m : ℕ} (t : PermutationTriple n) (f : ↥t.monodromyGroup →* Equiv.Perm (Fin m)) : (t.mapMonodromy f).σinf = f ⟨t.σinf, ⋯⟩

@[simp]

theorem TauCeti.PermutationTriple.mapMonodromy_subtype {n : ℕ} (t : PermutationTriple n) : t.mapMonodromy t.monodromyGroup.subtype = t

The image of a triple under the inclusion of its monodromy group is the triple itself.

theorem TauCeti.PermutationTriple.mapMonodromy_conj_comp {n m : ℕ} (t : PermutationTriple n) (f : ↥t.monodromyGroup →* Equiv.Perm (Fin m)) (τ : Equiv.Perm (Fin m)) : t.mapMonodromy ((MulEquiv.toMonoidHom (MulAut.conj τ)).comp f) = τ • t.mapMonodromy f

Composing the representation with conjugation by τ relabels the image triple by τ.

theorem TauCeti.PermutationTriple.monodromyGroup_mapMonodromy {n m : ℕ} (t : PermutationTriple n) (f : ↥t.monodromyGroup →* Equiv.Perm (Fin m)) : (t.mapMonodromy f).monodromyGroup = f.range

The monodromy group of the image triple is the image of the representation.

theorem TauCeti.PermutationTriple.isConnected_mapMonodromy_iff {n m : ℕ} (t : PermutationTriple n) (f : ↥t.monodromyGroup →* Equiv.Perm (Fin m)) : (t.mapMonodromy f).IsConnected ↔ m ≠ 0 ∧ MulAction.IsPretransitive (↥f.range) (Fin m)

The image triple is connected exactly when it has a sheet and the image of the representation is transitive on its sheets.