The Euler characteristic of a permutation triple

The surface carrying the cover encoded by a degree-n permutation triple t is glued from n faces, and its cells are counted by the cycles of the three components. Its Euler characteristic is therefore the integer

χ(t) = cycleCount σ0 + cycleCount σ1 + cycleCount σinf − n,

which this file defines as TauCeti.PermutationTriple.eulerChar — combinatorially, without constructing the surface. The cycle counts are TauCeti.orbitCount, so a fixed point of a component contributes a cycle of its own.

Main results

• TauCeti.PermutationTriple.even_eulerChar: the Euler characteristic is even, equivalently 2 ∣ 2 - χ(t). For connected triples, this is the divisibility needed to define the genus.
• TauCeti.PermutationTriple.eulerChar_disjointSum: the Euler characteristic is additive over TauCeti.PermutationTriple.disjointSum, as an Euler characteristic of a disjoint union should be.
• TauCeti.PermutationTriple.eulerChar_le_two_mul_card_monodromyOrbits: the Euler characteristic is at most twice the number of monodromy orbits.
• TauCeti.PermutationTriple.IsConnected.eulerChar_le_two: a connected triple has Euler characteristic at most two, proved combinatorially from transposition factorizations.
• TauCeti.PermutationTriple.genus: the genus derived from the Euler characteristic, with its integer characterizations for connected triples.
• TauCeti.PermutationTriple.eulerChar_smul, TauCeti.PermutationTriple.eulerChar_eq_of_equivalent: it is an invariant of the isomorphism class of a triple, and TauCeti.PermutationTriple.eulerChar_transport says it does not depend on the numbering of the sheets either.
• TauCeti.PermutationTriple.eulerChar_one: the trivial n-sheeted cover has Euler characteristic 2n, the n spheres it consists of contributing 2 each.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, Proposition 1.5.3.

noncomputable def TauCeti.PermutationTriple.eulerChar {n : ℕ} (t : PermutationTriple n) : ℤ

The Euler characteristic of a permutation triple: the total number of cycles of its three components, fixed points included, less the degree. It is the Euler characteristic of the surface obtained by gluing the associated cover, computed from the combinatorics alone.

Equations

• t.eulerChar = ↑(TauCeti.orbitCount t.σ0) + ↑(TauCeti.orbitCount t.σ1) + ↑(TauCeti.orbitCount t.σinf) - ↑n

theorem TauCeti.PermutationTriple.eulerChar_def {n : ℕ} (t : PermutationTriple n) : t.eulerChar = ↑(orbitCount t.σ0) + ↑(orbitCount t.σ1) + ↑(orbitCount t.σinf) - ↑n

theorem TauCeti.PermutationTriple.eulerChar_eq_cycleCounts {n : ℕ} (t : PermutationTriple n) : t.eulerChar = ↑t.cycleCounts.1 + ↑t.cycleCounts.2.1 + ↑t.cycleCounts.2.2 - ↑n

The Euler characteristic, read off the packaged cycle counts of a triple.

Invariance

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).eulerChar = t.eulerChar

Relabeling the sheets does not change the Euler characteristic.

theorem TauCeti.PermutationTriple.eulerChar_eq_of_equivalent {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.eulerChar = t'.eulerChar

Isomorphic triples have the same Euler characteristic.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_transport {m n : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).eulerChar = t.eulerChar

Renumbering the sheets does not change the Euler characteristic.

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_one {n : ℕ} : eulerChar 1 = 2 * ↑n

The trivial n-sheeted cover is a disjoint union of n spheres.

Parity

theorem TauCeti.PermutationTriple.even_eulerChar {n : ℕ} (t : PermutationTriple n) : Even t.eulerChar

The Euler characteristic of a permutation triple is even.

theorem TauCeti.PermutationTriple.two_dvd_two_sub_eulerChar {n : ℕ} (t : PermutationTriple n) : 2 ∣ 2 - t.eulerChar

Two divides 2 - χ for every permutation triple. For connected triples, this is the divisibility needed to define the genus.

The Euler bound and genus

theorem TauCeti.PermutationTriple.eulerChar_le_two_mul_card_monodromyOrbits {n : ℕ} (t : PermutationTriple n) : t.eulerChar ≤ 2 * ↑(Nat.card (MulAction.orbitRel.Quotient (↥t.monodromyGroup) (Fin n)))

The Euler characteristic of a permutation triple is at most twice the number of orbits of its monodromy group. For a connected triple the orbit quotient has one element, recovering TauCeti.PermutationTriple.IsConnected.eulerChar_le_two.

theorem TauCeti.PermutationTriple.IsConnected.eulerChar_le_two {n : ℕ} {t : PermutationTriple n} (ht : t.IsConnected) : t.eulerChar ≤ 2

The Euler characteristic of a connected permutation triple is at most two. This is the combinatorial Euler bound; it is what makes the genus TauCeti.PermutationTriple.genus of a connected triple a genuine natural number.

noncomputable def TauCeti.PermutationTriple.genus {n : ℕ} (t : PermutationTriple n) : ℕ

The genus of a permutation triple, defined by the Euler-characteristic formula. For a connected triple, TauCeti.PermutationTriple.IsConnected.natCast_genus identifies this natural number with the integer quotient (2 - χ) / 2, and TauCeti.PermutationTriple.IsConnected.two_sub_two_mul_genus makes the Int.toNat junk-free.

Connectedness is what gives the number its geometric meaning: the surface of a triple with c monodromy orbits has total genus c - χ / 2, which this formula computes only when c = 1, so on a disconnected triple the truncation returns a junk value and not a genus. Accordingly every statement below that reads the genus geometrically assumes TauCeti.PermutationTriple.IsConnected.

Equations

• t.genus = ((2 - t.eulerChar) / 2).toNat

theorem TauCeti.PermutationTriple.genus_def {n : ℕ} (t : PermutationTriple n) : t.genus = ((2 - t.eulerChar) / 2).toNat

The defining formula for the genus.

@[simp]

theorem TauCeti.PermutationTriple.genus_smul {n : ℕ} (τ : Equiv.Perm (Fin n)) (t : PermutationTriple n) : (τ • t).genus = t.genus

Relabeling the sheets does not change the genus.

theorem TauCeti.PermutationTriple.genus_eq_of_equivalent {n : ℕ} {t t' : PermutationTriple n} (h : t.Equivalent t') : t.genus = t'.genus

Isomorphic permutation triples have the same genus.

@[simp]

theorem TauCeti.PermutationTriple.genus_transport {m n : ℕ} (e : Fin n ≃ Fin m) (t : PermutationTriple n) : ((transport e) t).genus = t.genus

Renumbering the sheets does not change the genus.

theorem TauCeti.PermutationTriple.genus_of_degree_one (t : PermutationTriple 1) : t.genus = 0

A triple of degree one has genus zero.

theorem TauCeti.PermutationTriple.IsConnected.natCast_genus {n : ℕ} {t : PermutationTriple n} (ht : t.IsConnected) : ↑t.genus = (2 - t.eulerChar) / 2

For a connected triple, coercing its genus back to the integers recovers the exact quotient (2 - χ) / 2; the connected Euler bound supplies its nonnegativity.

theorem TauCeti.PermutationTriple.IsConnected.two_sub_two_mul_genus {n : ℕ} {t : PermutationTriple n} (ht : t.IsConnected) : 2 - 2 * ↑t.genus = t.eulerChar

The Euler characteristic of a connected permutation triple is 2 - 2g.

theorem TauCeti.PermutationTriple.IsConnected.natCast_genus_eq_one_add {n : ℕ} {t : PermutationTriple n} (ht : t.IsConnected) : ↑t.genus = 1 + (↑n - ↑(orbitCount t.σ0) - ↑(orbitCount t.σ1) - ↑(orbitCount t.σinf)) / 2

The cycle-count display formula for the genus of a connected permutation triple, written in the integers so that no truncated subtraction occurs.

Disjoint sums

@[simp]

theorem TauCeti.PermutationTriple.eulerChar_disjointSum {m n : ℕ} (s : PermutationTriple m) (t : PermutationTriple n) : (s.disjointSum t).eulerChar = s.eulerChar + t.eulerChar

The Euler characteristic is additive over disjoint sums of triples, the two summands being carried by disjoint sets of sheets.

Worked examples

The monodromy of z ↦ z ^ 3, and a disjoint union of two trivial covers.