Universal covers

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremEvery pointed connected cover of `(X, x₀)` is realised by exactly one subgroup of `π₁(X, x₀)`#

The subgroups of π₁(X, x₀) therefore parametrise the pointed connected covers of (X, x₀) bijectively, up to isomorphism over X respecting the chosen lifts.

TauCeti.UniversalCover.existsUnique_subgroup_homeomorph_subgroupQuotient.{u_1, u_2} {X : Type u_1}
  [TopologicalSpace X] [LocallyPathConnectedSpace X] [TauCeti.SemilocallySimplyConnectedSpace X]
  (x₀ : X) {E : Type u_2} [TopologicalSpace E] [PathConnectedSpace E] {p : E → X}
  (hp : IsCoveringMap p) {e₀ : E} (hpe : p e₀ = x₀) :
  ∃! H,
    ∃ h,
      h e₀ = TauCeti.UniversalCover.SubgroupQuotient.basepoint x₀ H ∧
        TauCeti.UniversalCover.subgroupQuotientProj x₀ H ∘ ⇑h = p

Lean

Formalized in Tau Ceti as TauCeti.UniversalCover.existsUnique_subgroup_homeomorph_subgroupQuotient.

Sources

LeanTauCeti.UniversalCover.existsUnique_subgroup_homeomorph_subgroupQuotient

DefinitionThe classification of covering spaces by fundamental-groupoid actions #

Over a path-connected, locally path-connected, semilocally simply connected base, monodromy is an equivalence from covering spaces to functors from the fundamental groupoid to types.

TauCeti.CoveringSpace.monodromyEquivalence.{u} (X : TopCat) [PathConnectedSpace ↑X]
  [LocallyPathConnectedSpace ↑X] [TauCeti.SemilocallySimplyConnectedSpace ↑X] :
  TauCeti.CoveringSpace X ≌ CategoryTheory.Functor (FundamentalGroupoid ↑X) (Type u)

Lean

Formalized in Tau Ceti as TauCeti.CoveringSpace.monodromyEquivalence.

Sources

LeanTauCeti.CoveringSpace.monodromyEquivalence

Uses 2

Statement usesTauCeti.CoveringSpace

Proof usesTauCeti.CoveringSpace.mk

DefinitionThe fundamental group of `X` at `x₀` is the automorphism group of the fibre functor over `x₀`#

A loop class is sent to the natural automorphism acting on every fibre by monodromy; that this is a bijection onto all natural automorphisms is Tannaka duality for π₁(X, x₀)-sets, transported along the classification of covering spaces by π₁(X, x₀)-sets.

TauCeti.CoveringSpace.autFiberFunctorMulEquiv.{u} {X : TopCat} (x₀ : ↑X) [PathConnectedSpace ↑X]
  [LocallyPathConnectedSpace ↑X] [TauCeti.SemilocallySimplyConnectedSpace ↑X] :
  FundamentalGroup (↑X) x₀ ≃* CategoryTheory.Aut (TauCeti.CoveringSpace.fiberFunctor x₀)

Lean

Formalized in Tau Ceti as TauCeti.CoveringSpace.autFiberFunctorMulEquiv.

Sources

LeanTauCeti.CoveringSpace.autFiberFunctorMulEquiv

Uses 2

Statement usesTauCeti.CoveringSpace

Proof usesTauCeti.CoveringSpace.mk

DefinitionThe profinite completion of `π₁(X, x₀)` is the automorphism group of the finite-cover fibre functor #

TauCeti.FiniteCoveringSpace.profiniteCompletionAutFiberFunctorMulEquiv.{u} {X : TopCat} (x₀ : ↑X)
  [PathConnectedSpace ↑X] [LocallyPathConnectedSpace ↑X]
  [TauCeti.SemilocallySimplyConnectedSpace ↑X] :
  ↑(ProfiniteGrp.ProfiniteCompletion.completion ↧(FundamentalGroup (↑X) x₀)).toProfinite.toTop ≃*
    CategoryTheory.Aut (TauCeti.FiniteCoveringSpace.fiberFunctor x₀)

Lean

Formalized in Tau Ceti as TauCeti.FiniteCoveringSpace.profiniteCompletionAutFiberFunctorMulEquiv.

Sources

LeanTauCeti.FiniteCoveringSpace.profiniteCompletionAutFiberFunctorMulEquiv

Uses 2

Statement usesTauCeti.CoveringSpace

Proof usesTauCeti.CoveringSpace.mk

TheoremA path-connected, locally path-connected space is semilocally simply connected if and only if it admits a simply connected covering space #

The forward direction is the universal-cover construction, the reverse direction is TauCeti.SemilocallySimplyConnectedSpace.of_isCoveringMap; surjectivity of the covering map is automatic here, by IsCoveringMap.comp_subtypeVal_pathComponent_surjective, because the base is path-connected and a simply connected total space is nonempty.

TauCeti.semilocallySimplyConnectedSpace_iff_exists_isCoveringMap_and_simplyConnectedSpace.{u}
  (X : Type u) [TopologicalSpace X] [PathConnectedSpace X] [LocallyPathConnectedSpace X] :
  TauCeti.SemilocallySimplyConnectedSpace X ↔ ∃ E x p, IsCoveringMap p ∧ SimplyConnectedSpace E

Lean

Formalized in Tau Ceti as TauCeti.semilocallySimplyConnectedSpace_iff_exists_isCoveringMap_and_simplyConnectedSpace.

Sources

LeanTauCeti.semilocallySimplyConnectedSpace_iff_exists_isCoveringMap_and_simplyConnectedSpace

DefinitionThe fundamental group of real projective space `RPⁿ` (for `2 ≤ n`) is isomorphic to `ℤˣ` for any basepoint `x`#

FundamentalGroup (RealProjectiveSpace n) x ≃* ℤˣ.

TauCeti.RealProjectiveSpace.fundamentalGroupMulEquivAt (n : ℕ) (hn : 2 ≤ n)
  (x : TauCeti.RealProjectiveSpace n) : FundamentalGroup (TauCeti.RealProjectiveSpace n) x ≃* ℤˣ

Lean

Formalized in Tau Ceti as TauCeti.RealProjectiveSpace.fundamentalGroupMulEquivAt.

Sources

LeanTauCeti.RealProjectiveSpace.fundamentalGroupMulEquivAt

Uses 1

Proof usesTauCeti.simplyConnectedSpace_sphere

TheoremTauCeti.simplyConnectedSpace_sphere #

Every sphere of nonnegative radius in a real normed space of rank greater than two is simply connected.

TauCeti.simplyConnectedSpace_sphere.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  (h : 2 < Module.rank ℝ E) (c : E) {r : ℝ} (hr : 0 ≤ r) : SimplyConnectedSpace ↑(Metric.sphere c r)

Lean

Formalized in Tau Ceti as TauCeti.simplyConnectedSpace_sphere.

Sources

LeanTauCeti.simplyConnectedSpace_sphere

Used by 1

Used byThe fundamental group of real projective space RPⁿ (for 2 ≤ n) is isomorphic to ℤˣ for any basepoint x

AbbreviationTauCeti.CoveringSpace #

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.

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

Lean

Formalized in Tau Ceti as TauCeti.CoveringSpace.

Sources

LeanTauCeti.CoveringSpace

Used by 7

Used byAnalytic Belyi pairs are classified by finite covers of the thrice-punctured sphere · Connected covers of ℂ ∖ {0, 1} of degree n up to isomorphism are classified by the isomorphism classes of connected triples of degree n · The superelliptic curve is the analytic Belyi pair of the torus triple · TauCeti.CoveringSpace.mk · The classification of covering spaces by fundamental-groupoid actions · The fundamental group of X at x₀ is the automorphism group of the fibre functor over x₀ · The profinite completion of π₁(X, x₀) is the automorphism group of the finite-cover fibre functor

DefinitionTauCeti.CoveringSpace.mk #

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.

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

Lean

Formalized in Tau Ceti as TauCeti.CoveringSpace.mk.

Sources

LeanTauCeti.CoveringSpace.mk

Uses 1 · Used by 3

Statement usesTauCeti.CoveringSpace

Used byThe classification of covering spaces by fundamental-groupoid actions · The fundamental group of X at x₀ is the automorphism group of the fibre functor over x₀ · The profinite completion of π₁(X, x₀) is the automorphism group of the finite-cover fibre functor

InstanceThe fundamental group at `x` acts on every homotopy group based at `x`#

The fundamental group at x acts on every homotopy group based at x, an element of π₁(X, x) acting by transport around the loop it represents.

The action is a left action: transport composes covariantly and FundamentalGroup.mul_def reverses the order of concatenation, so the two reversals cancel.

TauCeti.homotopyGroupMulAction.{u_1, u_2} {N : Type u_1} [Fintype N] {X : Type u_2}
  [TopologicalSpace X] {x : X} : MulAction (FundamentalGroup X x) (HomotopyGroup N X x)

Lean

Formalized in Tau Ceti as TauCeti.homotopyGroupMulAction.

Sources

LeanTauCeti.homotopyGroupMulAction

Used by 4

Used byEvery group has a K(G, 1) · The cellular and the simplicial classifying spaces agree · The singular cohomology of the classifying space is group cohomology · The singular homology of the classifying space is group homology

TheoremAddCircle.fundamentalGroupMulEquiv_eq_windingNumberIso #

For positive periods, the chosen-lift equivalence agrees with Mathlib's winding-number isomorphism. In particular it is independent of the chosen lift and has the same orientation.

AddCircle.fundamentalGroupMulEquiv_eq_windingNumberIso (p : ℝ) [hp : Fact (0 < p)] {x : AddCircle p}
  (e : ↑(QuotientAddGroup.mk ⁻¹' {x})) :
  AddCircle.fundamentalGroupMulEquiv p ⋯ e = x.windingNumberIso

Lean

Formalized in Tau Ceti as AddCircle.fundamentalGroupMulEquiv_eq_windingNumberIso.

Sources

LeanAddCircle.fundamentalGroupMulEquiv_eq_windingNumberIso

Used by 1

Used byThe isomorphism π₁(S¹) ≃* ℤ is the degree

TheoremThe isomorphism `π₁(S¹) ≃* ℤ` is the degree #

The class of a loop is sent to its degree Circle.degree, the number of full turns of any continuous angle lift.

Circle.fundamentalGroupMulEquiv_fromPath {x : Circle} (γ : Path x x) :
  x.fundamentalGroupMulEquiv (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)) =
    Multiplicative.ofAdd (Circle.degree γ)

Lean

Formalized in Tau Ceti as Circle.fundamentalGroupMulEquiv_fromPath.

Sources

LeanCircle.fundamentalGroupMulEquiv_fromPath

Uses 1 · Used by 11

Proof usesAddCircle.fundamentalGroupMulEquiv_eq_windingNumberIso

Used byAnalytic Belyi pairs are classified by finite covers of the thrice-punctured sphere · Connected covers of ℂ ∖ {0, 1} of degree n up to isomorphism are classified by the isomorphism classes of connected triples of degree n · The Riemann–Hurwitz formula for a filled cover · The superelliptic curve is the analytic Belyi pair of the torus triple · The cellular and the simplicial classifying spaces agree · Uniqueness of aspherical spaces of CW type · Analytic delineability from constant discriminant order · Correctness of McCallum's projection · Lazard lifting of a family · Recursive sign-invariant McCallum correctness · Sign-invariance of the McCallum projection does not suffice for lifting

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Universal covers

TheoremEvery pointed connected cover of (X, x₀) is realised by exactly one subgroup of π₁(X, x₀)#

Lean

Sources

DefinitionThe classification of covering spaces by fundamental-groupoid actions#

Lean

Sources

DefinitionThe fundamental group of X at x₀ is the automorphism group of the fibre functor over x₀#

Lean

Sources

DefinitionThe profinite completion of π₁(X, x₀) is the automorphism group of the finite-cover fibre functor#

Lean

Sources

TheoremA path-connected, locally path-connected space is semilocally simply connected if and only if it admits a simply connected covering space#

Lean

Sources

DefinitionThe fundamental group of real projective space RPⁿ (for 2 ≤ n) is isomorphic to ℤˣ for any basepoint x#

Lean

Sources

TheoremTauCeti.simplyConnectedSpace_sphere#

Lean

Sources

AbbreviationTauCeti.CoveringSpace#

Lean

Sources

DefinitionTauCeti.CoveringSpace.mk#

Lean

Sources

InstanceThe fundamental group at x acts on every homotopy group based at x#

Lean

Sources

TheoremAddCircle.fundamentalGroupMulEquiv_eq_windingNumberIso#

Lean

Sources

TheoremThe isomorphism π₁(S¹) ≃* ℤ is the degree#

Lean

Sources

TheoremEvery pointed connected cover of `(X, x₀)` is realised by exactly one subgroup of `π₁(X, x₀)`#

DefinitionThe classification of covering spaces by fundamental-groupoid actions #

DefinitionThe fundamental group of `X` at `x₀` is the automorphism group of the fibre functor over `x₀`#

DefinitionThe profinite completion of `π₁(X, x₀)` is the automorphism group of the finite-cover fibre functor #

TheoremA path-connected, locally path-connected space is semilocally simply connected if and only if it admits a simply connected covering space #

DefinitionThe fundamental group of real projective space `RPⁿ` (for `2 ≤ n`) is isomorphic to `ℤˣ` for any basepoint `x`#

TheoremTauCeti.simplyConnectedSpace_sphere #

AbbreviationTauCeti.CoveringSpace #

DefinitionTauCeti.CoveringSpace.mk #

InstanceThe fundamental group at `x` acts on every homotopy group based at `x`#

TheoremAddCircle.fundamentalGroupMulEquiv_eq_windingNumberIso #

TheoremThe isomorphism `π₁(S¹) ≃* ℤ` is the degree #