The open unit square

The open unit square Ioo 0 1 ×ˢ Ioo 0 1 in I × I is the interior of a 2-cell whose characteristic map is defined on the square I × I. This file records its two basic homotopical properties: it is simply connected, and it stays path connected when one point is removed.

Both are transported from the open square in ℝ × ℝ along the inclusion I × I → ℝ × ℝ. That square is convex, hence contractible; with one point removed it deforms onto a small sphere about the point (StarConvex.sphereHomotopyEquiv), which is path connected.

The square with its centre removed deforms onto its boundary, radially from the centre (unitInterval.radialPush). In the sup norm of ℝ × ℝ the boundary of the square is the sphere of radius 1 / 2 about the centre, so this is the radial deformation StarConvex.radialHomotopy of a punctured star-convex set onto a sphere. It is the deformation that pushes a space with 2-cells attached, minus one point in each open cell, back onto the space the cells are attached to.

Main definitions

• unitInterval.squareCentre: the centre of the unit square.
• unitInterval.radialPush: the radial deformation of the punctured square onto its boundary.

Main results

• unitInterval.notMem_Ioo_prod_Ioo_iff: the boundary of the square is the union of its four edges.
• unitInterval.image_prodMap_val_Ioo_prod_Ioo: the inclusion I × I → ℝ × ℝ carries the open unit square onto the open unit square.
• unitInterval.isSimplyConnected_Ioo_prod_Ioo: the open unit square is simply connected.
• unitInterval.isPathConnected_Ioo_prod_Ioo_diff_singleton: the open unit square with one point removed is path connected.
• unitInterval.radialPush_zero, unitInterval.radialPush_of_notMem, unitInterval.radialPush_one_notMem, unitInterval.continuousAt_radialPush: the radial deformation starts at the identity, fixes the boundary, ends on the boundary, and is continuous away from the centre. It also fixes the centre (unitInterval.radialPush_squareCentre).

theorem unitInterval.notMem_Ioo_prod_Ioo_iff {q : ↑unitInterval × ↑unitInterval} : q ∉ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 ↔ q.1 = 0 ∨ q.1 = 1 ∨ q.2 = 0 ∨ q.2 = 1

A point of the unit square outside the open square lies on one of its four edges.

theorem unitInterval.image_prodMap_val_Ioo_prod_Ioo : Prod.map Subtype.val Subtype.val '' Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 = Set.Ioo 0 1 ×ˢ Set.Ioo 0 1

The inclusion I × I → ℝ × ℝ carries the open unit square onto the open unit square.

theorem unitInterval.isSimplyConnected_Ioo_prod_Ioo : IsSimplyConnected (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1)

The open unit square is simply connected.

theorem unitInterval.isPathConnected_Ioo_prod_Ioo_diff_singleton {p : ↑unitInterval × ↑unitInterval} (hp : p ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) : IsPathConnected (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1 \ {p})

The open unit square with one point removed is path connected. In ℝ × ℝ it is a convex set punctured at p, which deforms onto a small sphere about p (StarConvex.sphereHomotopyEquiv), and that sphere is path connected.

The radial deformation of the punctured square onto its boundary

In ℝ × ℝ, whose norm is the sup norm, the sphere of radius 1 / 2 about the centre of the unit square is the boundary of the square. So the radial deformation of the punctured square onto its boundary is the radial deformation StarConvex.radialHomotopy of a punctured star-convex set onto a sphere about the puncture, read through the inclusion I × I → ℝ × ℝ.

noncomputable def unitInterval.squareCentre : ↑unitInterval × ↑unitInterval

The centre (1 / 2, 1 / 2) of the unit square.

@[simp]

theorem unitInterval.coe_squareCentre_fst : ↑squareCentre.1 = 1 / 2

@[simp]

theorem unitInterval.coe_squareCentre_snd : ↑squareCentre.2 = 1 / 2

theorem unitInterval.squareCentre_mem_Ioo_prod_Ioo : squareCentre ∈ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1

noncomputable def unitInterval.radialPush (t : ↑unitInterval) (q : ↑unitInterval × ↑unitInterval) : ↑unitInterval × ↑unitInterval

The radial deformation of the unit square with its centre removed onto its boundary, at time t: a point q other than the centre moves along the ray from the centre through q, from q at time 0 to the boundary of the square at time 1, and points of the boundary do not move. It is StarConvex.radialHomotopy run backwards, for the sup norm on ℝ × ℝ. The centre itself, where the deformation is not continuous, is sent to itself.

@[simp]

theorem unitInterval.radialPush_zero (q : ↑unitInterval × ↑unitInterval) : radialPush 0 q = q

At time 0 the radial deformation is the identity.

@[simp]

theorem unitInterval.radialPush_squareCentre (t : ↑unitInterval) : radialPush t squareCentre = squareCentre

The radial deformation fixes the centre of the square.

@[simp]

theorem unitInterval.radialPush_of_notMem {q : ↑unitInterval × ↑unitInterval} (hq : q ∉ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1) (t : ↑unitInterval) : radialPush t q = q

The radial deformation fixes the boundary of the square.

theorem unitInterval.radialPush_one_notMem {q : ↑unitInterval × ↑unitInterval} (hq : q ≠ squareCentre) : radialPush 1 q ∉ Set.Ioo 0 1 ×ˢ Set.Ioo 0 1

At time 1 the radial deformation sends every point other than the centre to the boundary of the square.

theorem unitInterval.continuousAt_radialPush {t : ↑unitInterval} {q : ↑unitInterval × ↑unitInterval} (hq : q ≠ squareCentre) : ContinuousAt (fun (p : ↑unitInterval × ↑unitInterval × ↑unitInterval) => radialPush p.1 p.2) (t, q)

The radial deformation is continuous in the time and the point away from the centre.