Topology of the combined symmetry action

The Bridgeland topology is generated by the sets basisNhd C σ ε. This file shows that a compatible autoequivalence pair carries each such neighborhood into the neighborhood with the same radius at the transported centre. Consequently every element of AutPairQuot v acts by a homeomorphism.

Only a one-sided estimate is needed for continuity. The inverse group element supplies the opposite direction automatically through Homeomorph.smul.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.Slicing.mapEquiv_phiPlus {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (s : Slicing C) (a : AutPair v) (E : C) (hE : ¬Limits.IsZero E) : Slicing.phiPlus C (s.mapEquiv a.Φ.e) E hE = Slicing.phiPlus C s (a.Φ.e.inverse.obj E) ⋯

Transport by an autoequivalence does not change the largest HN phase; it only replaces the object by its inverse image.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.Slicing.mapEquiv_phiMinus {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (s : Slicing C) (a : AutPair v) (E : C) (hE : ¬Limits.IsZero E) : Slicing.phiMinus C (s.mapEquiv a.Φ.e) E hE = Slicing.phiMinus C s (a.Φ.e.inverse.obj E) ⋯

Transport by an autoequivalence does not change the smallest HN phase; it only replaces the object by its inverse image.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.slicingDist_mapEquiv_le {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (a : AutPair v) (s₁ s₂ : Slicing C) : slicingDist C (s₁.mapEquiv a.Φ.e) (s₂.mapEquiv a.Φ.e) ≤ slicingDist C s₁ s₂

An autoequivalence does not increase the generalized slicing distance.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.stabSeminorm_aut_le {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} [IsTriangulated C] (a : AutPair v) (σ τ : StabilityCondition.WithClassMap C v) : Deformation.stabilitySeminorm C (a.act σ) ((a.act τ).Z - (a.act σ).Z) ≤ Deformation.stabilitySeminorm C σ (τ.Z - σ.Z)

The seminorm of a transported charge difference is no larger than the original seminorm.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.mapsTo_basisNhd {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} [IsTriangulated C] (a : AutPair v) (σ : StabilityCondition.WithClassMap C v) (ε : ℝ) : Set.MapsTo a.act (Deformation.basisNhd C σ ε) (Deformation.basisNhd C (a.act σ) ε)

A representative autoequivalence pair carries a basic neighborhood into the basic neighborhood of the transported centre, with unchanged radius.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair.continuous_act {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} [IsTriangulated C] (a : AutPair v) : Continuous a.act

Every fixed compatible autoequivalence acts continuously on the Bridgeland stability space.

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.autPairQuotContinuousConstSMul {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} [IsTriangulated C] : ContinuousConstSMul (AutPairQuot v) (StabilityCondition.WithClassMap C v)

The quotient action is continuous in the stability-condition variable.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.homeomorph {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} [IsTriangulated C] (q : AutPairQuot v) : StabilityCondition.WithClassMap C v ≃ₜ StabilityCondition.WithClassMap C v

A named homeomorphism for each compatible autoequivalence class.

Equations

• q.homeomorph = Homeomorph.smul q