Documentation

TauCeti.AlgebraicTopology.Disk

Euclidean disks and their boundaries #

The closed Euclidean disk is contractible, and its boundary is path-connected when the disk has dimension at least two. This module also constructs the standard TopPair consisting of a disk and its boundary, providing the topological input for relative-homology calculations.

Mathlib's TopCat.diskBoundary n is the universe lift of the unit sphere of EuclideanSpace ℝ (Fin n). It is homeomorphic to the unit sphere of the Euclidean space EuclideanSpace ℝ (ULift (Fin n)) of the same dimension in the lifted universe (TauCeti.diskBoundaryHomeomorph), which lets results about unit spheres of inner product spaces in that universe be applied to it. In particular the boundary of the 0-disk is empty.

source
instance TauCeti.TopCat.contractibleSpace_disk (n : ℕ) :
ContractibleSpace ↑(TopCat.disk n)

The n-dimensional Euclidean disk is contractible.

source
theorem TauCeti.TopCat.pathConnectedSpace_diskBoundary {n : ℕ} (hn : 2 ≤ n) :
PathConnectedSpace ↑(TopCat.diskBoundary n)

The boundary of the n-dimensional disk is path-connected when n ≥ 2.

source
@[reducible, inline]
noncomputable abbrev TauCeti.diskBoundaryPair (n : ℕ) :
TopPair

The standard pair consisting of the n-dimensional disk and its boundary, used to express relative singular homology of the disk with respect to its boundary.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.diskBoundaryPair_fst (n : ℕ) :
    TopPair.fst = TopCat.disk n
    source
    @[simp]
    theorem TauCeti.diskBoundaryPair_snd (n : ℕ) :
    TopPair.snd = TopCat.diskBoundary n
    source
    theorem TauCeti.diskBoundaryPair_map (n : ℕ) :
    TopPair.map = TopCat.diskBoundaryInclusion n

    The underlying map of diskBoundaryPair n is the standard boundary inclusion.

    source
    instance TauCeti.contractibleSpace_diskBoundaryPair_fst (n : ℕ) :
    ContractibleSpace ↑TopPair.fst

    The ambient space of the pair consisting of a disk and its boundary is contractible. This lets instances about pairs with contractible ambient space apply to diskBoundaryPair n.

    source
    noncomputable def TauCeti.diskBoundaryHomeomorph (n : ℕ) :
    ↑(TopCat.diskBoundary n) ≃ₜ ↑(Metric.sphere 0 1)

    Mathlib's boundary TopCat.diskBoundary n of the n-disk, the universe lift of the unit sphere of EuclideanSpace ℝ (Fin n), is homeomorphic to the unit sphere of the Euclidean space EuclideanSpace ℝ (ULift (Fin n)) of the same dimension in the lifted universe.

    Equations
    Instances For
      source
      theorem TauCeti.finrank_euclideanSpace_ulift_fin (n : ℕ) :
      Module.finrank ℝ (EuclideanSpace ℝ (ULift.{u, 0} (Fin n))) = n

      The dimension of the Euclidean space EuclideanSpace ℝ (ULift (Fin n)).

      source
      instance TauCeti.isEmpty_diskBoundary_zero :
      IsEmpty ↑(TopCat.diskBoundary 0)

      The boundary of the 0-disk is empty.

      source
      instance TauCeti.isEmpty_diskBoundaryPair_zero_snd :
      IsEmpty ↑TopPair.snd

      The subspace of the pair consisting of the 0-disk and its boundary is empty. This lets instances about pairs with empty subspace apply to diskBoundaryPair 0.