Numbered, pointed and bare connected covers of degree n

A connected cover of degree n over a basepoint x can be rigidified in three ways, and each rigidification has its own notion of isomorphism:

• a fibre-numbered cover TauCeti.ConnectedFiberNumberedCover x n carries a numbering ν : p ⁻¹' {x} ≃ Fin n of the fibre, and its isomorphisms preserve the label of every point of the fibre;
• a pointed cover TauCeti.ConnectedPointedCover x n carries one point of the fibre, and its isomorphisms preserve that point;
• a bare cover TauCeti.ConnectedCover x n carries neither, and its isomorphisms are all isomorphisms of covers.

All three are built on TauCeti.ConnectedCoveringSpace X. The degree is a parameter rather than something recovered afterwards: it is the cardinality of the fibre over x, recorded by the numbering itself or by the existence of one. Isomorphism is an equivalence relation in each case, and the three types of isomorphism classes are the quotients TauCeti.ConnectedFiberNumberedCoverClass, TauCeti.ConnectedPointedCoverClass and TauCeti.ConnectedCoverClass.

The rigidifications are related by forgetful maps — forgetting the numbering, keeping only the point with a given label, forgetting the point — which descend to isomorphism classes and form a commuting triangle. The symmetric group Equiv.Perm (Fin n) acts on numberings by relabelling, τ • ν = ν.trans τ. The forgetful maps have these orbit descriptions:

• two numbered classes have the same underlying cover exactly when they differ by a relabelling, so the bare classes are the relabelling orbits of the numbered ones (TauCeti.ConnectedFiberNumberedCoverClass.orbitRelQuotientEquiv);
• two marked numbered classes give the same pointed class exactly when a relabelling carries one to the other and carries its marked label to the other label, so the pointed classes are the orbits of the diagonal action on numbered classes paired with a label (TauCeti.ConnectedFiberNumberedCoverClass.markedOrbitRelQuotientEquiv).

These are the covering-space counterparts of the passage from literal permutation triples to their simultaneous-conjugacy classes (TauCeti.ConnectedIsoClass) and to marked triples modulo the diagonal action: a classification of numbered covers that is equivariant for relabelling therefore descends to the other two rigidifications.

Over a path-connected base the degree does not depend on the basepoint, and over a preconnected base a connected cover has positive degree.

The basepoint can be moved. A bare cover at x₀ is a bare cover at any point of the connected component of x₀, with no choice involved. A numbered cover is moved along a path γ from x₀ to x₁: lifting γ identifies the two fibres, so the numbering of the fibre over x₀ induces one of the fibre over x₁, and the numbered monodromy of π₁(X, x₁) is that of π₁(X, x₀) read through the change of basepoint along γ.

Over a path-connected, locally path-connected base, a numbered cover is determined up to isomorphism by its monodromy representation read through the numbering, π₁(X, x) →* Equiv.Perm (Fin n): taking the fibre over x with its monodromy action is faithful and full (TauCeti.CoveringSpace.fiberActionFunctor_faithful, TauCeti.CoveringSpace.fiberActionFunctor_full), and the numberings turn equal representations into an isomorphism of π₁(X, x)-sets preserving the labels.

Conversely, over a locally path-connected, semilocally simply connected base, every representation π₁(X, x) →* Equiv.Perm (Fin n) with n ≠ 0 and transitive image is the numbered monodromy of some numbered cover: the realisation theorem for transitive fundamental-group sets (TauCeti.ConnectedCoveringSpace.exists_fiberAction_iso) supplies a connected cover whose fibre is equivariantly identified with the finite set, and that identification is a numbering.

A deck transformation of a numbered cover permutes the fibre, hence the labels (TauCeti.ConnectedFiberNumberedCover.deckPerm). Over a preconnected base this determines the deck transformation, and over a path-connected, locally path-connected base the permutations so obtained are exactly those commuting with the numbered monodromy: a permutation τ commuting with it leaves the numbered monodromy of the relabelled cover unchanged, so some isomorphism from the cover to its relabelling preserves every label, and that isomorphism is a deck transformation inducing τ. Relabelling the fibre conjugates the induced permutations.

Main declarations

• TauCeti.ConnectedFiberNumberedCover, TauCeti.ConnectedPointedCover, TauCeti.ConnectedCover: the three carriers.
• TauCeti.ConnectedFiberNumberedCoverIso, TauCeti.ConnectedPointedCoverIso: the isomorphism relations of numbered and pointed covers, with setoids TauCeti.connectedFiberNumberedCoverSetoid and TauCeti.connectedPointedCoverSetoid. Bare covers are related by CategoryTheory.IsIsomorphic of their underlying covers, with setoid TauCeti.connectedCoverSetoid.
• TauCeti.ConnectedFiberNumberedCoverClass, TauCeti.ConnectedPointedCoverClass, TauCeti.ConnectedCoverClass: the types of isomorphism classes.
• forgetNumbering, markLabel, forgetPoint: the forgetful maps, on carriers and on classes, with TauCeti.ConnectedFiberNumberedCoverClass.forgetPoint_markLabel.
• TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering_eq_forgetNumbering_iff and TauCeti.ConnectedFiberNumberedCoverClass.orbitRelQuotientEquiv: bare classes are relabelling orbits of numbered classes.
• TauCeti.ConnectedFiberNumberedCoverClass.markLabel_eq_markLabel_iff and TauCeti.ConnectedFiberNumberedCoverClass.markedOrbitRelQuotientEquiv: pointed classes are diagonal orbits of marked numbered classes.
• TauCeti.ConnectedCover.nonempty_equiv_fin_of_mem_connectedComponent: the degree is the same over the whole connected component of the base point; TauCeti.ConnectedCover.ne_zero: over a preconnected base the degree is positive.
• TauCeti.ConnectedFiberNumberedCover.basepointChange, TauCeti.ConnectedCover.basepointChange, TauCeti.ConnectedCoverClass.basepointChange: moving the basepoint, with TauCeti.ConnectedFiberNumberedCover.permCongrHom_comp_monodromyPerm_basepointChange computing the numbered monodromy of the moved cover.
• TauCeti.connectedFiberNumberedCoverIso_iff_permCongrHom_comp_monodromyPerm_eq: two numbered covers are isomorphic exactly when their numbered monodromy representations agree.
• TauCeti.ConnectedFiberNumberedCover.exists_permCongrHom_comp_monodromyPerm_eq: over a semilocally simply connected base, every transitive representation on Fin n is the numbered monodromy of some numbered cover.
• TauCeti.ConnectedFiberNumberedCover.deckPerm: the permutation of the labels induced by a deck transformation, with deckPerm_injective and deckPerm_smul.
• TauCeti.ConnectedFiberNumberedCover.range_deckPerm: the induced permutations are exactly those commuting with the numbered monodromy.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, §1.3 (isomorphism of covering spaces, the change of basepoint within a fibre, and deck transformations).
• E. Girondo and G. González-Diez, Introduction to Compact Riemann Surfaces and Dessins d'Enfants, London Mathematical Society Student Texts 79, Cambridge University Press, 2012, §2.7 (the monodromy of a cover is well defined up to the numbering of the fibre).

The three carriers

structure TauCeti.ConnectedFiberNumberedCover {X : TopCat} (x : ↑X) (n : ℕ) : Type (u + 1)

A connected covering space of X of degree n, with its fibre over x numbered by Fin n. This is the rigidification at which the monodromy of the cover is a literal action of π₁(X, x) on Fin n, rather than an action up to relabelling.

• cover : ConnectedCoveringSpace X

  The underlying connected covering space.

• ν : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj self.cover)) ⁻¹' {x}) ≃ Fin n

  The numbering of the fibre over the basepoint.

structure TauCeti.ConnectedPointedCover {X : TopCat} (x : ↑X) (n : ℕ) : Type (u + 1)

A connected covering space of X of degree n with one chosen point of its fibre over x. Only that point is rigidified: the relabellings of the fibre fixing it survive.

• cover : ConnectedCoveringSpace X

  The underlying connected covering space.

• e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj self.cover)) ⁻¹' {x})

  The chosen point of the fibre over the basepoint.

• nonempty_equiv_fin : Nonempty (↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj self.cover)) ⁻¹' {x}) ≃ Fin n)

  The fibre over the basepoint has n points.

structure TauCeti.ConnectedCover {X : TopCat} (x : ↑X) (n : ℕ) : Type (u + 1)

A connected covering space of X whose fibre over x has n points, with no further rigidification. Two such covers are equal exactly when their underlying covers are (TauCeti.ConnectedCover.ext).

• cover : ConnectedCoveringSpace X

  The underlying connected covering space.

• nonempty_equiv_fin : Nonempty (↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj self.cover)) ⁻¹' {x}) ≃ Fin n)

  The fibre over the basepoint has n points.

theorem TauCeti.ConnectedCover.ext_iff {X : TopCat} {x : ↑X} {n : ℕ} {x✝ y : ConnectedCover x n} : x✝ = y ↔ x✝.cover = y.cover

theorem TauCeti.ConnectedCover.ext {X : TopCat} {x : ↑X} {n : ℕ} {x✝ y : ConnectedCover x n} (cover : x✝.cover = y.cover) : x✝ = y

Isomorphisms

def TauCeti.ConnectedFiberNumberedCoverIso {X : TopCat} {x : ↑X} {n : ℕ} (c c' : ConnectedFiberNumberedCover x n) : Prop

Two fibre-numbered covers are isomorphic when some isomorphism of the underlying covers carries the point labelled i to the point labelled i, for every label i.

Equations

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

def TauCeti.ConnectedPointedCoverIso {X : TopCat} {x : ↑X} {n : ℕ} (c c' : ConnectedPointedCover x n) : Prop

Two pointed covers are isomorphic when some isomorphism of the underlying covers carries the chosen point to the chosen point.

Equations

• TauCeti.ConnectedPointedCoverIso c c' = ∃ (f : c.cover ≅ c'.cover), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left f.hom.hom)) ↑c.e = ↑c'.e

theorem TauCeti.connectedFiberNumberedCoverIso_def {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedFiberNumberedCover x n} : ConnectedFiberNumberedCoverIso c c' ↔ ∃ (f : c.cover ≅ c'.cover), ∀ (i : Fin n), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left f.hom.hom)) ↑(c.ν.symm i) = ↑(c'.ν.symm i)

A numbered isomorphism consists of a cover isomorphism preserving every fibre label.

theorem TauCeti.connectedPointedCoverIso_def {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedPointedCover x n} : ConnectedPointedCoverIso c c' ↔ ∃ (f : c.cover ≅ c'.cover), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left f.hom.hom)) ↑c.e = ↑c'.e

A pointed isomorphism consists of a cover isomorphism preserving the chosen point.

theorem TauCeti.ConnectedFiberNumberedCoverIso.refl {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) : ConnectedFiberNumberedCoverIso c c

Every fibre-numbered cover is isomorphic to itself, by the identity.

theorem TauCeti.ConnectedFiberNumberedCoverIso.symm {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedFiberNumberedCover x n} (h : ConnectedFiberNumberedCoverIso c c') : ConnectedFiberNumberedCoverIso c' c

Label-preserving isomorphism of fibre-numbered covers is symmetric.

theorem TauCeti.ConnectedFiberNumberedCoverIso.trans {X : TopCat} {x : ↑X} {n : ℕ} {c c' c'' : ConnectedFiberNumberedCover x n} (h : ConnectedFiberNumberedCoverIso c c') (h' : ConnectedFiberNumberedCoverIso c' c'') : ConnectedFiberNumberedCoverIso c c''

Label-preserving isomorphism of fibre-numbered covers is transitive.

theorem TauCeti.ConnectedPointedCoverIso.refl {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedPointedCover x n) : ConnectedPointedCoverIso c c

Every pointed cover is isomorphic to itself, by the identity.

theorem TauCeti.ConnectedPointedCoverIso.symm {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedPointedCover x n} (h : ConnectedPointedCoverIso c c') : ConnectedPointedCoverIso c' c

Isomorphism of pointed covers is symmetric.

theorem TauCeti.ConnectedPointedCoverIso.trans {X : TopCat} {x : ↑X} {n : ℕ} {c c' c'' : ConnectedPointedCover x n} (h : ConnectedPointedCoverIso c c') (h' : ConnectedPointedCoverIso c' c'') : ConnectedPointedCoverIso c c''

Isomorphism of pointed covers is transitive.

@[instance_reducible]

instance TauCeti.connectedFiberNumberedCoverSetoid {X : TopCat} (x : ↑X) (n : ℕ) : Setoid (ConnectedFiberNumberedCover x n)

Fibre-numbered covers related by label-preserving isomorphism.

Equations

• TauCeti.connectedFiberNumberedCoverSetoid x n = { r := TauCeti.ConnectedFiberNumberedCoverIso, iseqv := ⋯ }

@[instance_reducible]

instance TauCeti.connectedPointedCoverSetoid {X : TopCat} (x : ↑X) (n : ℕ) : Setoid (ConnectedPointedCover x n)

Pointed covers related by pointed isomorphism.

Equations

• TauCeti.connectedPointedCoverSetoid x n = { r := TauCeti.ConnectedPointedCoverIso, iseqv := ⋯ }

@[instance_reducible]

instance TauCeti.connectedCoverSetoid {X : TopCat} (x : ↑X) (n : ℕ) : Setoid (ConnectedCover x n)

Covers related by isomorphism of the underlying covers.

Equations

• TauCeti.connectedCoverSetoid x n = Setoid.comap TauCeti.ConnectedCover.cover (CategoryTheory.isIsomorphicSetoid (TauCeti.ConnectedCoveringSpace X))

Isomorphism classes

def TauCeti.ConnectedFiberNumberedCoverClass {X : TopCat} (x : ↑X) (n : ℕ) : Type (u + 1)

Fibre-numbered connected covers of degree n up to label-preserving isomorphism.

Equations

• TauCeti.ConnectedFiberNumberedCoverClass x n = Quotient (TauCeti.connectedFiberNumberedCoverSetoid x n)

def TauCeti.ConnectedPointedCoverClass {X : TopCat} (x : ↑X) (n : ℕ) : Type (u + 1)

Pointed connected covers of degree n up to pointed isomorphism.

Equations

• TauCeti.ConnectedPointedCoverClass x n = Quotient (TauCeti.connectedPointedCoverSetoid x n)

def TauCeti.ConnectedCoverClass {X : TopCat} (x : ↑X) (n : ℕ) : Type (u + 1)

Connected covers of degree n up to isomorphism.

Equations

• TauCeti.ConnectedCoverClass x n = Quotient (TauCeti.connectedCoverSetoid x n)

def TauCeti.ConnectedFiberNumberedCoverClass.mk {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) : ConnectedFiberNumberedCoverClass x n

The isomorphism class of a fibre-numbered cover.

Equations

• TauCeti.ConnectedFiberNumberedCoverClass.mk c = ⟦c⟧

def TauCeti.ConnectedPointedCoverClass.mk {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedPointedCover x n) : ConnectedPointedCoverClass x n

The isomorphism class of a pointed cover.

Equations

• TauCeti.ConnectedPointedCoverClass.mk c = ⟦c⟧

def TauCeti.ConnectedCoverClass.mk {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedCover x n) : ConnectedCoverClass x n

The isomorphism class of a cover.

Equations

• TauCeti.ConnectedCoverClass.mk c = ⟦c⟧

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.mk_eq_mk_iff {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedFiberNumberedCover x n} : mk c = mk c' ↔ ConnectedFiberNumberedCoverIso c c'

Two fibre-numbered covers have the same class exactly when they are isomorphic by a label-preserving isomorphism.

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.mk_eq_mk_iff {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedPointedCover x n} : mk c = mk c' ↔ ConnectedPointedCoverIso c c'

Two pointed covers have the same class exactly when they are isomorphic as pointed covers.

@[simp]

theorem TauCeti.ConnectedCoverClass.mk_eq_mk_iff {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedCover x n} : mk c = mk c' ↔ CategoryTheory.IsIsomorphic c.cover c'.cover

Two covers have the same class exactly when their underlying covers are isomorphic.

theorem TauCeti.ConnectedFiberNumberedCoverClass.mk_surjective {X : TopCat} {x : ↑X} {n : ℕ} : Function.Surjective mk

Every class of fibre-numbered covers is the class of a fibre-numbered cover.

def TauCeti.ConnectedFiberNumberedCoverClass.lift {X : TopCat} {x : ↑X} {n : ℕ} {α : Sort u_1} (f : ConnectedFiberNumberedCover x n → α) (hf : ∀ (c c' : ConnectedFiberNumberedCover x n), ConnectedFiberNumberedCoverIso c c' → f c = f c') : ConnectedFiberNumberedCoverClass x n → α

A function on numbered covers that is constant on label-preserving isomorphism classes, as a function on the classes.

Equations

• TauCeti.ConnectedFiberNumberedCoverClass.lift f hf = Quotient.lift f hf

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.lift_mk {X : TopCat} {x : ↑X} {n : ℕ} {α : Sort u_1} (f : ConnectedFiberNumberedCover x n → α) (hf : ∀ (c c' : ConnectedFiberNumberedCover x n), ConnectedFiberNumberedCoverIso c c' → f c = f c') (c : ConnectedFiberNumberedCover x n) : lift f hf (mk c) = f c

The lift of f takes the class of c to f c.

theorem TauCeti.ConnectedFiberNumberedCoverClass.ind {X : TopCat} {x : ↑X} {n : ℕ} {motive : ConnectedFiberNumberedCoverClass x n → Prop} (h : ∀ (c : ConnectedFiberNumberedCover x n), motive (mk c)) (C : ConnectedFiberNumberedCoverClass x n) : motive C

A property of the classes holds for every class once it holds for the class of every numbered cover.

theorem TauCeti.ConnectedPointedCoverClass.mk_surjective {X : TopCat} {x : ↑X} {n : ℕ} : Function.Surjective mk

Every class of pointed covers is the class of a pointed cover.

theorem TauCeti.ConnectedCoverClass.mk_surjective {X : TopCat} {x : ↑X} {n : ℕ} : Function.Surjective mk

Every class of covers is the class of a cover.

The forgetful maps

def TauCeti.ConnectedFiberNumberedCover.forgetNumbering {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) : ConnectedCover x n

Forgetting the numbering of the fibre.

Equations

• c.forgetNumbering = { cover := c.cover, nonempty_equiv_fin := ⋯ }

def TauCeti.ConnectedFiberNumberedCover.markLabel {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) (i : Fin n) : ConnectedPointedCover x n

Keeping only the point labelled i.

Equations

• c.markLabel i = { cover := c.cover, e := c.ν.symm i, nonempty_equiv_fin := ⋯ }

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.markLabel_cover {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) (i : Fin n) : (c.markLabel i).cover = c.cover

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.markLabel_e {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) (i : Fin n) : (c.markLabel i).e = c.ν.symm i

def TauCeti.ConnectedPointedCover.forgetPoint {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedPointedCover x n) : ConnectedCover x n

Forgetting the chosen point.

Equations

• c.forgetPoint = { cover := c.cover, nonempty_equiv_fin := ⋯ }

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.forgetNumbering_cover {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) : c.forgetNumbering.cover = c.cover

Forgetting the numbering keeps the underlying cover.

@[simp]

theorem TauCeti.ConnectedPointedCover.forgetPoint_cover {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedPointedCover x n) : c.forgetPoint.cover = c.cover

Forgetting the chosen point keeps the underlying cover.

noncomputable def TauCeti.ConnectedCover.numbering {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedCover x n) : ConnectedFiberNumberedCover x n

A cover with some numbering chosen.

Equations

• c.numbering = { cover := c.cover, ν := ⋯.some }

@[simp]

theorem TauCeti.ConnectedCover.numbering_cover {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedCover x n) : c.numbering.cover = c.cover

Choosing a numbering keeps the underlying cover.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.forgetPoint_markLabel {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) (i : Fin n) : (c.markLabel i).forgetPoint = c.forgetNumbering

Marking a label and then forgetting the point is forgetting the numbering.

@[simp]

theorem TauCeti.ConnectedCover.forgetNumbering_numbering {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedCover x n) : c.numbering.forgetNumbering = c

Choosing a numbering and then forgetting it gives back the cover.

def TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering {X : TopCat} {x : ↑X} {n : ℕ} : ConnectedFiberNumberedCoverClass x n → ConnectedCoverClass x n

Forgetting the numbering, on isomorphism classes.

Equations

• TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering = Quotient.map TauCeti.ConnectedFiberNumberedCover.forgetNumbering ⋯

def TauCeti.ConnectedFiberNumberedCoverClass.markLabel {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedFiberNumberedCoverClass x n) (i : Fin n) : ConnectedPointedCoverClass x n

Keeping only the point labelled i, on isomorphism classes: a label-preserving isomorphism preserves in particular the point labelled i.

Equations

• C.markLabel i = Quotient.map (fun (x_1 : TauCeti.ConnectedFiberNumberedCover x n) => x_1.markLabel i) ⋯ C

def TauCeti.ConnectedPointedCoverClass.forgetPoint {X : TopCat} {x : ↑X} {n : ℕ} : ConnectedPointedCoverClass x n → ConnectedCoverClass x n

Forgetting the chosen point, on isomorphism classes.

Equations

• TauCeti.ConnectedPointedCoverClass.forgetPoint = Quotient.map TauCeti.ConnectedPointedCover.forgetPoint ⋯

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering_mk {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) : (mk c).forgetNumbering = ConnectedCoverClass.mk c.forgetNumbering

Forgetting the numbering of the class of c gives the class of c.forgetNumbering.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.markLabel_mk {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) (i : Fin n) : (mk c).markLabel i = ConnectedPointedCoverClass.mk (c.markLabel i)

Marking the label i in the class of c gives the class of c.markLabel i.

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.forgetPoint_mk {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedPointedCover x n) : (mk c).forgetPoint = ConnectedCoverClass.mk c.forgetPoint

Forgetting the point of the class of c gives the class of c.forgetPoint.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.forgetPoint_markLabel {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedFiberNumberedCoverClass x n) (i : Fin n) : (C.markLabel i).forgetPoint = C.forgetNumbering

The forgetful triangle commutes: marking a label and then forgetting the point is forgetting the numbering.

theorem TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering_surjective {X : TopCat} {x : ↑X} {n : ℕ} : Function.Surjective forgetNumbering

Every bare class is obtained by forgetting the numbering of a numbered class, since every cover has a numbering.

theorem TauCeti.ConnectedPointedCoverClass.exists_markLabel_eq {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedPointedCoverClass x n) : ∃ (N : ConnectedFiberNumberedCoverClass x n) (i : Fin n), N.markLabel i = C

Every pointed class is obtained by marking a label in a numbered class.

Relabelling the fibre

@[instance_reducible]

instance TauCeti.ConnectedFiberNumberedCover.instSMulPermFin {X : TopCat} {x : ↑X} {n : ℕ} : SMul (Equiv.Perm (Fin n)) (ConnectedFiberNumberedCover x n)

The symmetric group on the labels acts on numberings by relabelling: τ • ν = ν.trans τ.

Equations

• TauCeti.ConnectedFiberNumberedCover.instSMulPermFin = { smul := fun (τ : Equiv.Perm (Fin n)) (c : TauCeti.ConnectedFiberNumberedCover x n) => { cover := c.cover, ν := c.ν.trans τ } }

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.smul_cover {X : TopCat} {x : ↑X} {n : ℕ} (τ : Equiv.Perm (Fin n)) (c : ConnectedFiberNumberedCover x n) : (τ • c).cover = c.cover

Relabelling keeps the underlying cover.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.smul_ν {X : TopCat} {x : ↑X} {n : ℕ} (τ : Equiv.Perm (Fin n)) (c : ConnectedFiberNumberedCover x n) : (τ • c).ν = c.ν.trans τ

Relabelling by τ composes the numbering with τ.

@[instance_reducible]

instance TauCeti.ConnectedFiberNumberedCover.instMulActionPermFin {X : TopCat} {x : ↑X} {n : ℕ} : MulAction (Equiv.Perm (Fin n)) (ConnectedFiberNumberedCover x n)

Relabelling is an action of the symmetric group on fibre-numbered covers.

Equations

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

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.forgetNumbering_smul {X : TopCat} {x : ↑X} {n : ℕ} (τ : Equiv.Perm (Fin n)) (c : ConnectedFiberNumberedCover x n) : (τ • c).forgetNumbering = c.forgetNumbering

Relabelling does not change the cover left after forgetting the numbering.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.markLabel_smul {X : TopCat} {x : ↑X} {n : ℕ} (τ : Equiv.Perm (Fin n)) (c : ConnectedFiberNumberedCover x n) (i : Fin n) : (τ • c).markLabel i = c.markLabel ((Equiv.symm τ) i)

Relabelling by τ and then marking the label i marks the original label τ.symm i.

theorem TauCeti.ConnectedFiberNumberedCoverIso.smul {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedFiberNumberedCover x n} (h : ConnectedFiberNumberedCoverIso c c') (τ : Equiv.Perm (Fin n)) : ConnectedFiberNumberedCoverIso (τ • c) (τ • c')

Relabelling both sides preserves label-preserving isomorphism.

@[instance_reducible]

instance TauCeti.ConnectedFiberNumberedCoverClass.instSMulPermFin {X : TopCat} {x : ↑X} {n : ℕ} : SMul (Equiv.Perm (Fin n)) (ConnectedFiberNumberedCoverClass x n)

Relabelling descends to classes, since relabelling both sides preserves label-preserving isomorphism.

Equations

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

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.smul_mk {X : TopCat} {x : ↑X} {n : ℕ} (τ : Equiv.Perm (Fin n)) (c : ConnectedFiberNumberedCover x n) : τ • mk c = mk (τ • c)

Relabelling the class of c gives the class of the relabelled cover.

@[instance_reducible]

instance TauCeti.ConnectedFiberNumberedCoverClass.instMulActionPermFin {X : TopCat} {x : ↑X} {n : ℕ} : MulAction (Equiv.Perm (Fin n)) (ConnectedFiberNumberedCoverClass x n)

Relabelling is an action of the symmetric group on classes of fibre-numbered covers.

Equations

• TauCeti.ConnectedFiberNumberedCoverClass.instMulActionPermFin = Function.Surjective.mulAction TauCeti.ConnectedFiberNumberedCoverClass.mk ⋯ ⋯

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering_smul {X : TopCat} {x : ↑X} {n : ℕ} (τ : Equiv.Perm (Fin n)) (C : ConnectedFiberNumberedCoverClass x n) : (τ • C).forgetNumbering = C.forgetNumbering

Relabelling a class does not change its bare class.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.markLabel_smul {X : TopCat} {x : ↑X} {n : ℕ} (τ : Equiv.Perm (Fin n)) (C : ConnectedFiberNumberedCoverClass x n) (i : Fin n) : (τ • C).markLabel i = C.markLabel ((Equiv.symm τ) i)

Relabelling a class by τ and then marking the label i marks the original label τ.symm i.

theorem TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering_eq_forgetNumbering_iff {X : TopCat} {x : ↑X} {n : ℕ} {C C' : ConnectedFiberNumberedCoverClass x n} : C.forgetNumbering = C'.forgetNumbering ↔ ∃ (τ : Equiv.Perm (Fin n)), τ • C' = C

Forgetting the numbering is passing to the relabelling orbit. Two numbered classes have the same underlying cover exactly when a relabelling carries one to the other.

theorem TauCeti.ConnectedFiberNumberedCoverClass.markLabel_eq_markLabel_iff {X : TopCat} {x : ↑X} {n : ℕ} {C C' : ConnectedFiberNumberedCoverClass x n} {i j : Fin n} : C.markLabel i = C'.markLabel j ↔ ∃ (τ : Equiv.Perm (Fin n)), τ • C' = C ∧ τ j = i

Marking a label is passing to the diagonal relabelling orbit. Two numbered classes with marked labels give the same pointed class exactly when a relabelling carries the second class to the first and the second label to the first.

noncomputable def TauCeti.ConnectedFiberNumberedCoverClass.orbitRelQuotientEquiv {X : TopCat} {x : ↑X} {n : ℕ} : MulAction.orbitRel.Quotient (Equiv.Perm (Fin n)) (ConnectedFiberNumberedCoverClass x n) ≃ ConnectedCoverClass x n

The bare isomorphism classes of connected covers of degree n are the relabelling orbits of the numbered classes.

Equations

• TauCeti.ConnectedFiberNumberedCoverClass.orbitRelQuotientEquiv = (Quotient.congrRight ⋯).trans (Setoid.quotientKerEquivOfSurjective TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering ⋯)

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.orbitRelQuotientEquiv_mk {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedFiberNumberedCoverClass x n) : orbitRelQuotientEquiv ⟦C⟧ = C.forgetNumbering

orbitRelQuotientEquiv sends the orbit of a numbered class to its bare class.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.orbitRelQuotientEquiv_symm_forgetNumbering {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedFiberNumberedCoverClass x n) : orbitRelQuotientEquiv.symm C.forgetNumbering = ⟦C⟧

The inverse of orbitRelQuotientEquiv sends the bare class of a numbered class to its orbit.

noncomputable def TauCeti.ConnectedFiberNumberedCoverClass.markedOrbitRelQuotientEquiv {X : TopCat} {x : ↑X} {n : ℕ} : MulAction.orbitRel.Quotient (Equiv.Perm (Fin n)) (ConnectedFiberNumberedCoverClass x n × Fin n) ≃ ConnectedPointedCoverClass x n

The pointed isomorphism classes of connected covers of degree n are the orbits of the diagonal relabelling action on numbered classes with a marked label.

Equations

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

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.markedOrbitRelQuotientEquiv_mk {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedFiberNumberedCoverClass x n) (i : Fin n) : markedOrbitRelQuotientEquiv ⟦(C, i)⟧ = C.markLabel i

markedOrbitRelQuotientEquiv sends the orbit of a numbered class with a marked label to the pointed class obtained by marking that label.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.markedOrbitRelQuotientEquiv_symm_markLabel {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedFiberNumberedCoverClass x n) (i : Fin n) : markedOrbitRelQuotientEquiv.symm (C.markLabel i) = ⟦(C, i)⟧

The inverse of markedOrbitRelQuotientEquiv sends the pointed class obtained by marking the label i of a numbered class to the orbit of that class and label.

Degree and inhabited fibres

theorem TauCeti.ConnectedCover.nonempty_equiv_fin_of_mem_connectedComponent {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedCover x n) {y : ↑X} (hy : y ∈ connectedComponent x) : Nonempty (↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)) ⁻¹' {y}) ≃ Fin n)

The degree is the same over every point of the connected component of x: the number of points in a fibre of a covering map is locally constant.

theorem TauCeti.ConnectedCover.ne_zero {X : TopCat} {x : ↑X} {n : ℕ} [PreconnectedSpace ↑X] (c : ConnectedCover x n) : n ≠ 0

A connected cover of a preconnected space has positive degree.

theorem TauCeti.ConnectedPointedCoverClass.forgetPoint_surjective {X : TopCat} {x : ↑X} {n : ℕ} (hn : n ≠ 0) : Function.Surjective forgetPoint

For positive degree, every bare cover has a point over x, so forgetting the point is surjective on isomorphism classes.

Moving the basepoint

noncomputable def TauCeti.ConnectedFiberNumberedCover.basepointChange {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (c : ConnectedFiberNumberedCover x₀ n) (γ : Path x₀ x₁) : ConnectedFiberNumberedCover x₁ n

Moving the basepoint of a numbered cover along a path γ from x₀ to x₁: the same cover, with the fibre over x₁ numbered by transporting it back to the fibre over x₀ along γ. The numbering depends on γ, through the monodromy of loops at x₀.

Equations

• c.basepointChange γ = { cover := c.cover, ν := (TauCeti.coveringFiberEquiv ⋯ (Path.Homotopic.Quotient.mk γ)).symm.trans c.ν }

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.basepointChange_cover {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (c : ConnectedFiberNumberedCover x₀ n) (γ : Path x₀ x₁) : (c.basepointChange γ).cover = c.cover

theorem TauCeti.ConnectedFiberNumberedCover.basepointChange_ν {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (c : ConnectedFiberNumberedCover x₀ n) (γ : Path x₀ x₁) : (c.basepointChange γ).ν ≍ (coveringFiberEquiv ⋯ (Path.Homotopic.Quotient.mk γ)).symm.trans c.ν

The numbering of the moved cover transports the fibre over x₁ back to the fibre over x₀ along γ and numbers it there. The two fibres live over the same cover only up to basepointChange_cover, so the equality is heterogeneous.

theorem TauCeti.ConnectedFiberNumberedCover.permCongrHom_comp_monodromyPerm_basepointChange {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (c : ConnectedFiberNumberedCover x₀ n) (γ : Path x₀ x₁) : (c.basepointChange γ).ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x₁) = (c.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x₀)).comp (FundamentalGroup.fundamentalGroupMulEquivOfPath γ).symm.toMonoidHom

Moving the basepoint along γ conjugates the numbered monodromy by γ. The numbered monodromy representation of π₁(X, x₁) of the moved cover is that of π₁(X, x₀) precomposed with the basepoint-change isomorphism π₁(X, x₁) ≃* π₁(X, x₀), which sends the class of a loop g at x₁ to the class of γ ⬝ g ⬝ γ⁻¹.

def TauCeti.ConnectedCover.basepointChange {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (c : ConnectedCover x₀ n) (h : x₁ ∈ connectedComponent x₀) : ConnectedCover x₁ n

Moving the basepoint of a bare cover of degree n from x₀ to a point x₁ of its connected component: the same cover, which has degree n over x₁ as well (TauCeti.ConnectedCover.nonempty_equiv_fin_of_mem_connectedComponent).

Equations

• c.basepointChange h = { cover := c.cover, nonempty_equiv_fin := ⋯ }

@[simp]

theorem TauCeti.ConnectedCover.basepointChange_cover {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (c : ConnectedCover x₀ n) (h : x₁ ∈ connectedComponent x₀) : (c.basepointChange h).cover = c.cover

theorem TauCeti.ConnectedFiberNumberedCover.forgetNumbering_basepointChange {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (c : ConnectedFiberNumberedCover x₀ n) (γ : Path x₀ x₁) (h : x₁ ∈ connectedComponent x₀) : (c.basepointChange γ).forgetNumbering = c.forgetNumbering.basepointChange h

Moving the basepoint of a numbered cover along a path and then forgetting the numbering is forgetting the numbering and then moving the basepoint.

def TauCeti.ConnectedCoverClass.basepointChange {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (C : ConnectedCoverClass x₀ n) (h : x₁ ∈ connectedComponent x₀) : ConnectedCoverClass x₁ n

Moving the basepoint of a bare cover to a point of its connected component, on isomorphism classes.

Equations

• C.basepointChange h = Quotient.map (fun (x : TauCeti.ConnectedCover x₀ n) => x.basepointChange h) ⋯ C

@[simp]

theorem TauCeti.ConnectedCoverClass.basepointChange_mk {X : TopCat} {n : ℕ} {x₀ x₁ : ↑X} (c : ConnectedCover x₀ n) (h : x₁ ∈ connectedComponent x₀) : (mk c).basepointChange h = mk (c.basepointChange h)

Numbered monodromy

theorem TauCeti.ConnectedFiberNumberedCoverIso.permCongrHom_comp_monodromyPerm_eq {X : TopCat} {x : ↑X} {n : ℕ} {c c' : ConnectedFiberNumberedCover x n} (h : ConnectedFiberNumberedCoverIso c c') : c.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x) = c'.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x)

Isomorphic numbered covers have the same numbered monodromy. A label-preserving isomorphism of covers identifies their monodromy representations π₁(X, x) →* Equiv.Perm (Fin n) read through the numberings; this direction needs no hypothesis on the base.

theorem TauCeti.ConnectedFiberNumberedCoverIso.of_permCongrHom_comp_monodromyPerm_eq {X : TopCat} {x : ↑X} {n : ℕ} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] {c c' : ConnectedFiberNumberedCover x n} (h : c.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x) = c'.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x)) : ConnectedFiberNumberedCoverIso c c'

Numbered covers with the same numbered monodromy are isomorphic. Over a path-connected, locally path-connected base, if the monodromy representations π₁(X, x) →* Equiv.Perm (Fin n) of two numbered covers, read through their numberings, agree, then some isomorphism of the covers preserves every label.

theorem TauCeti.connectedFiberNumberedCoverIso_iff_permCongrHom_comp_monodromyPerm_eq {X : TopCat} {x : ↑X} {n : ℕ} [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] {c c' : ConnectedFiberNumberedCover x n} : ConnectedFiberNumberedCoverIso c c' ↔ c.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x) = c'.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x)

A numbered connected cover is determined by its numbered monodromy. Over a path-connected, locally path-connected base, two numbered covers are isomorphic, by an isomorphism preserving every label, exactly when their monodromy representations π₁(X, x) →* Equiv.Perm (Fin n), read through the numberings, agree.

Realising a numbered monodromy

theorem TauCeti.ConnectedFiberNumberedCover.exists_permCongrHom_comp_monodromyPerm_eq {X : TopCat} {x : ↑X} {n : ℕ} [LocallyPathConnectedSpace ↑X] [SemilocallySimplyConnectedSpace ↑X] (ρ : FundamentalGroup (↑X) x →* Equiv.Perm (Fin n)) (hn : n ≠ 0) (hρ : MulAction.IsPretransitive (↥ρ.range) (Fin n)) : ∃ (c : ConnectedFiberNumberedCover x n), c.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x) = ρ

Every transitive representation on Fin n is the numbered monodromy of a cover. Over a locally path-connected, semilocally simply connected base, a homomorphism ρ : π₁(X, x) →* Equiv.Perm (Fin n) whose image acts transitively on the nonempty set Fin n is the monodromy representation, read through the numbering, of some connected cover with numbered fibre.

Deck transformations

def TauCeti.ConnectedFiberNumberedCover.deckPerm {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) : ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover))) →* Equiv.Perm (Fin n)

The permutation of the labels induced by a deck transformation of a numbered cover: the label i goes to the label of the image of the point labelled i (deckPerm_apply). This is the permutation representation of the deck action on the fibre, read through the numbering.

Equations

• c.deckPerm = c.ν.permutationRepresentation

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.deckPerm_apply {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) (φ : ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)))) (i : Fin n) : (c.deckPerm φ) i = c.ν (φ • c.ν.symm i)

The label of the image of the point labelled i under a deck transformation.

theorem TauCeti.ConnectedFiberNumberedCover.isPretransitive_range_deckPerm_iff {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) : MulAction.IsPretransitive (↥c.deckPerm.range) (Fin n) ↔ MulAction.IsPretransitive ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover))) ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)) ⁻¹' {x})

The permutations of the labels induced by deck transformations act transitively exactly when the deck group acts transitively on the fibre.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.deckPerm_smul {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) (τ : Equiv.Perm (Fin n)) (φ : ↥(deck ⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c.cover)))) : (τ • c).deckPerm φ = τ * c.deckPerm φ * τ⁻¹

Relabelling the fibre by τ conjugates the permutation induced by each deck transformation by τ.

theorem TauCeti.ConnectedFiberNumberedCover.deckPerm_injective {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) [PreconnectedSpace ↑X] : Function.Injective ⇑c.deckPerm

A deck transformation of a numbered cover is determined by the permutation it induces on the labels. Over a preconnected base the fibre is nonempty, and a deck transformation of a connected cover is determined by its value at one point.

theorem TauCeti.ConnectedFiberNumberedCover.range_deckPerm {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X] : c.deckPerm.range = Subgroup.centralizer ↑(c.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x)).range

The permutations of the labels induced by deck transformations are exactly those commuting with the numbered monodromy. Over a path-connected, locally path-connected base, the image of deckPerm is the centralizer in Equiv.Perm (Fin n) of the monodromy representation π₁(X, x) →* Equiv.Perm (Fin n) read through the numbering.