LeanPool.WhiteheadTheorem.Shapes.DiskHomeoCube

Imported Lean Pool material for LeanPool.WhiteheadTheorem.Shapes.DiskHomeoCube.

def TopCat.pDisk (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : TopCat

The unit disk in ℝⁿ based on the Lᵖ norm, where p ≥ 1.

Equations

• TopCat.pDisk n p = TopCat.of (ULift.{?u.1, 0} ↑(Metric.closedBall 0 1))

def TopCat.pDiskBoundary (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : TopCat

The boundary of the pDisk.

Equations

• TopCat.pDiskBoundary n p = TopCat.of (ULift.{?u.1, 0} ↑(Metric.sphere 0 1))

def TopCat.pDiskBoundaryIncl (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : pDiskBoundary n p ⟶ pDisk n p

The inclusion of the boundary of the pDisk.

Equations

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

instance TopCat.pDisk.instT1Space (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : T1Space ↑(pDisk n p)

instance TopCat.pDisk.boundaryInstT1Space (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : T1Space ↑(pDiskBoundary n p)

@[implicit_reducible]

noncomputable instance TopCat.pDisk.instPseudoMetricSpace (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : PseudoMetricSpace ↑(pDisk n p)

Equations

• TopCat.pDisk.instPseudoMetricSpace n p = inferInstance

@[implicit_reducible]

noncomputable instance TopCat.pDisk.boundaryInstPseudoMetricSpace (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : PseudoMetricSpace ↑(pDiskBoundary n p)

Equations

• TopCat.pDisk.boundaryInstPseudoMetricSpace n p = inferInstance

theorem TopCat.pDisk.dist_eq (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] (x y : ↑(pDisk n p)) : dist x y = dist ↑x.down ↑y.down

@[implicit_reducible]

instance TopCat.pDisk.instOfNatCarrierOfNatNat (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : OfNat (↑(pDisk n p)) 0

Use 0 to denote the center of the disk.

Equations

• TopCat.pDisk.instOfNatCarrierOfNatNat n p = { ofNat := { down := ⟨0, ⋯⟩ } }

theorem TopCat.pDisk.zero_eq (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] : 0 = ↑(ULift.down 0)

theorem TopCat.pDisk.eq_zero_iff (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] (x : ↑(pDisk n p)) : x = 0 ↔ ↑x.down = 0

noncomputable def TopCat.pDisk.toQDisk (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : ↑(pDisk n p) → ↑(pDisk n q)

Map x to (‖x‖_p / ‖x‖_q) • x. Note that division by zero evaluates to zero (see toQDisk_zero).

Equations

• TopCat.pDisk.toQDisk n p q { down := ⟨x_1, hx⟩ } = { down := ⟨(‖x_1‖ * ‖WithLp.toLp q x_1.ofLp‖⁻¹) • WithLp.toLp q x_1.ofLp, ⋯⟩ }

theorem TopCat.pDisk.toQDisk_zero (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : toQDisk n p q 0 = 0

pDisk.toQDisk maps 0 to 0. Note that division by zero evaluates to zero, due to GroupWithZero.inv_zero.

theorem TopCat.pDisk.toPDisk_comp_toQDisk (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] (x : ↑(pDisk n p)) : toQDisk n q p (toQDisk n p q x) = x

The map toQDisk has a left inverse.

theorem TopCat.pDisk.continuousAt_toQDisk_zero (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : ContinuousAt (toQDisk n p q) 0

The map toQDisk is continuous at 0.

theorem TopCat.pDisk.continuousOn_toQDisk_nonzero (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : ContinuousOn (toQDisk n p q) {x : ↑(pDisk n p) | x ≠ 0}

The map toQDisk is continuous on {x | x ≠ 0}.

theorem TopCat.pDisk.continuous_toQDisk (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : Continuous (toQDisk n p q)

The map toQDisk is continuous.

noncomputable def TopCat.pDisk.homeoQDisk (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : ↑(pDisk n p) ≃ₜ ↑(pDisk n q)

pDisk n p (the unit disk in ℝⁿ based on the Lᵖ norm) is homeomorphic to pDisk n q (the unit disk in ℝⁿ based on the L^q norm).

Equations

• TopCat.pDisk.homeoQDisk n p q = { toFun := TopCat.pDisk.toQDisk n p q, invFun := TopCat.pDisk.toQDisk n q p, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

noncomputable def TopCat.pDisk.isoQDisk (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : pDisk n p ≅ pDisk n q

isoQDisk

Equations

• TopCat.pDisk.isoQDisk n p q = TopCat.isoOfHomeo (TopCat.pDisk.homeoQDisk n p q)

instance TopCat.pDiskBoundary.instIsEmptyZero (p : ENNReal) [hp : Fact (1 ≤ p)] : IsEmpty ↑(pDiskBoundary 0 p)

theorem TopCat.pDiskBoundary.neq_zero (n : ℕ) (p : ENNReal) [hp : Fact (1 ≤ p)] (x : ↑(pDiskBoundary n p)) : ↑x.down ≠ 0

noncomputable def TopCat.pDiskBoundary.toQDiskBoundary (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : ↑(pDiskBoundary n p) → ↑(pDiskBoundary n q)

toQDiskBoundary

Equations

• TopCat.pDiskBoundary.toQDiskBoundary n p q { down := ⟨x_1, hx⟩ } = { down := ⟨(‖x_1‖ * ‖WithLp.toLp q x_1.ofLp‖⁻¹) • WithLp.toLp q x_1.ofLp, ⋯⟩ }

theorem TopCat.pDiskBoundary.toPDiskBoundary_comp_toQDiskBoundary (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] (x : ↑(pDiskBoundary n p)) : toQDiskBoundary n q p (toQDiskBoundary n p q x) = x

The map boundaryToQDiskBoundary has a left inverse.

theorem TopCat.pDiskBoundary.continuous_toQDiskBoundary (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : Continuous (toQDiskBoundary n p q)

The map boundaryToQDiskBoundary is continuous.

noncomputable def TopCat.pDiskBoundary.homeoQDiskBoundary (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : ↑(pDiskBoundary n p) ≃ₜ ↑(pDiskBoundary n q)

pDiskBounday n p is homeomorphic to pDiskBoundary n q.

Equations

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

noncomputable def TopCat.pDiskBoundary.isoQDiskBoundary (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : pDiskBoundary n p ≅ pDiskBoundary n q

isoQDiskBoundary

Equations

• TopCat.pDiskBoundary.isoQDiskBoundary n p q = TopCat.isoOfHomeo (TopCat.pDiskBoundary.homeoQDiskBoundary n p q)

noncomputable def TopCat.pDiskPair.homeoQDiskPair (n : ℕ) (p q : ENNReal) [hp : Fact (1 ≤ p)] [hq : Fact (1 ≤ q)] : CategoryTheory.Arrow.mk (pDiskBoundaryIncl n p) ≅ CategoryTheory.Arrow.mk (pDiskBoundaryIncl n q)

Homeomorphism from the pair (pDisk n p, pDiskBoundary n p) to the pair (pDisk n q, pDiskBoundary n q)

Equations

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

def TopCat.largeCubeHomeoPDisk (n : ℕ) : (Fin n → ↑(Set.Icc (-1) 1)) ≃ₜ ↑(pDisk n ⊤)

The large cube $[-1, 1]^n$ is homeomorphic to pDisk n ∞ (the disk in ℝⁿ according to the L∞ norm).

Equations

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

noncomputable def TopCat.largeCubeHomeoCube (n : ℕ) : (Fin n → ↑(Set.Icc (-1) 1)) ≃ₜ (Fin n → ↑unitInterval)

The large cube $[-1, 1]^n$ is homeomorphic to the cube $[0, 1]^n$.

Equations

• TopCat.largeCubeHomeoCube n = Homeomorph.piCongrRight fun (x : Fin n) => iccHomeoI (-1) 1 TopCat.largeCubeHomeoCube._proof_1

noncomputable def TopCat.diskHomeoCube (n : ℕ) : ↑(disk n) ≃ₜ (Fin n → ↑unitInterval)

The n-disk 𝔻 n is homeomorphic to the cube $[0, 1]^n$.

Equations

• TopCat.diskHomeoCube n = (TopCat.pDisk.homeoQDisk n 2 ⊤).trans ((TopCat.largeCubeHomeoPDisk n).symm.trans (TopCat.largeCubeHomeoCube n))

noncomputable def TopCat.largeCubeBoundaryHomeoPDiskBoundary (n : ℕ) : ↑{x : Fin n → ↑(Set.Icc (-1) 1) | ∃ (i : Fin n), ↑(x i) = -1 ∨ ↑(x i) = 1} ≃ₜ ↑(pDiskBoundary n ⊤)

largeCubeBoundaryHomeoPDiskBoundary

Equations

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

noncomputable def TopCat.largeCubeBoundaryHomeoCubeBoundary (n : ℕ) : ↑{x : Fin n → ↑(Set.Icc (-1) 1) | ∃ (i : Fin n), ↑(x i) = -1 ∨ ↑(x i) = 1} ≃ₜ ↑(Cube.boundary (Fin n))

largeCubeBoundaryHomeoCubeBoundary

Equations

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

noncomputable def TopCat.diskBoundaryHomeoCubeBoundary (n : ℕ) : ↑(diskBoundary n) ≃ₜ ↑(Cube.boundary (Fin n))

diskBoundaryHomeoCubeBoundary

Equations

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

noncomputable def TopCat.diskIsoCube (n : ℕ) : disk n ≅ of (Fin n → ↑unitInterval)

diskIsoCube

Equations

• TopCat.diskIsoCube n = TopCat.isoOfHomeo (TopCat.diskHomeoCube n)

noncomputable def TopCat.diskBoundaryIsoCubeBoundary (n : ℕ) : diskBoundary n ≅ of ↑(Cube.boundary (Fin n))

diskBoundaryIsoCubeBoundary

Equations

• TopCat.diskBoundaryIsoCubeBoundary n = TopCat.isoOfHomeo (TopCat.diskBoundaryHomeoCubeBoundary n)

noncomputable def TopCat.diskPair.homeoCubePair (n : ℕ) : CategoryTheory.Arrow.mk (diskBoundaryIncl n) ≅ CategoryTheory.Arrow.mk (ofHom (Cube.boundaryIncl n))

homeoCubePair

Equations

• TopCat.diskPair.homeoCubePair n = CategoryTheory.Arrow.isoMk' (TopCat.diskBoundaryIncl n) (TopCat.ofHom (Cube.boundaryIncl n)) (TopCat.diskBoundaryIsoCubeBoundary n) (TopCat.diskIsoCube n) ⋯

theorem TopCat.diskPair.homeoCubePair_comm (n : ℕ) : CategoryTheory.CategoryStruct.comp (diskBoundaryIncl n) (CategoryTheory.Arrow.Hom.right (homeoCubePair n).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left (homeoCubePair n).hom) (ofHom (Cube.boundaryIncl n))

noncomputable def TopCat.diskHomeoCubeULift (n : ℕ) : ↑(disk n) ≃ₜ ↑(cube n)

diskHomeoCubeULift

Equations

• TopCat.diskHomeoCubeULift n = (TopCat.diskHomeoCube n).trans Homeomorph.ulift.symm

noncomputable def TopCat.diskIsoCubeULift (n : ℕ) : disk n ≅ cube n

diskIsoCubeULift

Equations

• TopCat.diskIsoCubeULift n = TopCat.isoOfHomeo (TopCat.diskHomeoCubeULift n)

noncomputable def TopCat.diskBoundaryHomeoCubeBoundaryULift (n : ℕ) : ↑(diskBoundary n) ≃ₜ ↑(cubeBoundary n)

diskBoundaryHomeoCubeBoundaryULift

Equations

• TopCat.diskBoundaryHomeoCubeBoundaryULift n = (TopCat.diskBoundaryHomeoCubeBoundary n).trans Homeomorph.ulift.symm

noncomputable def TopCat.diskBoundaryIsoCubeBoundaryULift (n : ℕ) : diskBoundary n ≅ cubeBoundary n

diskBoundaryIsoCubeBoundaryULift

Equations

• TopCat.diskBoundaryIsoCubeBoundaryULift n = TopCat.isoOfHomeo (TopCat.diskBoundaryHomeoCubeBoundaryULift n)

noncomputable def TopCat.diskPair.homeoCubePairULift (n : ℕ) : CategoryTheory.Arrow.mk (diskBoundaryIncl n) ≅ CategoryTheory.Arrow.mk (cubeBoundaryIncl n)

Homeomorphism from the pair (TopCat.disk.{u} n, TopCat.diskBoundary.{u} n) to the pair (TopCat.cube.{u} n, TopCat.cubeBoundary.{u} n)

Equations

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

theorem TopCat.diskPair.homeoCubePairULift_comm (n : ℕ) : CategoryTheory.CategoryStruct.comp (diskBoundaryIncl n) (CategoryTheory.Arrow.Hom.right (homeoCubePairULift n).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left (homeoCubePairULift n).hom) (cubeBoundaryIncl n)