Source topology and simple connectedness of the lifted group

This file begins the topological half of the universal-cover theorem. The group-theoretic half is in UniversalCover/Fibre.lean and UniversalCover/Surjectivity.lean.

The useful coordinates do not require a computation of π₁(S¹). If x = (T, f) : GLTilde, rotate the first column of T backwards through the lifted angle f(0). Compatibility says that the resulting matrix has the form

  !![r, b; 0, d]     with r > 0 and d > 0.

Conversely, an angle and such an upper-triangular matrix determine a unique compatible lift. Thus GLTilde has global coordinates

  ℝ × (0, ∞) × ℝ × (0, ∞),

which are contractible. We transport the product topology through this coordinate equivalence and obtain ContractibleSpace GLTilde, hence SimplyConnectedSpace GLTilde.

UniversalCover/Map.lean continues from these coordinates, gives global circle coordinates on GL⁺(2, ℝ), and proves that the matrix projection is a covering map. UniversalCover/TopologicalGroup.lean then proves that multiplication and inversion are continuous for the transported topology.

Rotations and lifted rotations

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rotationMatrix (θ : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

Counterclockwise rotation through angle π θ.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rotationMatrix_det (θ : ℝ) : (rotationMatrix θ).det = 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rotationMatrix_mulVec_rayVec (θ φ : ℝ) : (rotationMatrix θ).mulVec (rayVec φ) = rayVec (φ + θ)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rotationMatrix_neg_mul (θ : ℝ) : rotationMatrix (-θ) * rotationMatrix θ = 1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rotationMatrix_mul_neg (θ : ℝ) : rotationMatrix θ * rotationMatrix (-θ) = 1

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rotationGLPos (θ : ℝ) : ↥(Matrix.GLPos (Fin 2) ℝ)

Rotation as an element of GL⁺(2, ℝ).

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rotationGLPos_mat (θ : ℝ) : toMat (rotationGLPos θ) = rotationMatrix θ

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.phaseTranslation (θ : ℝ) : NormalizedShift

Translation of the phase line through θ.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.phaseTranslation θ = { toOrderIso := OrderIso.addRight θ, map_add_one := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.phaseTranslation_apply (θ φ : ℝ) : (phaseTranslation θ).toOrderIso φ = φ + θ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.compatible_rotation (θ : ℝ) : Compatible (rotationGLPos θ) (phaseTranslation θ)

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation (θ : ℝ) : GLTilde

Rotation together with its tautological lift to the phase line.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation_mat (θ : ℝ) : (liftedRotation θ).mat = rotationGLPos θ

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.liftedRotation_shift_zero (θ : ℝ) : (liftedRotation θ).shift.toOrderIso 0 = θ

A lift is determined by its matrix and one lifted phase

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.ext_mat_shift_zero {x y : GLTilde} (hmat : x.mat = y.mat) (hzero : x.shift.toOrderIso 0 = y.shift.toOrderIso 0) : x = y

Two compatible lifts of the same matrix agreeing at phase zero are equal.

The unique deck-factorisation reduces this to injectivity of ℤ → ℝ.

Upper-triangular representatives

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.PositiveReal : Set ℝ

Positive real numbers, with their standard subspace topology.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.PositiveReal = Set.Ioi 0

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTildeCoordinates : Type

Global coordinates for GLTilde: angle, first diagonal, shear, second diagonal.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperMatrix (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : Matrix (Fin 2) (Fin 2) ℝ

The upper-triangular matrix represented by the last three coordinates.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperMatrix r b d = !![↑r, b; 0, ↑d]

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperMatrix_det (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : (upperMatrix r b d).det = ↑r * ↑d

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperMatrixInv (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : Matrix (Fin 2) (Fin 2) ℝ

The explicit inverse of upperMatrix.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperMatrixInv r b d = !![(↑r)⁻¹, -((↑r)⁻¹ * b * (↑d)⁻¹); 0, (↑d)⁻¹]

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperMatrix_mul_inv (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : upperMatrix r b d * upperMatrixInv r b d = 1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperMatrix_inv_mul (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : upperMatrixInv r b d * upperMatrix r b d = 1

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperGLPos (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : ↥(Matrix.GLPos (Fin 2) ℝ)

A positive-diagonal upper-triangular matrix as an element of GL⁺(2, ℝ).

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperGLPos_mat (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : toMat (upperGLPos r b d) = upperMatrix r b d

Extracting coordinates

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.alignedMatrix (x : GLTilde) : Matrix (Fin 2) (Fin 2) ℝ

Rotate the first column of x.mat back through its lifted phase at zero.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.alignedMatrix_zero_zero_pos (x : GLTilde) : 0 < alignedMatrix x 0 0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.alignedMatrix_one_zero (x : GLTilde) : alignedMatrix x 1 0 = 0

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.alignedMatrix_one_one_pos (x : GLTilde) : 0 < alignedMatrix x 1 1

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeCoordinates (x : GLTilde) : GLTildeCoordinates

The global coordinate map.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.matrixOfCoordinates (c : GLTildeCoordinates) : Matrix (Fin 2) (Fin 2) ℝ

Rebuild the underlying matrix from the four coordinates.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.matrixOfCoordinates_apply (x : GLTilde) : matrixOfCoordinates (glTildeCoordinates x) = toMat x.mat

Reconstructing a lift from coordinates

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperDeckIndex (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : ℤ

The deck displacement of the canonical upper-triangular lift.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperDeckIndex r b d = Classical.choose ⋯

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperDeckIndex_spec (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : lift (upperGLPos r b d) 0 = 2 * ↑(upperDeckIndex r b d)

The chosen deck index removes exactly the value at zero of the canonical upper-triangular lift.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperSectionZero (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : GLTilde

The compatible lift of an upper-triangular matrix normalized to take 0 to 0.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperSectionZero_mat (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : (upperSectionZero r b d).mat = upperGLPos r b d

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperSectionZero_shift_zero (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) : (upperSectionZero r b d).shift.toOrderIso 0 = 0

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeOfCoordinates (c : GLTildeCoordinates) : GLTilde

Reconstruct a compatible lift from its four global coordinates.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeOfCoordinates_shift_zero (c : GLTildeCoordinates) : (glTildeOfCoordinates c).shift.toOrderIso 0 = c.1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeOfCoordinates_mat (c : GLTildeCoordinates) : toMat (glTildeOfCoordinates c).mat = matrixOfCoordinates c

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.alignedMatrix_glTildeOfCoordinates (c : GLTildeCoordinates) : alignedMatrix (glTildeOfCoordinates c) = upperMatrix c.2.1 c.2.2.1 c.2.2.2

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeCoordinates_ofCoordinates (c : GLTildeCoordinates) : glTildeCoordinates (glTildeOfCoordinates c) = c

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeCoordinates_injective : Function.Injective glTildeCoordinates

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeCoordinates_surjective : Function.Surjective glTildeCoordinates

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeCoordinateEquiv : GLTilde ≃ GLTildeCoordinates

The global coordinate equivalence for GLTilde.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeCoordinateEquiv_apply (x : GLTilde) : glTildeCoordinateEquiv x = glTildeCoordinates x

Topology and simple connectedness

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.topologicalSpace : TopologicalSpace GLTilde

The topology transported from ℝ × (0,∞) × ℝ × (0,∞) by the global coordinate equivalence.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeCoordinateHomeomorph : GLTilde ≃ₜ GLTildeCoordinates

The global coordinates as a homeomorphism.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.continuous_rotationMatrix : Continuous rotationMatrix

Rotation matrices depend continuously on their lifted angle.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeOfCoordinates_coordinates (x : GLTilde) : glTildeOfCoordinates (glTildeCoordinates x) = x

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.continuous_toMat : Continuous mat

The matrix projection is continuous for the global-coordinate topology.

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.contractibleSpace : ContractibleSpace GLTilde

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.simplyConnectedSpace : SimplyConnectedSpace GLTilde

The space underlying Bridgeland's pair presentation is simply connected.

This proves the formerly missing simple-connectedness fact. The covering-map theorem is proved separately in UniversalCover/Map.lean.