Pulling connected covers back along a homeomorphism of the base

A homeomorphism h : X ≃ₜ Y pulls a covering space p : E → Y back to the covering space h.symm ∘ p : E → X of X, with the same total space. This file packages that operation on the connected covering spaces of TauCeti.Topology.Covering.Category and on the three rigidified carriers of TauCeti.AlgebraicTopology.UniversalCover.Classification.NumberedFiber, and computes its effect on monodromy.

• TauCeti.ConnectedCoveringSpace.pullback h is the functor ConnectedCoveringSpace Y ⥤ ConnectedCoveringSpace X; it keeps the total space and the maps of total spaces, and composes the projection with h.symm. Pulling back along the identity is the identity functor, and pulling back along a composite is the composite of the pullbacks in the reverse order (TauCeti.ConnectedCoveringSpace.pullback_refl, TauCeti.ConnectedCoveringSpace.pullback_trans), so the self-homeomorphisms of X act on its covers through this functor.
• When h x = y, the fibre of the pulled-back cover over x is the fibre of the original cover over y (TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv), and under that identification the monodromy of the pullback along a loop γ at x is the monodromy of the original cover along the image loop h ∘ γ at y (TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv_monodromy). Pulling back is contravariant: the cover of X sees π₁(X, x) through the isomorphism π₁(X, x) ≃* π₁(Y, y) induced by h.
• Consequently a fibre-numbered cover of (Y, y) pulls back to a fibre-numbered cover of (X, x) whose numbered monodromy representation is the original one precomposed with that isomorphism (TauCeti.ConnectedFiberNumberedCover.permCongrHom_comp_monodromyPerm_pullback), a pointed cover pulls back to a pointed cover, and a bare cover to a bare cover. Pullback descends to the isomorphism classes of all three kinds of covers, satisfies the identity and composition laws on the nose at every level, and commutes with relabelling and with the forgetful maps between the levels.

For the thrice-punctured sphere this is how the anharmonic self-homeomorphisms act on covers: the pullback along z ↦ 1 − z, which fixes the basepoint, realizes the exchange of the branch points 0 and 1 on monodromy triples.

Main declarations

• TauCeti.ConnectedCoveringSpace.pullback: the pullback functor along a homeomorphism of bases, with TauCeti.ConnectedCoveringSpace.pullback_refl and TauCeti.ConnectedCoveringSpace.pullback_trans.
• TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv, TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv_monodromy: the fibre identification and its compatibility with monodromy.
• TauCeti.ConnectedFiberNumberedCover.pullback, TauCeti.ConnectedPointedCover.pullback, TauCeti.ConnectedCover.pullback: pullback of numbered, of pointed and of bare covers, with TauCeti.ConnectedFiberNumberedCover.permCongrHom_comp_monodromyPerm_pullback computing the numbered monodromy of the pullback, and the laws pullback_refl and pullback_pullback in each namespace.
• TauCeti.ConnectedFiberNumberedCoverClass.pullback, TauCeti.ConnectedPointedCoverClass.pullback, TauCeti.ConnectedCoverClass.pullback: the descended maps on isomorphism classes, with their pullback_mk, pullback_refl and pullback_pullback lemmas and the compatibilities TauCeti.ConnectedFiberNumberedCoverClass.pullback_smul, TauCeti.ConnectedFiberNumberedCoverClass.markLabel_pullback, TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering_pullback and TauCeti.ConnectedPointedCoverClass.forgetPoint_pullback.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, §1.3 (change of base for covering spaces and the action of the fundamental group on a fibre).

def TauCeti.ConnectedCoveringSpace.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) : CategoryTheory.Functor (ConnectedCoveringSpace Y) (ConnectedCoveringSpace X)

The pullback of connected covering spaces along a homeomorphism h : X ≃ₜ Y of bases: the total space is unchanged and the projection is composed with h.symm. On morphisms it is the identity on maps of total spaces.

Equations

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

@[simp]

theorem TauCeti.ConnectedCoveringSpace.pullback_obj_proj_apply {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) (c : ConnectedCoveringSpace Y) (e : ↑((pullback h).obj c).obj.left) : (CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj ((pullback h).obj c))) e = h.symm ((CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c)) e)

The projection of the pullback is the original projection followed by h.symm.

@[simp]

theorem TauCeti.ConnectedCoveringSpace.pullback_map_hom_left {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {c c' : ConnectedCoveringSpace Y} (f : c ⟶ c') : CategoryTheory.Over.Hom.left ((pullback h).map f).hom = CategoryTheory.Over.Hom.left f.hom

The pullback functor acts on morphisms by the same map of total spaces.

@[simp]

theorem TauCeti.ConnectedCoveringSpace.pullback_refl {X : TopCat} : pullback (Homeomorph.refl ↑X) = CategoryTheory.Functor.id (ConnectedCoveringSpace X)

Pulling back along the identity is the identity functor.

@[simp]

theorem TauCeti.ConnectedCoveringSpace.pullback_trans {X Y Z : TopCat} (h : ↑X ≃ₜ ↑Y) (h' : ↑Y ≃ₜ ↑Z) : pullback (h.trans h') = (pullback h').comp (pullback h)

Pulling back along a composite homeomorphism is the composite of the pullbacks, in the reverse order.

def TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) (c : ConnectedCoveringSpace Y) {x : ↑X} {y : ↑Y} (hx : h x = y) : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj ((pullback h).obj c))) ⁻¹' {x}) ≃ ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c)) ⁻¹' {y})

When h x = y, the fibre of the pullback over x is the fibre of the original cover over y: both are the same subset of the common total space.

Equations

• TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv h c hx = Equiv.subtypeEquivRight ⋯

@[simp]

theorem TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv_apply_coe {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) (c : ConnectedCoveringSpace Y) {x : ↑X} {y : ↑Y} (hx : h x = y) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj ((pullback h).obj c))) ⁻¹' {x})) : ↑((pullbackFiberEquiv h c hx) e) = ↑e

On underlying points, the fibre identification of the pullback is the identity.

@[simp]

theorem TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv_symm_apply_coe {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) (c : ConnectedCoveringSpace Y) {x : ↑X} {y : ↑Y} (hx : h x = y) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj c)) ⁻¹' {y})) : ↑((pullbackFiberEquiv h c hx).symm e) = ↑e

On underlying points, the inverse fibre identification of the pullback is the identity.

theorem TauCeti.ConnectedCoveringSpace.pullbackFiberEquiv_monodromy {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) (c : ConnectedCoveringSpace Y) {x : ↑X} {y : ↑Y} (hx : h x = y) (γ : FundamentalGroup (↑X) x) (e : ↑(⇑(CategoryTheory.ConcreteCategory.hom (CoveringSpace.FullSubcategory.proj ((pullback h).obj c))) ⁻¹' {x})) : (pullbackFiberEquiv h c hx) (⋯.monodromy γ e) = ⋯.monodromy ((FundamentalGroup.homeomorphMulEquivOfEq h hx) γ) ((pullbackFiberEquiv h c hx) e)

The monodromy of a pullback is the monodromy along the image loop. Under the fibre identification, the pullback along h transports a point of the fibre along a loop γ at x exactly as the original cover transports it along h ∘ γ at y.

Fibre-numbered covers

def TauCeti.ConnectedFiberNumberedCover.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedFiberNumberedCover y n) : ConnectedFiberNumberedCover x n

The pullback of a fibre-numbered cover of (Y, y) along a homeomorphism h with h x = y: the pulled-back cover, with the fibre over x numbered through the fibre over y.

Equations

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

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.pullback_cover {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedFiberNumberedCover y n) : (pullback h hx c).cover = (ConnectedCoveringSpace.pullback h).obj c.cover

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.pullback_ν {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedFiberNumberedCover y n) : (pullback h hx c).ν = (ConnectedCoveringSpace.pullbackFiberEquiv h c.cover hx).trans c.ν

theorem TauCeti.ConnectedFiberNumberedCover.permCongrHom_comp_monodromyPerm_pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedFiberNumberedCover y n) : (pullback h hx c).ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm x) = (c.ν.permCongrHom.toMonoidHom.comp (⋯.monodromyPerm y)).comp (FundamentalGroup.homeomorphMulEquivOfEq h hx).toMonoidHom

The numbered monodromy of a pullback is the numbered monodromy precomposed with the induced isomorphism of fundamental groups.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.pullback_smul {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedFiberNumberedCover y n) (τ : Equiv.Perm (Fin n)) : pullback h hx (τ • c) = τ • pullback h hx c

Relabelling commutes with pullback.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.pullback_refl {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedFiberNumberedCover x n) : pullback (Homeomorph.refl ↑X) ⋯ c = c

Pulling back along the identity changes nothing.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.pullback_pullback {X Y Z : TopCat} (h : ↑X ≃ₜ ↑Y) (h' : ↑Y ≃ₜ ↑Z) {x : ↑X} {y : ↑Y} {z : ↑Z} (hx : h x = y) (hy : h' y = z) {n : ℕ} (c : ConnectedFiberNumberedCover z n) : pullback h hx (pullback h' hy c) = pullback (h.trans h') ⋯ c

Pulling back twice is pulling back along the composite homeomorphism.

theorem TauCeti.ConnectedFiberNumberedCoverIso.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} {c c' : ConnectedFiberNumberedCover y n} (hcc : ConnectedFiberNumberedCoverIso c c') : ConnectedFiberNumberedCoverIso (ConnectedFiberNumberedCover.pullback h hx c) (ConnectedFiberNumberedCover.pullback h hx c')

A label-preserving isomorphism of numbered covers pulls back to one.

def TauCeti.ConnectedFiberNumberedCoverClass.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} : ConnectedFiberNumberedCoverClass y n → ConnectedFiberNumberedCoverClass x n

Pullback along h, on isomorphism classes of fibre-numbered covers.

Equations

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

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.pullback_mk {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedFiberNumberedCover y n) : pullback h hx (mk c) = mk (ConnectedFiberNumberedCover.pullback h hx c)

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.pullback_smul {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (τ : Equiv.Perm (Fin n)) (C : ConnectedFiberNumberedCoverClass y n) : pullback h hx (τ • C) = τ • pullback h hx C

Relabelling commutes with pullback on classes.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.pullback_refl {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedFiberNumberedCoverClass x n) : pullback (Homeomorph.refl ↑X) ⋯ C = C

Pulling back along the identity changes nothing, on classes.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.pullback_pullback {X Y Z : TopCat} (h : ↑X ≃ₜ ↑Y) (h' : ↑Y ≃ₜ ↑Z) {x : ↑X} {y : ↑Y} {z : ↑Z} (hx : h x = y) (hy : h' y = z) {n : ℕ} (C : ConnectedFiberNumberedCoverClass z n) : pullback h hx (pullback h' hy C) = pullback (h.trans h') ⋯ C

Pulling back twice is pulling back along the composite homeomorphism, on classes.

Pointed covers

def TauCeti.ConnectedPointedCover.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedPointedCover y n) : ConnectedPointedCover x n

The pullback of a pointed cover of (Y, y) along a homeomorphism h with h x = y: the pulled-back cover, pointed at the same point, which lies over x in the pullback.

Equations

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

@[simp]

theorem TauCeti.ConnectedPointedCover.pullback_cover {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedPointedCover y n) : (pullback h hx c).cover = (ConnectedCoveringSpace.pullback h).obj c.cover

@[simp]

theorem TauCeti.ConnectedPointedCover.pullback_e {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedPointedCover y n) : (pullback h hx c).e = (ConnectedCoveringSpace.pullbackFiberEquiv h c.cover hx).symm c.e

@[simp]

theorem TauCeti.ConnectedPointedCover.pullback_refl {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedPointedCover x n) : pullback (Homeomorph.refl ↑X) ⋯ c = c

Pulling back along the identity changes nothing.

@[simp]

theorem TauCeti.ConnectedPointedCover.pullback_pullback {X Y Z : TopCat} (h : ↑X ≃ₜ ↑Y) (h' : ↑Y ≃ₜ ↑Z) {x : ↑X} {y : ↑Y} {z : ↑Z} (hx : h x = y) (hy : h' y = z) {n : ℕ} (c : ConnectedPointedCover z n) : pullback h hx (pullback h' hy c) = pullback (h.trans h') ⋯ c

Pulling back twice is pulling back along the composite homeomorphism.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.markLabel_pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedFiberNumberedCover y n) (i : Fin n) : (pullback h hx c).markLabel i = ConnectedPointedCover.pullback h hx (c.markLabel i)

Marking a label commutes with pullback.

theorem TauCeti.ConnectedPointedCoverIso.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} {c c' : ConnectedPointedCover y n} (hcc : ConnectedPointedCoverIso c c') : ConnectedPointedCoverIso (ConnectedPointedCover.pullback h hx c) (ConnectedPointedCover.pullback h hx c')

A pointed isomorphism of pointed covers pulls back to one.

noncomputable def TauCeti.ConnectedPointedCoverClass.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (C : ConnectedPointedCoverClass y n) : ConnectedPointedCoverClass x n

Pullback along h, on isomorphism classes of pointed covers: pull back the class of any numbering of the cover and mark the label of the chosen point again. This does not depend on the numbering because pullback commutes with relabelling (TauCeti.ConnectedFiberNumberedCoverClass.pullback_smul), and it is characterized by TauCeti.ConnectedFiberNumberedCoverClass.markLabel_pullback and pullback_mk.

Equations

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

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.markLabel_pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (C : ConnectedFiberNumberedCoverClass y n) (i : Fin n) : (pullback h hx C).markLabel i = ConnectedPointedCoverClass.pullback h hx (C.markLabel i)

Marking a label commutes with pullback, on classes.

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.pullback_mk {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedPointedCover y n) : pullback h hx (mk c) = mk (ConnectedPointedCover.pullback h hx c)

The pullback of the class of a pointed cover is the class of its pullback.

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.pullback_refl {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedPointedCoverClass x n) : pullback (Homeomorph.refl ↑X) ⋯ C = C

Pulling back along the identity changes nothing, on classes.

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.pullback_pullback {X Y Z : TopCat} (h : ↑X ≃ₜ ↑Y) (h' : ↑Y ≃ₜ ↑Z) {x : ↑X} {y : ↑Y} {z : ↑Z} (hx : h x = y) (hy : h' y = z) {n : ℕ} (C : ConnectedPointedCoverClass z n) : pullback h hx (pullback h' hy C) = pullback (h.trans h') ⋯ C

Pulling back twice is pulling back along the composite homeomorphism, on classes.

Bare covers

def TauCeti.ConnectedCover.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedCover y n) : ConnectedCover x n

The pullback of a bare cover of (Y, y) of degree n along a homeomorphism h with h x = y, a bare cover of (X, x) of degree n.

Equations

• TauCeti.ConnectedCover.pullback h hx c = { cover := (TauCeti.ConnectedCoveringSpace.pullback h).obj c.cover, nonempty_equiv_fin := ⋯ }

@[simp]

theorem TauCeti.ConnectedCover.pullback_cover {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedCover y n) : (pullback h hx c).cover = (ConnectedCoveringSpace.pullback h).obj c.cover

@[simp]

theorem TauCeti.ConnectedCover.pullback_refl {X : TopCat} {x : ↑X} {n : ℕ} (c : ConnectedCover x n) : pullback (Homeomorph.refl ↑X) ⋯ c = c

Pulling back along the identity changes nothing.

@[simp]

theorem TauCeti.ConnectedCover.pullback_pullback {X Y Z : TopCat} (h : ↑X ≃ₜ ↑Y) (h' : ↑Y ≃ₜ ↑Z) {x : ↑X} {y : ↑Y} {z : ↑Z} (hx : h x = y) (hy : h' y = z) {n : ℕ} (c : ConnectedCover z n) : pullback h hx (pullback h' hy c) = pullback (h.trans h') ⋯ c

Pulling back twice is pulling back along the composite homeomorphism.

@[simp]

theorem TauCeti.ConnectedFiberNumberedCover.forgetNumbering_pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedFiberNumberedCover y n) : (pullback h hx c).forgetNumbering = ConnectedCover.pullback h hx c.forgetNumbering

Forgetting the numbering commutes with pullback.

@[simp]

theorem TauCeti.ConnectedPointedCover.forgetPoint_pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedPointedCover y n) : (pullback h hx c).forgetPoint = ConnectedCover.pullback h hx c.forgetPoint

Forgetting the chosen point commutes with pullback.

noncomputable def TauCeti.ConnectedCoverClass.pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (C : ConnectedCoverClass y n) : ConnectedCoverClass x n

Pullback along h, on isomorphism classes of bare covers: pull back the class of any numbering of the cover and forget the numbering again. This does not depend on the numbering because pullback commutes with relabelling (TauCeti.ConnectedFiberNumberedCoverClass.pullback_smul), and it is characterized by TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering_pullback and pullback_mk.

Equations

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

@[simp]

theorem TauCeti.ConnectedFiberNumberedCoverClass.forgetNumbering_pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (C : ConnectedFiberNumberedCoverClass y n) : (pullback h hx C).forgetNumbering = ConnectedCoverClass.pullback h hx C.forgetNumbering

Forgetting the numbering commutes with pullback, on classes.

@[simp]

theorem TauCeti.ConnectedCoverClass.pullback_mk {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (c : ConnectedCover y n) : pullback h hx (mk c) = mk (ConnectedCover.pullback h hx c)

The pullback of the class of a bare cover is the class of its pullback.

@[simp]

theorem TauCeti.ConnectedPointedCoverClass.forgetPoint_pullback {X Y : TopCat} (h : ↑X ≃ₜ ↑Y) {x : ↑X} {y : ↑Y} (hx : h x = y) {n : ℕ} (C : ConnectedPointedCoverClass y n) : (pullback h hx C).forgetPoint = ConnectedCoverClass.pullback h hx C.forgetPoint

Forgetting the chosen point commutes with pullback, on classes.

@[simp]

theorem TauCeti.ConnectedCoverClass.pullback_refl {X : TopCat} {x : ↑X} {n : ℕ} (C : ConnectedCoverClass x n) : pullback (Homeomorph.refl ↑X) ⋯ C = C

Pulling back along the identity changes nothing, on classes.

@[simp]

theorem TauCeti.ConnectedCoverClass.pullback_pullback {X Y Z : TopCat} (h : ↑X ≃ₜ ↑Y) (h' : ↑Y ≃ₜ ↑Z) {x : ↑X} {y : ↑Y} {z : ↑Z} (hx : h x = y) (hy : h' y = z) {n : ℕ} (C : ConnectedCoverClass z n) : pullback h hx (pullback h' hy C) = pullback (h.trans h') ⋯ C

Pulling back twice is pulling back along the composite homeomorphism, on classes.