Surjectivity of the lifted matrix projection #
Every T ∈ GL⁺(2, ℝ) admits a compatible phase relabelling, so toMatHom
is onto.
Together with UniversalCover/Fibre.lean this closes the algebraic exact sequence.
UniversalCover/SourceTopology.lean now supplies a topology, continuity of the projection,
and simple connectedness; UniversalCover/Map.lean proves the covering-map property.
The construction, and why it needs no branch cut #
Write T acting on ℂ in the form z ↦ a z + b z̄. This is possible for any
real-linear map, and the determinant comes out as ‖a‖² - ‖b‖², so det T > 0
says exactly ‖b‖ < ‖a‖. That single inequality is what makes the whole
construction work.
On the unit circle,
T (e^{iπφ}) = a e^{iπφ} + b e^{-iπφ} = e^{iπφ} · a · (1 + (b/a) e^{-2iπφ})
and the last factor W φ has real part at least 1 - ‖b/a‖ > 0. So W φ
never leaves the right half-plane, arg (W φ) is continuous with no branch-cut
trouble at all, and the lift can simply be written down:
lift φ = φ + arg a / π + arg (W φ) / π
No covering-space machinery, no path lifting, no monodromy. The branch cut is avoided by construction rather than worked around.
Monotonicity without differentiating #
The obvious route is to differentiate: lift' φ = (1 - ‖b/a‖²) / ‖W φ‖² > 0.
That is true and is the reason the result holds, but it costs a chain rule
through Complex.arg.
The cheaper route used here is the 2×2 cross product v × w = v₀w₁ - v₁w₀:
rayVec φ × rayVec ψ = sin (π (ψ - φ)), and(M *ᵥ v) × (M *ᵥ w) = det M · (v × w).
So for 0 < ψ - φ < 1 the image cross product is det T · sin (π (ψ - φ)) > 0,
which forces sin (π (lift ψ - lift φ)) > 0. That alone leaves the difference
ambiguous modulo 2 — but arg (W ·) lands in (-π/2, π/2), so
lift ψ - lift φ is pinned inside (-1, 2), and on that interval
sin (π x) > 0 has the unique solution set (0, 1).
Positivity of det is used twice, and differently: once to put W in the
right half-plane, once to sign the cross product.
The unit-circle exponential #
cexpI x = e^{ix}. Mathlib has no Complex.cis at the pinned revision.
Equations
Instances For
T as z ↦ a z + b z̄ #
The holomorphic part of T.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The antiholomorphic part of T.
Equations
- One or more equations did not get rendered due to their size.
Instances For
det T = ‖a‖² - ‖b‖². This is the identity that turns the hypothesis
det T > 0 into the inequality ‖b‖ < ‖a‖ the construction runs on.
The right-half-plane factor #
b / a, of norm < 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The factor that carries all the φ-dependence.
Its real part is bounded below by 1 - ‖b/a‖ > 0, which is the whole reason
this construction needs no branch cut.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lift #
The phase relabelling attached to T.
arg (cA T) is a constant; all the motion is in arg (Wmap T φ), which is
continuous because Wmap T φ never leaves the right half-plane.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining property of the lift. T carries the ray at phase φ to
the ray at phase lift T φ, scaled by ‖a‖ ‖W φ‖ > 0.
The 2×2 cross product #
The signed area v₀w₁ - v₁w₀.
Equations
- CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.cross v w = v 0 * w 1 - v 1 * w 0
Instances For
Strict monotonicity #
arg (Wmap T φ) is confined to (-π/2, π/2), because Wmap T φ has
positive real part. This is what pins the ambiguity the cross product leaves.
Continuity and surjectivity #
The result #
The phase relabelling attached to T, as a NormalizedShift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
G̃L⁺(2, ℝ) → GL⁺(2, ℝ) is surjective.
Every matrix of positive determinant carries a compatible phase relabelling, so it lies in the image of the projection.
The canonical section, and the ℤ-torsor structure #
What surjectivity gives beyond a bare existence statement: lift is canonical
— it is written down, not chosen — so it is a genuine section of the
projection, and every element of G̃L⁺(2, ℝ) factors uniquely through it.
This is concrete algebraic data supporting the later covering-map proof. What
it is not by itself is a topological statement; see
exact_deckHom_toMatHom.
The canonical section of the projection, given by the explicit lift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unique factorisation. Every element is a deck transformation composed with the canonical lift of its own matrix part.
No group-homomorphism property is claimed for sect, so this is a bijection
of sets with a canonical section, not a claimed semidirect-product
decomposition.
The algebraic covering-space facts, together.
1 → ℤ → G̃L⁺(2, ℝ) → GL⁺(2, ℝ) → 1 is exact: deckHom is injective, its
range is exactly the kernel of the projection, and the projection is onto.
This theorem packages the extension, not the topology. The covering-map and
simple-connectedness properties are packaged separately by
GLTilde.universalCoverData in UniversalCover/Map.lean.