The integer fibre of the lifted matrix projection #

The algebraic fibre calculation underlying the universal-cover construction.

Proved here: ker (toMatHom) ≃* Multiplicative ℤ, generated by the deck transformations φ ↦ φ + 2n. Every element of G̃L⁺(2, ℝ) lying over the identity matrix is one of these, and distinct n give distinct elements.

Proved in the companion files:

Surjectivity of toMatHom. Not proved here — landed separately in UniversalCover/Surjectivity.lean, which writes the lift down in closed form rather than invoking covering-space machinery.
Simple connectedness. Landed separately in UniversalCover/SourceTopology.lean, using global contractible coordinates rather than a computation of π₁(S¹).
Covering-map property. Landed in UniversalCover/Map.lean, by conjugating the projection in global coordinates to the standard exponential cover ℝ → S¹ times an identity map.

Why the kernel is exactly `2ℤ` and not `ℤ` #

Bridgeland's phase convention puts the circle at ℝ / 2ℤ: rayVec φ is the ray at angle π φ, so φ ↦ φ + 1 is the antipodal map (rayVec_add_one), and only φ ↦ φ + 2 returns a ray to itself. A normalized shift over the identity matrix must therefore move phases by an even integer.

The group is still ℤ — n ↦ (φ ↦ φ + 2n) — but the factor of two is Bridgeland's convention showing through, not an accident, and it is why deckShift is defined with 2 * n rather than n.

When two phases give the same ray #

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rayVec_eq_iff (φ ψ : ℝ) :

rayVec φ = rayVec ψ ↔ ∃ (n : ℤ), φ = ψ + 2 * ↑n

rayVec identifies exactly the phases differing by an even integer.

This is the statement that the phase line covers the circle of rays with deck group 2ℤ, in elementary form and with no covering-space machinery.

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.rayVec_eq_of_onRay {φ ψ : ℝ} (h : OnRay (rayVec φ) (rayVec ψ)) :

rayVec φ = rayVec ψ

On the unit circle OnRay is equality: both vectors have norm one, so the positive scalar is forced to be 1.

The deck transformations #

source

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deckShift (n : ℤ) :

NormalizedShift

The deck transformation φ ↦ φ + 2n, as a normalized shift.

2 * n, not n: only an even shift of phase returns every ray to itself. See the module docstring.

Equations

CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deckShift n = { toOrderIso := OrderIso.addRight (2 * ↑n), map_add_one := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deckShift_apply (n : ℤ) (φ : ℝ) :

(deckShift n).toOrderIso φ = φ + 2 * ↑n

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.compat_one_deckShift (n : ℤ) :

Compatible 1 (deckShift n)

A deck transformation is compatible with the identity matrix: it moves every ray back onto itself.

source

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deck (n : ℤ) :

GLTilde

The deck transformation as an element of G̃L⁺(2, ℝ).

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deck_mat (n : ℤ) :

(deck n).mat = 1

source

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deck_shift (n : ℤ) :

(deck n).shift = deckShift n

Everything over the identity is a deck transformation #

The one analytic step. A normalized shift lying over 1 moves each phase by some even integer; the content is that it is the same integer for every phase, which is connectedness of ℝ and nothing else.

source