The lifted group as a covering of the positive general linear group

This file completes the topological part of the universal-cover construction. The base has coordinates

  S¹ × (0, ∞) × ℝ × (0, ∞),

obtained from the direction and length of the first column, followed by the coordinates of the second column in the resulting oriented orthonormal frame. In these coordinates the matrix projection is the product of

  θ ↦ exp(π θ) : ℝ → S¹

with the identity on the remaining three coordinates. The first map is the standard exponential covering; the product and coordinate homeomorphisms therefore give the required covering map.

UniversalCover/TopologicalGroup.lean supplies the final compatibility layer by proving that the transported topology makes GLTilde a topological group.

The product-of-a-covering-with-an-identity step is the general lemma isCoveringMap_prodMap_id, which quantifies over arbitrary spaces and lives with the topology owner in Topology/Covering/Basic.lean (MO1.12, #1323).

Circle-valued rotations

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleMatrix (z : Circle) : Matrix (Fin 2) (Fin 2) ℝ

Rotation matrix whose first column is the point z of the unit circle.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleMatrix z = !![(↑z).re, -(↑z).im; (↑z).im, (↑z).re]

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleMatrixInv (z : Circle) : Matrix (Fin 2) (Fin 2) ℝ

The transpose/inverse of circleMatrix.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleMatrixInv z = !![(↑z).re, (↑z).im; -(↑z).im, (↑z).re]

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleMatrix_det (z : Circle) : (circleMatrix z).det = 1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleMatrix_mul_inv (z : Circle) : circleMatrix z * circleMatrixInv z = 1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleMatrix_inv_mul (z : Circle) : circleMatrixInv z * circleMatrix z = 1

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleGLPos (z : Circle) : ↥(Matrix.GLPos (Fin 2) ℝ)

A circle-valued 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.circleGLPos_mat (z : Circle) : toMat (circleGLPos z) = circleMatrix z

Global coordinates on the base

@[reducible, inline]

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

Coordinates on GL⁺(2, ℝ): first-column direction and radius, followed by the coordinates of the second column in that oriented orthonormal frame.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.firstColumnComplex (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : ℂ

The first column of a positive-determinant matrix, regarded as a complex number.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.firstColumnComplex_ne_zero (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : firstColumnComplex T ≠ 0

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.firstColumnRadius (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : ↑PositiveReal

The positive length of the first column.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.firstColumnDirection (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : Circle

The direction of the first column.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.firstColumnDirection_re (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : (↑(firstColumnDirection T)).re = toMat T 0 0 / ↑(firstColumnRadius T)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.firstColumnDirection_im (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : (↑(firstColumnDirection T)).im = toMat T 1 0 / ↑(firstColumnRadius T)

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

Component of the second column along the normalized first column.

Equations

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

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

Component of the second column along the positively oriented normal.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.secondColumnPerp_pos (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : 0 < secondColumnPerp T

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glPosCoordinates (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : GLPosCoordinates

Coordinates of a positive-determinant matrix.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glPosOfCoordinates (c : GLPosCoordinates) : ↥(Matrix.GLPos (Fin 2) ℝ)

Reconstruct a positive-determinant matrix from its circle coordinates.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glPosOfCoordinates_mat (c : GLPosCoordinates) : toMat (glPosOfCoordinates c) = circleMatrix c.1 * upperMatrix c.2.1 c.2.2.1 c.2.2.2

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.firstColumnDirection_glPosOfCoordinates (c : GLPosCoordinates) : firstColumnDirection (glPosOfCoordinates c) = c.1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.secondColumnAlong_glPosOfCoordinates (c : GLPosCoordinates) : secondColumnAlong (glPosOfCoordinates c) = c.2.2.1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.secondColumnPerp_glPosOfCoordinates (c : GLPosCoordinates) : secondColumnPerp (glPosOfCoordinates c) = ↑c.2.2.2

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glPosCoordinates_ofCoordinates (c : GLPosCoordinates) : glPosCoordinates (glPosOfCoordinates c) = c

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glPosOfCoordinates_coordinates (T : ↥(Matrix.GLPos (Fin 2) ℝ)) : glPosOfCoordinates (glPosCoordinates T) = T

The base-coordinate homeomorphism

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.continuous_toMatGLPos : Continuous toMat

The underlying matrix of an element of GL⁺(2, ℝ) depends continuously on that element.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glPosCoordinateHomeomorph : ↥(Matrix.GLPos (Fin 2) ℝ) ≃ₜ GLPosCoordinates

Global coordinates on GL⁺(2, ℝ).

Equations

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

The standard phase covering

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.phaseCircle (θ : ℝ) : Circle

The direction on the unit circle represented by a lifted phase.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.phaseCircle θ = Circle.exp (Real.pi * θ)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.phaseCircle_isCoveringMap : IsCoveringMap phaseCircle

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.coordinateProjection : GLTildeCoordinates → GLPosCoordinates

The standard product covering in the global coordinates.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.coordinateProjection_isCoveringMap : IsCoveringMap coordinateProjection

Conjugating the matrix projection to the standard cover

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.phaseCircle_coe (θ : ℝ) : ↑(phaseCircle θ) = ↑(Real.cos (Real.pi * θ)) + ↑(Real.sin (Real.pi * θ)) * Complex.I

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.circleMatrix_phaseCircle (θ : ℝ) : circleMatrix (phaseCircle θ) = rotationMatrix θ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glPosOfCoordinates_coordinateProjection (c : GLTildeCoordinates) : glPosOfCoordinates (coordinateProjection c) = (glTildeOfCoordinates c).mat

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.coordinateProjection_apply_glTildeCoordinates (x : GLTilde) : coordinateProjection (glTildeCoordinateHomeomorph x) = glPosCoordinateHomeomorph x.mat

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.isCoveringMap_toMat : IsCoveringMap mat

The matrix projection is a covering map for the global-coordinate topology.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.universalCoverData : IsCoveringMap mat ∧ Function.Surjective mat ∧ SimplyConnectedSpace GLTilde

The data comprising the universal-cover statement: the matrix projection is a surjective covering map and its source is simply connected.