The category of covering spaces over a fixed base

For a topological space X, this file defines TauCeti.CoveringSpace X, whose objects are covering maps to X and whose morphisms are continuous maps over X. It is constructed as the full subcategory of TopCat / X cut out by IsCoveringMap, so its category structure and the commuting triangle carried by every morphism come from Mathlib's Over and ObjectProperty.FullSubcategory APIs.

Full subcategories of TauCeti.CoveringSpace X cut out by a further property of the underlying object of TopCat / X are packaged once as TauCeti.CoveringSpace.FullSubcategory X P, which carries the constructor API. TauCeti.ConnectedCoveringSpace X, the covers with connected total space, is the instance taking P to be connectedness; TauCeti.FiniteCoveringSpace in TauCeti.Topology.Covering.Finite is the other.

Each is a reducible abbreviation, so the general API applies to it unchanged. What a subcategory restates is its constructor together with the computation lemmas that mention it — mk, mk_coe, mk_proj, forget_obj_mk — and its own forget, which fixes P; it adds whatever its property gives, such as TauCeti.ConnectedCoveringSpace.connectedSpace. The docstring of TauCeti.CoveringSpace.FullSubcategory says how to name the rest from a subcategory.

The connected covers are the source category for the classification by transitive fundamental-group actions.

Main declarations

• TauCeti.Over.isCoveringMap and TauCeti.Over.isCoveringMap_iff: the property of an object of TopCat / X that its structure morphism is a covering map, and its membership lemma.
• TauCeti.CoveringSpace X: covering spaces over X and maps over X.
• TauCeti.CoveringSpace.mk, proj, homMk, isoMk: constructors for covering spaces and their morphisms and isomorphisms.
• TauCeti.CoveringSpace.forget, fullyFaithfulForget: the inclusion into TopCat / X and its full faithfulness.
• TauCeti.CoveringSpace.totalSpace: the functor taking a cover to its total space.
• TauCeti.CoveringSpace.isIso_iff_isHomeomorph_hom_left: a map of covers is an isomorphism exactly when its map of total spaces is a homeomorphism.
• TauCeti.CoveringSpace.isInitial_iff_isEmpty: a cover is an initial object exactly when its total space is empty.
• TauCeti.CoveringSpace.FullSubcategory X P: the full subcategory of covers whose underlying object satisfies P.
• TauCeti.CoveringSpace.FullSubcategory.mk, mk_coe, mk_proj, forget_obj_mk, proj, homMk, isoMk: the constructor API shared by every such subcategory.
• TauCeti.CoveringSpace.FullSubcategory.prop_obj: the cutting property of an object.
• TauCeti.CoveringSpace.FullSubcategory.totalSpace, totalSpace_obj, totalSpace_map: the functor taking an object to its total space, and its characteristic equations.
• TauCeti.CoveringSpace.FullSubcategory.forget: the inclusion into all covers.
• TauCeti.CoveringSpace.FullSubcategory.isIso_iff_isHomeomorph_hom_left: the corresponding isomorphism criterion.
• TauCeti.ConnectedCoveringSpace X: connected covering spaces over X, with TauCeti.ConnectedCoveringSpace.mk, mk_coe, mk_proj, forget_obj_mk and forget.
• TauCeti.ConnectedCoveringSpace.connectedSpace: the total space of a connected covering space is connected.

References

The construction follows Mathlib's CategoryTheory.MonoOver: both are full subcategories of an over category selected by a property of the structure morphism. The forget, mk, proj, homMk, isoMk, and isomorphism-characterization APIs are adapted from Mathlib/CategoryTheory/Subobject/MonoOver.lean, using the generic Over and ObjectProperty.FullSubcategory constructors directly, and are stated once for TauCeti.CoveringSpace.FullSubcategory.

def TauCeti.Over.isCoveringMap (X : TopCat) : CategoryTheory.ObjectProperty (CategoryTheory.Over X)

The property of an object of TopCat / X that its structure morphism is a covering map.

Equations

• TauCeti.Over.isCoveringMap X p = IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p.hom)

@[simp]

theorem TauCeti.Over.isCoveringMap_iff {X : TopCat} {p : CategoryTheory.Over X} : isCoveringMap X p ↔ IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p.hom)

Membership in the covering-map property of objects of TopCat / X.

This is the lemma downstream modules use to build objects of the full subcategories that TauCeti.Over.isCoveringMap cuts out from a bare proof of IsCoveringMap.

theorem TauCeti.Over.isIso_iff_isHomeomorph_left {X : TopCat} {p q : CategoryTheory.Over X} (f : p ⟶ q) : CategoryTheory.IsIso f ↔ IsHomeomorph ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left f))

A morphism in TopCat / X is an isomorphism exactly when its map on left objects is a homeomorphism.

@[reducible, inline]

abbrev TauCeti.CoveringSpace (X : TopCat) : Type (u + 1)

The category of covering spaces over X. Its objects are covering maps to X, and its morphisms are continuous maps commuting with the projections to X.

Equations

• TauCeti.CoveringSpace X = (TauCeti.Over.isCoveringMap X).FullSubcategory

@[reducible, inline]

abbrev TauCeti.CoveringSpace.forget (X : TopCat) : CategoryTheory.Functor (CoveringSpace X) (CategoryTheory.Over X)

The fully faithful inclusion of covering spaces over X into TopCat / X.

Equations

• TauCeti.CoveringSpace.forget X = (TauCeti.Over.isCoveringMap X).ι

@[reducible, inline]

abbrev TauCeti.CoveringSpace.totalSpace (X : TopCat) : CategoryTheory.Functor (CoveringSpace X) TopCat

The functor taking a covering space to its total space.

Equations

• TauCeti.CoveringSpace.totalSpace X = (TauCeti.CoveringSpace.forget X).comp (CategoryTheory.Over.forget X)

@[instance_reducible]

instance TauCeti.CoveringSpace.instCoeOutTopCat {X : TopCat} : CoeOut (CoveringSpace X) TopCat

A covering space over X coerces to its total space.

Equations

• TauCeti.CoveringSpace.instCoeOutTopCat = { coe := fun (p : TauCeti.CoveringSpace X) => p.obj.left }

def TauCeti.CoveringSpace.mk {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) : CoveringSpace X

Construct a covering space over X from a covering map p. The definition is @[expose]d so that its total space is E and its projection is p by rfl in downstream modules.

Equations

• TauCeti.CoveringSpace.mk p hp = { obj := CategoryTheory.Over.mk p, property := ⋯ }

@[simp]

theorem TauCeti.CoveringSpace.mk_coe {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) : (mk p hp).obj.left = E

@[reducible, inline]

abbrev TauCeti.CoveringSpace.proj {X : TopCat} (p : CoveringSpace X) : p.obj.left ⟶ X

The projection of a covering space to its base.

Equations

• p.proj = p.obj.hom

theorem TauCeti.CoveringSpace.forget_obj_left {X : TopCat} (p : CoveringSpace X) : ((forget X).obj p).left = p.obj.left

theorem TauCeti.CoveringSpace.forget_obj_hom {X : TopCat} (p : CoveringSpace X) : ((forget X).obj p).hom = p.proj

@[simp]

theorem TauCeti.CoveringSpace.mk_proj {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) : (mk p hp).proj = p

theorem TauCeti.CoveringSpace.isCoveringMap_proj {X : TopCat} (p : CoveringSpace X) : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p.proj)

The projection from an object of CoveringSpace X is a covering map.

def TauCeti.CoveringSpace.fullyFaithfulForget (X : TopCat) : (forget X).FullyFaithful

The inclusion CoveringSpace X ⥤ TopCat / X is fully faithful.

Equations

• TauCeti.CoveringSpace.fullyFaithfulForget X = (TauCeti.Over.isCoveringMap X).fullyFaithfulι

theorem TauCeti.CoveringSpace.totalSpace_obj {X : TopCat} (p : CoveringSpace X) : (totalSpace X).obj p = p.obj.left

theorem TauCeti.CoveringSpace.totalSpace_map {X : TopCat} {p q : CoveringSpace X} (f : p ⟶ q) : (totalSpace X).map f = CategoryTheory.Over.Hom.left f.hom

theorem TauCeti.CoveringSpace.w {X : TopCat} {p q : CoveringSpace X} (f : p ⟶ q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom) q.proj = p.proj

A morphism of covering spaces commutes with the projections to the base.

theorem TauCeti.CoveringSpace.w_assoc {X : TopCat} {p q : CoveringSpace X} (f : p ⟶ q) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom) (CategoryTheory.CategoryStruct.comp q.proj h) = CategoryTheory.CategoryStruct.comp p.proj h

A morphism of covering spaces commutes with the projections to the base.

theorem TauCeti.CoveringSpace.proj_hom_comp_hom_left_hom {X : TopCat} {p q : CoveringSpace X} (f : p ⟶ q) : ⇑(TopCat.Hom.hom q.proj) ∘ ⇑(TopCat.Hom.hom (CategoryTheory.Over.Hom.left f.hom)) = ⇑(TopCat.Hom.hom p.proj)

The commuting triangle of a morphism of covering spaces, as an equality of the underlying functions.

def TauCeti.CoveringSpace.homMk {X : TopCat} {p q : CoveringSpace X} (f : p.obj.left ⟶ q.obj.left) (w : CategoryTheory.CategoryStruct.comp f q.proj = p.proj := by cat_disch) : p ⟶ q

Construct a morphism of covering spaces from a continuous map over the base.

Equations

• TauCeti.CoveringSpace.homMk f w = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk f w)

@[simp]

theorem TauCeti.CoveringSpace.homMk_hom_left {X : TopCat} {p q : CoveringSpace X} (f : p.obj.left ⟶ q.obj.left) (w : CategoryTheory.CategoryStruct.comp f q.proj = p.proj) : CategoryTheory.Over.Hom.left (homMk f w).hom = f

def TauCeti.CoveringSpace.isoMk {X : TopCat} {p q : CoveringSpace X} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj := by cat_disch) : p ≅ q

Construct an isomorphism of covering spaces from an isomorphism of their total spaces over the base.

Equations

• TauCeti.CoveringSpace.isoMk e w = (TauCeti.Over.isCoveringMap X).isoMk (CategoryTheory.Over.isoMk e w)

@[simp]

theorem TauCeti.CoveringSpace.isoMk_hom_hom_left {X : TopCat} {p q : CoveringSpace X} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj) : CategoryTheory.Over.Hom.left (isoMk e w).hom.hom = e.hom

@[simp]

theorem TauCeti.CoveringSpace.isoMk_inv_hom_left {X : TopCat} {p q : CoveringSpace X} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj) : CategoryTheory.Over.Hom.left (isoMk e w).inv.hom = e.inv

def TauCeti.CoveringSpace.mkProjIso {X : TopCat} (p : CoveringSpace X) : mk p.proj ⋯ ≅ p

Reconstructing a covering space from its projection gives an isomorphic object.

Equations

• p.mkProjIso = TauCeti.CoveringSpace.isoMk (CategoryTheory.Iso.refl (TauCeti.CoveringSpace.mk p.proj ⋯).obj.left) ⋯

@[simp]

theorem TauCeti.CoveringSpace.mkProjIso_hom_hom_left {X : TopCat} (p : CoveringSpace X) : CategoryTheory.Over.Hom.left p.mkProjIso.hom.hom = CategoryTheory.eqToHom ⋯

@[simp]

theorem TauCeti.CoveringSpace.mkProjIso_inv_hom_left {X : TopCat} (p : CoveringSpace X) : CategoryTheory.Over.Hom.left p.mkProjIso.inv.hom = CategoryTheory.eqToHom ⋯

theorem TauCeti.CoveringSpace.isIso_iff_isHomeomorph_hom_left {X : TopCat} {p q : CoveringSpace X} (f : p ⟶ q) : CategoryTheory.IsIso f ↔ IsHomeomorph ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left f.hom))

A map of covering spaces is an isomorphism exactly when its map of total spaces is a homeomorphism.

@[simp]

theorem TauCeti.CoveringSpace.isInitial_iff_isEmpty {X : TopCat} (p : CoveringSpace X) : Nonempty (CategoryTheory.Limits.IsInitial p) ↔ IsEmpty ↑p.obj.left

A covering space of X is an initial object of TauCeti.CoveringSpace X exactly when its total space is empty. The empty space covers X — vacuously, by IsCoveringMap.of_isEmpty — and is the initial object, so a cover is "non-initial" exactly when it is nonempty. No hypothesis on X is needed.

@[reducible, inline]

abbrev TauCeti.CoveringSpace.FullSubcategory (X : TopCat) (P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)) : Type (u + 1)

The full subcategory of TauCeti.CoveringSpace X cut out by a further property P of the underlying object of TopCat / X.

A subcategory of covers is built by abbreviating this type at its own P, as TauCeti.ConnectedCoveringSpace and TauCeti.FiniteCoveringSpace do. Such a subcategory restates only its constructor and the lemmas naming it — mk, mk_coe, mk_proj, forget_obj_mk — since each takes its property in a different form, and its own forget, which fixes P. The rest of the API below is used from it rather than restated:

• object accessors support dot notation: p.proj, p.prop_obj, p.isCoveringMap_proj, and p.mkProjIso;
• morphism constructors and the commuting triangle can be named as CoveringSpace.FullSubcategory.homMk f w, CoveringSpace.FullSubcategory.isoMk e w, and CoveringSpace.FullSubcategory.w f. The forms p.homMk f w, p.isoMk e w, and p.w f also work: generalized field notation supplies the implicit source object (p := p);
• f.w does not resolve because the morphism type is headed by CategoryTheory.InducedCategory.Hom; use the qualified form or p.w f instead;
• a member parameterized only by X and P is named through this namespace.

Equations

• TauCeti.CoveringSpace.FullSubcategory X P = (TauCeti.Over.isCoveringMap X ⊓ P).FullSubcategory

@[reducible, inline]

abbrev TauCeti.CoveringSpace.FullSubcategory.forget (X : TopCat) (P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)) : CategoryTheory.Functor (FullSubcategory X P) (CoveringSpace X)

The inclusion into all covering spaces. It is fully faithful: Full and Faithful are found by instance search from Mathlib's ObjectProperty.full_ιOfLE and ObjectProperty.faithful_ιOfLE, and the bundled witness is ObjectProperty.fullyFaithfulιOfLE inf_le_left.

Equations

• TauCeti.CoveringSpace.FullSubcategory.forget X P = CategoryTheory.ObjectProperty.ιOfLE ⋯

@[instance_reducible]

instance TauCeti.CoveringSpace.FullSubcategory.instCoeOutTopCat {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} : CoeOut (FullSubcategory X P) TopCat

An object of a full subcategory of covering spaces coerces to its total space.

Equations

• TauCeti.CoveringSpace.FullSubcategory.instCoeOutTopCat = { coe := fun (p : TauCeti.CoveringSpace.FullSubcategory X P) => p.obj.left }

def TauCeti.CoveringSpace.FullSubcategory.mk {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hP : P (CategoryTheory.Over.mk p)) : FullSubcategory X P

Construct an object from a covering map whose underlying object satisfies P. The definition is @[expose]d so that its total space is E and its projection is p by rfl in downstream modules.

Equations

• TauCeti.CoveringSpace.FullSubcategory.mk p hp hP = { obj := CategoryTheory.Over.mk p, property := ⋯ }

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.mk_coe {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hP : P (CategoryTheory.Over.mk p)) : (mk p hp hP).obj.left = E

@[reducible, inline]

abbrev TauCeti.CoveringSpace.FullSubcategory.proj {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} (p : FullSubcategory X P) : p.obj.left ⟶ X

The projection of an object to its base.

Equations

• p.proj = p.obj.hom

@[reducible, inline]

abbrev TauCeti.CoveringSpace.FullSubcategory.totalSpace (X : TopCat) (P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)) : CategoryTheory.Functor (FullSubcategory X P) TopCat

The functor taking an object to its total space.

Equations

• TauCeti.CoveringSpace.FullSubcategory.totalSpace X P = (TauCeti.CoveringSpace.FullSubcategory.forget X P).comp (TauCeti.CoveringSpace.totalSpace X)

theorem TauCeti.CoveringSpace.FullSubcategory.totalSpace_obj {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} (p : FullSubcategory X P) : (totalSpace X P).obj p = p.obj.left

The total-space functor sends an object to its total space.

theorem TauCeti.CoveringSpace.FullSubcategory.totalSpace_map {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (f : p ⟶ q) : (totalSpace X P).map f = CategoryTheory.Over.Hom.left f.hom

The total-space functor sends a morphism to its map of total spaces.

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.forget_obj_proj {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} (p : FullSubcategory X P) : ((forget X P).obj p).proj = p.proj

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.mk_proj {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hP : P (CategoryTheory.Over.mk p)) : (mk p hp hP).proj = p

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.forget_obj_mk {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) (hP : P (CategoryTheory.Over.mk p)) : (forget X P).obj (mk p hp hP) = CoveringSpace.mk p hp

theorem TauCeti.CoveringSpace.FullSubcategory.isCoveringMap_proj {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} (p : FullSubcategory X P) : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p.proj)

The projection from an object of a full subcategory of covering spaces is a covering map.

theorem TauCeti.CoveringSpace.FullSubcategory.prop_obj {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} (p : FullSubcategory X P) : P p.obj

The cutting property holds of the underlying object of TopCat / X.

theorem TauCeti.CoveringSpace.FullSubcategory.w {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (f : p ⟶ q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom) q.proj = p.proj

A morphism commutes with the projections to the base.

theorem TauCeti.CoveringSpace.FullSubcategory.w_assoc {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (f : p ⟶ q) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f.hom) (CategoryTheory.CategoryStruct.comp q.proj h) = CategoryTheory.CategoryStruct.comp p.proj h

A morphism commutes with the projections to the base.

def TauCeti.CoveringSpace.FullSubcategory.homMk {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (f : p.obj.left ⟶ q.obj.left) (w : CategoryTheory.CategoryStruct.comp f q.proj = p.proj := by cat_disch) : p ⟶ q

Construct a morphism from a continuous map over the base.

Equations

• TauCeti.CoveringSpace.FullSubcategory.homMk f w = CategoryTheory.ObjectProperty.homMk (CategoryTheory.Over.homMk f w)

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.homMk_hom_left {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (f : p.obj.left ⟶ q.obj.left) (w : CategoryTheory.CategoryStruct.comp f q.proj = p.proj) : CategoryTheory.Over.Hom.left (homMk f w).hom = f

def TauCeti.CoveringSpace.FullSubcategory.isoMk {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj := by cat_disch) : p ≅ q

Construct an isomorphism from an isomorphism of total spaces over the base.

Equations

• TauCeti.CoveringSpace.FullSubcategory.isoMk e w = (TauCeti.Over.isCoveringMap X ⊓ P).isoMk (CategoryTheory.Over.isoMk e w)

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.isoMk_hom_hom_left {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj) : CategoryTheory.Over.Hom.left (isoMk e w).hom.hom = e.hom

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.isoMk_inv_hom_left {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (e : p.obj.left ≅ q.obj.left) (w : CategoryTheory.CategoryStruct.comp e.hom q.proj = p.proj) : CategoryTheory.Over.Hom.left (isoMk e w).inv.hom = e.inv

def TauCeti.CoveringSpace.FullSubcategory.mkProjIso {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} (p : FullSubcategory X P) : mk p.proj ⋯ ⋯ ≅ p

Reconstructing an object from its projection gives an isomorphic object.

Equations

• p.mkProjIso = TauCeti.CoveringSpace.FullSubcategory.isoMk (CategoryTheory.Iso.refl (TauCeti.CoveringSpace.FullSubcategory.mk p.proj ⋯ ⋯).obj.left) ⋯

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.mkProjIso_hom_hom_left {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} (p : FullSubcategory X P) : CategoryTheory.Over.Hom.left p.mkProjIso.hom.hom = CategoryTheory.eqToHom ⋯

@[simp]

theorem TauCeti.CoveringSpace.FullSubcategory.mkProjIso_inv_hom_left {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} (p : FullSubcategory X P) : CategoryTheory.Over.Hom.left p.mkProjIso.inv.hom = CategoryTheory.eqToHom ⋯

theorem TauCeti.CoveringSpace.FullSubcategory.isIso_iff_isHomeomorph_hom_left {X : TopCat} {P : CategoryTheory.ObjectProperty (CategoryTheory.Over X)} {p q : FullSubcategory X P} (f : p ⟶ q) : CategoryTheory.IsIso f ↔ IsHomeomorph ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left f.hom))

A morphism is an isomorphism exactly when its map of total spaces is a homeomorphism.

@[reducible, inline]

abbrev TauCeti.ConnectedCoveringSpace (X : TopCat) : Type (u + 1)

The category of connected covering spaces over X.

Equations

• TauCeti.ConnectedCoveringSpace X = TauCeti.CoveringSpace.FullSubcategory X fun (p : CategoryTheory.Over X) => ConnectedSpace ↑p.left

@[reducible, inline]

abbrev TauCeti.ConnectedCoveringSpace.forget (X : TopCat) : CategoryTheory.Functor (ConnectedCoveringSpace X) (CoveringSpace X)

The fully faithful inclusion of connected covering spaces into all covering spaces.

Equations

• TauCeti.ConnectedCoveringSpace.forget X = TauCeti.CoveringSpace.FullSubcategory.forget X fun (p : CategoryTheory.Over X) => ConnectedSpace ↑p.left

def TauCeti.ConnectedCoveringSpace.mk {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) [ConnectedSpace ↑E] : ConnectedCoveringSpace X

Construct a connected covering space from a covering map with connected total space.

Equations

• TauCeti.ConnectedCoveringSpace.mk p hp = TauCeti.CoveringSpace.FullSubcategory.mk p hp inst✝

@[simp]

theorem TauCeti.ConnectedCoveringSpace.mk_coe {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) [ConnectedSpace ↑E] : (mk p hp).obj.left = E

@[simp]

theorem TauCeti.ConnectedCoveringSpace.mk_proj {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) [ConnectedSpace ↑E] : CoveringSpace.FullSubcategory.proj (mk p hp) = p

@[simp]

theorem TauCeti.ConnectedCoveringSpace.forget_obj_mk {X E : TopCat} (p : E ⟶ X) (hp : IsCoveringMap ⇑(CategoryTheory.ConcreteCategory.hom p)) [ConnectedSpace ↑E] : (forget X).obj (mk p hp) = CoveringSpace.mk p hp

instance TauCeti.ConnectedCoveringSpace.connectedSpace {X : TopCat} (p : ConnectedCoveringSpace X) : ConnectedSpace ↑p.obj.left

The total space of a connected covering space is connected.