Compatibility, restated on the complex rays #
A central charge is Z : Λ →+ ℂ -- it lands in ℂ. GLTilde.mat acts on
Fin 2 → ℝ. These do not compose directly, so the two coordinate conventions
must agree.
They do, and cplxCoord_exp is the proof: under Complex.basisOneI (whose
repr is ![z.re, z.im]), the canonical ray exp (i π φ) has coordinates
![cos (π φ), sin (π φ)], which is exactly rayVec φ.
The neutral half of the bridge -- cplxCoord, actC and the two action laws,
whose public types mention the general-linear group and not its cover -- is in
LinearAlgebra/Complex/Coordinates.lean. The three statements here are the
ones that mention rayVec, Compatible and NormalizedShift, so they are
comparisons and stay with the cover (MO1.12, #1323; cutover-ledger row 08).
The conventions agree. The stability foundation writes its rays as
exp (i π φ)
(CategoryTheory/Triangulated/StabilityCondition/Foundation/PreStabilityCondition.lean);
in basisOneI coordinates that is rayVec φ.
Proved through Complex.basisOneI.repr rather than Basis.equivFun_apply:
the two are definitionally equal, and the repr route avoids simp
normalising ↑(π * φ) into ↑π * ↑φ, which stops
Complex.exp_ofReal_mul_I_re from matching.
Compatible, restated on the stability foundation's rays.
It says T carries the charge-ray at phase φ to the charge-ray at phase
f φ, entirely in the exp (i π ·) vocabulary of
CategoryTheory/Triangulated/StabilityCondition/Foundation/PreStabilityCondition.lean.
Compatible, as a statement about actC on the charge rays.
The map T carries the charge ray at phase φ to the charge ray at phase
f φ, scaled by some r > 0.