The lifted general linear group as compatible pairs

Bridgeland presents the universal cover of GL⁺(2, ℝ) concretely, as pairs (T, f) with T ∈ GL⁺(2, ℝ) and f a normalized shift, subject to T and f inducing the same map on the circle of phases.

The circle is ℝ / 2ℤ, embedded in ℝ² by φ ↦ (cos πφ, sin πφ). The factor π (not 2π) is Bridgeland's phase convention: a semistable object of phase φ has central charge on the ray at angle πφ, so φ ↦ φ + 1 is the antipodal map — the shift functor [1]. rayVec_add_one below is exactly that statement, and it is the reason NormalizedShift demands f (φ + 1) = f φ + 1.

"Same map on the circle" is then: T sends the ray through rayVec φ to the ray through rayVec (f φ).

What is proved across this development

This file proves that the compatible pairs form a group under componentwise multiplication, and that the type is nonempty (compat_one is the witness). The companion files prove the covering-space properties:

• Fibre ℤ — proved, in UniversalCover/Fibre.lean. The kernel of the projection is exactly the deck transformations φ ↦ φ + 2n.
• Surjectivity of the projection — proved, in UniversalCover/Surjectivity.lean. Every T of positive determinant carries a compatible phase relabelling.
• Simple connectedness — proved, in UniversalCover/SourceTopology.lean, by global coordinates ℝ × (0,∞) × ℝ × (0,∞) and contractibility.
• Covering-map property — proved, in UniversalCover/Map.lean. Global base coordinates identify the projection with the standard exponential cover ℝ → S¹ times an identity map.

Thus GLTilde.universalCoverData packages the surjective covering-map and simple-connectedness properties, while exact_deckHom_toMatHom packages the extension with fibre ℤ. UniversalCover/TopologicalGroup.lean proves continuity of multiplication and inversion and installs IsTopologicalGroup GLTilde.

The action on stability conditions is downstream and stays with stability: StabilityCondition/Symmetry/GLTilde/Action/PreStability.lean and .../Action/Stability.lean use this group to define and prove it.

The phase circle

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rayVec (φ : ℝ) : Fin 2 → ℝ

The unit vector at phase φ: the ray at angle π φ.

The π, rather than 2π, is Bridgeland's phase convention — see the module docstring.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rayVec φ = ![Real.cos (Real.pi * φ), Real.sin (Real.pi * φ)]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rayVec_add_one (φ : ℝ) : rayVec (φ + 1) = -rayVec φ

Advancing the phase by one is the antipodal map.

This is the compatibility between NormalizedShift's +1-equivariance and the shift functor [1]: adding 1 to a phase negates the central charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rayVec_ne_zero (φ : ℝ) : rayVec φ ≠ 0

Phase vectors are never zero, so they really do determine rays.

Rays

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.OnRay (v w : Fin 2 → ℝ) : Prop

v lies on the same ray as w: a positive multiple of it.

Deliberately not Mathlib's SameRay, which admits the zero vector. Every vector here is a rayVec, hence nonzero, and the strict version keeps the closure proofs free of degenerate cases.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.OnRay v w = ∃ (r : ℝ), 0 < r ∧ v = r • w

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.OnRay.refl (v : Fin 2 → ℝ) : OnRay v v

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.OnRay.trans {u v w : Fin 2 → ℝ} (h₁ : OnRay u v) (h₂ : OnRay v w) : OnRay u w

Compatible pairs

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.Compatible (T : ↥(Matrix.GLPos (Fin 2) ℝ)) (f : NormalizedShift) : Prop

T and f induce the same map on the circle of phases: T carries the ray at phase φ to the ray at phase f φ.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.compat_one : Compatible 1 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.compat_mul {T U : ↥(Matrix.GLPos (Fin 2) ℝ)} {f g : NormalizedShift} (hT : Compatible T f) (hU : Compatible U g) : Compatible (T * U) (f * g)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.compat_inv {T : ↥(Matrix.GLPos (Fin 2) ℝ)} {f : NormalizedShift} (hT : Compatible T f) : Compatible T⁻¹ f⁻¹

The group

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde : Type

G̃L⁺(2, ℝ) in Bridgeland's concrete presentation: a matrix of positive determinant together with a phase relabelling that agrees with it on the circle.

The covering-map and simple-connectedness properties are proved in the companion topology files and packaged by GLTilde.universalCoverData.

• mat : ↥(Matrix.GLPos (Fin 2) ℝ)

  The linear part, acting on central charges.

• shift : NormalizedShift

  The phase relabelling, acting on slicings.

• compat : Compatible self.mat self.shift

  The two agree on the circle of phases.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.ext' {x y : GLTilde} (hm : x.mat = y.mat) (hs : x.shift = y.shift) : x = y

compat is a Prop, so the two data fields determine the pair.

Named ext': Lean auto-generates GLTilde.ext for the structure.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.ext'_iff {x y : GLTilde} : x = y ↔ x.mat = y.mat ∧ x.shift = y.shift

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.group : Group GLTilde

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.mul_mat (x y : GLTilde) : (x * y).mat = x.mat * y.mat

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.mul_shift (x y : GLTilde) : (x * y).shift = x.shift * y.shift

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.one_mat : mat 1 = 1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.one_shift : shift 1 = 1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.inv_mat (x : GLTilde) : x⁻¹.mat = x.mat⁻¹

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.inv_shift (x : GLTilde) : x⁻¹.shift = x.shift⁻¹

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.toMatHom : GLTilde →* ↥(Matrix.GLPos (Fin 2) ℝ)

Projection to the linear part. A group hom by construction.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.toShiftHom : GLTilde →* NormalizedShift

Projection to the phase relabelling. A group hom by construction.

Step 3 composes the Slicing action with this.

Equations

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