Connected permutation triples and their isomorphism classes

A connected permutation triple is a permutation triple whose monodromy group acts transitively on the sheets, and two connected triples are isomorphic when they are related by a simultaneous relabeling of the sheets. This file introduces the connected triples as a carrier, their isomorphism classes as the quotient by the relabeling action, and the finset of connected triples that make up a class. Since connectedness is decidable, the carrier is a computable Fintype, and since equality of classes reduces to a search through the finitely many relabelings, so is the quotient.

Finally, it introduces connected triples with a marked label modulo the diagonal relabeling action, which moves the label along with the triple. They are the combinatorial invariant of a pointed cover of the thrice-punctured sphere, as isomorphism classes of connected triples are of a cover.

Main definitions

• TauCeti.ConnectedTriple: a permutation triple together with connectedness.
• TauCeti.ConnectedIsoClass: connected triples modulo simultaneous relabeling.
• TauCeti.PermutationTriple.IsoClass.IsConnected: connectedness of an ordinary triple class.
• TauCeti.ConnectedIsoClass.forget: inclusion into the isomorphism classes of all triples.
• TauCeti.ConnectedIsoClass.orbitFinset: the connected triples in a class, as a finset.
• TauCeti.MarkedIsoClass: connected triples with a marked label, modulo the diagonal relabeling action τ • (t, i) = (τ • t, τ i), and TauCeti.MarkedIsoClass.forget, which forgets the label.

Main results

• TauCeti.ConnectedIsoClass.equivSubtype: connected classes are exactly the connected elements of the quotient of all triples, using Mathlib's Equiv.subtypeQuotientEquivQuotientSubtype.
• TauCeti.ConnectedIsoClass.forget_injective: forgetting connectedness preserves distinct classes.
• TauCeti.ConnectedIsoClass.mk_eq_mk_iff_exists_smul, TauCeti.ConnectedIsoClass.mk_eq_mk_iff_equivalent: two connected triples have the same class exactly when a relabeling carries one onto the other, that is, when the underlying permutation triples are isomorphic.
• TauCeti.ConnectedIsoClass.mem_orbitFinset, TauCeti.ConnectedIsoClass.coe_orbitFinset: the finset of a class consists of the connected triples of that class, and is the class's orbit MulAction.orbitRel.Quotient.orbit.
• TauCeti.ConnectedIsoClass.orbitFinset_injective: distinct classes have distinct finsets.
• TauCeti.MarkedIsoClass.mk_eq_mk_iff_exists_smul: two marked connected triples have the same class exactly when a relabeling carries one triple onto the other and its label onto the other label.
• TauCeti.MarkedIsoClass.stabilizerEquiv: fixing a label identifies marked classes with connected triples modulo permutations stabilizing that label.

def TauCeti.PermutationTriple.IsoClass.IsConnected {n : ℕ} : IsoClass n → Prop

Connectedness of any representative of an isomorphism class of triples.

Equations

• TauCeti.PermutationTriple.IsoClass.IsConnected = TauCeti.PermutationTriple.IsoClass.lift TauCeti.PermutationTriple.IsConnected ⋯

@[simp]

theorem TauCeti.PermutationTriple.IsoClass.isConnected_mk {n : ℕ} (t : PermutationTriple n) : (mk t).IsConnected ↔ t.IsConnected

A triple class is connected exactly when its representative is connected.

@[reducible, inline]

abbrev TauCeti.ConnectedTriple (n : ℕ) : Type

A connected permutation triple of degree n.

Equations

• TauCeti.ConnectedTriple n = { t : TauCeti.PermutationTriple n // t.IsConnected }

@[instance_reducible]

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

Relabeling a connected triple simultaneously conjugates its three permutations.

Equations

• TauCeti.ConnectedTriple.instMulActionPermFin = { smul := fun (τ : Equiv.Perm (Fin n)) (t : TauCeti.ConnectedTriple n) => ⟨τ • ↑t, ⋯⟩, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

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

Equations

• TauCeti.ConnectedTriple.instDecidableEq = inferInstance

@[simp]

theorem TauCeti.ConnectedTriple.coe_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : ConnectedTriple n) : ↑(τ • t) = τ • ↑t

def TauCeti.ConnectedIsoClass (n : ℕ) : Type

Isomorphism classes of connected permutation triples of degree n.

Equations

• TauCeti.ConnectedIsoClass n = MulAction.orbitRel.Quotient (Equiv.Perm (Fin n)) (TauCeti.ConnectedTriple n)

def TauCeti.ConnectedIsoClass.mk {n : ℕ} (t : ConnectedTriple n) : ConnectedIsoClass n

The isomorphism class of a connected triple.

Equations

• TauCeti.ConnectedIsoClass.mk t = Quotient.mk'' t

@[simp]

theorem TauCeti.ConnectedIsoClass.mk_eq_mk_iff {n : ℕ} {t t' : ConnectedTriple n} : mk t = mk t' ↔ (MulAction.orbitRel (Equiv.Perm (Fin n)) (ConnectedTriple n)) t t'

Two connected triples determine the same isomorphism class exactly when they are related by simultaneous relabeling.

theorem TauCeti.ConnectedIsoClass.mk_eq_mk_iff_exists_smul {n : ℕ} {t t' : ConnectedTriple n} : mk t = mk t' ↔ ∃ (τ : Equiv.Perm (Fin n)), τ • t' = t

Two connected triples determine the same isomorphism class exactly when some relabeling carries the second onto the first.

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

theorem TauCeti.ConnectedIsoClass.mk_eq_mk_iff_equivalent {n : ℕ} {t t' : ConnectedTriple n} : mk t = mk t' ↔ (↑t).Equivalent ↑t'

Two connected triples determine the same isomorphism class exactly when the underlying permutation triples are isomorphic.

def TauCeti.ConnectedIsoClass.equivSubtype (n : ℕ) : ConnectedIsoClass n ≃ { c : PermutationTriple.IsoClass n // c.IsConnected }

Connected isomorphism classes are exactly the connected elements of the quotient of all permutation triples.

Equations

• TauCeti.ConnectedIsoClass.equivSubtype n = (Equiv.subtypeQuotientEquivQuotientSubtype TauCeti.PermutationTriple.IsConnected TauCeti.PermutationTriple.IsoClass.IsConnected ⋯ ⋯).symm

@[simp]

theorem TauCeti.ConnectedIsoClass.equivSubtype_mk {n : ℕ} (t : ConnectedTriple n) : (equivSubtype n) (mk t) = ⟨PermutationTriple.IsoClass.mk ↑t, ⋯⟩

The connected class of a representative corresponds to its ordinary class together with the induced connectedness proof.

def TauCeti.ConnectedIsoClass.forget {n : ℕ} (c : ConnectedIsoClass n) : PermutationTriple.IsoClass n

The isomorphism class of a connected triple, viewed among all permutation triples.

Equations

• c.forget = ↑((TauCeti.ConnectedIsoClass.equivSubtype n) c)

@[simp]

theorem TauCeti.ConnectedIsoClass.forget_mk {n : ℕ} (t : ConnectedTriple n) : (mk t).forget = PermutationTriple.IsoClass.mk ↑t

Forgetting connectedness sends a connected representative to its ordinary triple class.

@[simp]

theorem TauCeti.ConnectedIsoClass.equivSubtype_symm_mk {n : ℕ} (t : PermutationTriple n) (h : (PermutationTriple.IsoClass.mk t).IsConnected) : (equivSubtype n).symm ⟨PermutationTriple.IsoClass.mk t, h⟩ = mk ⟨t, ⋯⟩

Recovering a connected quotient class from a connected representative of an ordinary class.

theorem TauCeti.ConnectedIsoClass.forget_injective {n : ℕ} : Function.Injective forget

Forgetting connectedness does not identify distinct isomorphism classes.

@[instance_reducible]

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

Equality of isomorphism classes is decidable: on representatives, decide isomorphism of the underlying permutation triples.

Equations

• c.instDecidableEq c' = Quotient.recOnSubsingleton₂ c c' fun (t t' : TauCeti.ConnectedTriple n) => decidable_of_iff ((↑t).Equivalent ↑t') ⋯

@[instance_reducible]

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

Equations

• TauCeti.ConnectedIsoClass.instFintype = Fintype.ofSurjective TauCeti.ConnectedIsoClass.mk ⋯

The connected triples of a class, as a finset

def TauCeti.ConnectedIsoClass.orbitFinset {n : ℕ} (c : ConnectedIsoClass n) : Finset (ConnectedTriple n)

The connected triples in an isomorphism class, as a finset: the relabeling orbit of any representative.

Equations

• c.orbitFinset = Quotient.liftOn' c (fun (t : TauCeti.ConnectedTriple n) => Finset.image (fun (x : Equiv.Perm (Fin n)) => x • t) Finset.univ) ⋯

@[simp]

theorem TauCeti.ConnectedIsoClass.orbitFinset_mk {n : ℕ} (t : ConnectedTriple n) : (mk t).orbitFinset = Finset.image (fun (x : Equiv.Perm (Fin n)) => x • t) Finset.univ

@[simp]

theorem TauCeti.ConnectedIsoClass.mem_orbitFinset {n : ℕ} {t : ConnectedTriple n} {c : ConnectedIsoClass n} : t ∈ c.orbitFinset ↔ mk t = c

A connected triple lies in the finset of a class exactly when the class is its own.

@[simp]

theorem TauCeti.ConnectedIsoClass.coe_orbitFinset {n : ℕ} (c : ConnectedIsoClass n) : ↑c.orbitFinset = MulAction.orbitRel.Quotient.orbit c

The finset of a class is the class's orbit, MulAction.orbitRel.Quotient.orbit.

theorem TauCeti.ConnectedIsoClass.orbitFinset_injective {n : ℕ} : Function.Injective orbitFinset

Distinct isomorphism classes have distinct finsets of connected triples.

def TauCeti.MarkedIsoClass (n : ℕ) : Type

Connected permutation triples of degree n with a marked label, modulo the diagonal relabeling action τ • (t, i) = (τ • t, τ i): the relabeling moves the label along with the triple. Quotienting by the stabilizer of the label instead would never identify pairs with different labels.

Equations

• TauCeti.MarkedIsoClass n = MulAction.orbitRel.Quotient (Equiv.Perm (Fin n)) (TauCeti.ConnectedTriple n × Fin n)

def TauCeti.MarkedIsoClass.mk {n : ℕ} (t : ConnectedTriple n) (i : Fin n) : MarkedIsoClass n

The class of a connected triple with the marked label i.

Equations

• TauCeti.MarkedIsoClass.mk t i = Quotient.mk'' (t, i)

@[simp]

theorem TauCeti.MarkedIsoClass.mk_eq_mk_iff {n : ℕ} {t t' : ConnectedTriple n} {i i' : Fin n} : mk t i = mk t' i' ↔ (MulAction.orbitRel (Equiv.Perm (Fin n)) (ConnectedTriple n × Fin n)) (t, i) (t', i')

Two marked connected triples determine the same class exactly when they are related by the diagonal relabeling action.

theorem TauCeti.MarkedIsoClass.mk_eq_mk_iff_exists_smul {n : ℕ} {t t' : ConnectedTriple n} {i i' : Fin n} : mk t i = mk t' i' ↔ ∃ (τ : Equiv.Perm (Fin n)), τ • t' = t ∧ τ i' = i

Two marked connected triples have the same class exactly when some relabeling carries the second triple onto the first and the second label onto the first.

@[simp]

theorem TauCeti.MarkedIsoClass.mk_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : ConnectedTriple n) (i : Fin n) : mk (τ • t) (τ i) = mk t i

Relabeling a marked triple, label included, does not change its class.

theorem TauCeti.MarkedIsoClass.mk_surjective {n : ℕ} (c : MarkedIsoClass n) : ∃ (t : ConnectedTriple n) (i : Fin n), mk t i = c

def TauCeti.MarkedIsoClass.forget {n : ℕ} : MarkedIsoClass n → ConnectedIsoClass n

Forgetting the marked label of a class.

Equations

• TauCeti.MarkedIsoClass.forget = Quotient.map' Prod.fst ⋯

@[simp]

theorem TauCeti.MarkedIsoClass.forget_mk {n : ℕ} (t : ConnectedTriple n) (i : Fin n) : (mk t i).forget = ConnectedIsoClass.mk t

noncomputable def TauCeti.MarkedIsoClass.stabilizerEquiv {n : ℕ} (i : Fin n) : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer (Equiv.Perm (Fin n)) i)) (ConnectedTriple n) ≃ MarkedIsoClass n

Fixing any label identifies its stabilizer-orbit quotient with marked triple classes. For positive degree, i = 0 gives the fixed-zero-label description.

Equations

• TauCeti.MarkedIsoClass.stabilizerEquiv i = TauCeti.MulAction.orbitRelQuotientStabilizerEquiv i

@[simp]

theorem TauCeti.MarkedIsoClass.stabilizerEquiv_mk {n : ℕ} (i : Fin n) (t : ConnectedTriple n) : (stabilizerEquiv i) (Quotient.mk'' t) = mk t i

The stabilizer orbit of a triple is sent to its class marked at the fixed label.

@[simp]

theorem TauCeti.MarkedIsoClass.stabilizerEquiv_symm_mk {n : ℕ} (i : Fin n) (t : ConnectedTriple n) : (stabilizerEquiv i).symm (mk t i) = Quotient.mk'' t

A class already marked at the fixed label is sent back to the stabilizer orbit of its triple.

@[simp]

theorem TauCeti.MarkedIsoClass.stabilizerEquiv_symm_mk_apply {n : ℕ} (i : Fin n) (t : ConnectedTriple n) (τ : Equiv.Perm (Fin n)) : (stabilizerEquiv i).symm (mk t (τ i)) = Quotient.mk'' (τ⁻¹ • t)

Moving a marked label back to the fixed label also applies the inverse permutation to its triple.