Topological-group structure on the lifted general linear group

The topology on GLTilde was transported from the global coordinates

  ℝ × (0, ∞) × ℝ × (0, ∞).

This file proves that the already-defined group operations are continuous for that topology. The main point is joint continuity of phase evaluation (x, φ) ↦ x.shift φ. In global coordinates the normalized upper-triangular lift is

  φ + (arg (W φ) - arg (W 0)) / π,

so the potentially discontinuous global branch arg (cA) cancels. Every W φ lies in the open right half-plane, where arg is continuous.

The normalized upper-triangular lift

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.upperSectionZero_shift_apply (r : ↑PositiveReal) (b : ℝ) (d : ↑PositiveReal) (φ : ℝ) : (upperSectionZero r b d).shift.toOrderIso φ = lift (upperGLPos r b d) φ - lift (upperGLPos r b d) 0

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.coordinateShift (c : GLTildeCoordinates) (φ : ℝ) : ℝ

Phase evaluation written entirely in the global coordinates.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.glTildeOfCoordinates_shift_apply (c : GLTildeCoordinates) (φ : ℝ) : (glTildeOfCoordinates c).shift.toOrderIso φ = coordinateShift c φ

Joint phase evaluation

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.continuous_shift_apply : Continuous fun (p : GLTilde × ℝ) => p.1.shift.toOrderIso p.2

Evaluation of the phase relabelling is jointly continuous in the lifted matrix and the phase.

Continuous group operations

Inversion in the upper-triangular coordinates

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.GLTilde.isTopologicalGroup : IsTopologicalGroup GLTilde

The transported global-coordinate topology is compatible with the group operations.