Symmetry actions on chambers

A set of lattice classes is IsAutStable when every compatible autoequivalence preserves membership through its descended lattice automorphism. For such a set, the combined GLTilde × AutPairQuot v action restricts to the regular-locus subtype and hence, through the existing generic connected-component machinery, acts on ChargeChamber.

The full kernel of the action on the stability space acts trivially on chamber labels. Consequently the chamber action descends to EffectiveCombinedSymmetry v.

No faithfulness is asserted for the descended chamber action: an effective symmetry can move stability conditions inside a chamber while fixing its component label. Nor does this file assert transitivity, nonemptiness of any chamber, finiteness of a chamber stabilizer, an orbit-space construction, or openness of the regular locus.

Invariant class sets

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.ChargeZero.IsAutStable {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 →+ Λ} (Δ : Set Λ) : Prop

A set of lattice classes is stable under every lattice automorphism carried by a compatible autoequivalence.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.ChargeZero.isAutStable_univ {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 →+ Λ} : IsAutStable Set.univ

The full class lattice is stable under compatible autoequivalences.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.ChargeZero.IsAutStable.inter {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 →+ Λ} {Δ Γ : Set Λ} (hΔ : IsAutStable Δ) (hΓ : IsAutStable Γ) : IsAutStable (Δ ∩ Γ)

An intersection of stable class sets is stable.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.ChargeZero.IsAutStable.image_lam {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 →+ Λ} {Δ : Set Λ} (hΔ : IsAutStable Δ) (q : GroupAction.AutPairQuot v) : ⇑q.lam '' Δ = Δ

A stable class set is carried onto itself by each descended lattice automorphism.

The regular-locus action

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.chargeRegularLocusMulAction {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) : MulAction (GLTilde × AutPairQuot v) ↑(ChargeZero.chargeRegularLocus Δ)

The combined symmetry action restricts to the regular locus of an autoequivalence-stable class set.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.chargeRegularLocusContinuousConstSMul {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) : ContinuousConstSMul (GLTilde × AutPairQuot v) ↑(ChargeZero.chargeRegularLocus Δ)

The restricted action is continuous in the regular-locus variable for each fixed combined symmetry.

Equations

• ⋯ = ⋯

Chamber transport

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.chamberSmul {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) (p : GLTilde × AutPairQuot v) (cc : ChargeZero.ChargeChamber Δ) : ChargeZero.ChargeChamber Δ

The named specialization of componentSmul to regular-locus chambers.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.chamberHomeomorph {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) (p : GLTilde × AutPairQuot v) (cc : ChargeZero.ChargeChamber Δ) : { σ : ↑(ChargeZero.chargeRegularLocus Δ) // ChargeZero.chargeChamberOf σ = cc } ≃ₜ { σ : ↑(ChargeZero.chargeRegularLocus Δ) // ChargeZero.chargeChamberOf σ = chamberSmul hΔ p cc }

The named specialization of componentHomeomorph between chambers of the regular locus.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.chamberStabilizer {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) (cc : ChargeZero.ChargeChamber Δ) : Subgroup (GLTilde × AutPairQuot v)

The subgroup of combined symmetries preserving a chamber label.

Equations

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

Descent to the effective quotient

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.chamberActionHom {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) : GLTilde × AutPairQuot v →* Equiv.Perm (ChargeZero.ChargeChamber Δ)

The permutation representation of the combined symmetry group on chamber labels.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.combinedActionKernel_le_chamberActionHom_ker {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) : combinedActionKernel v ≤ (chamberActionHom hΔ).ker

Every symmetry acting trivially on the full stability space also acts trivially on chamber labels.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.effectiveChamberActionHom {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) : EffectiveCombinedSymmetry v →* Equiv.Perm (ChargeZero.ChargeChamber Δ)

The chamber permutation representation descended through the full kernel of the action on the stability space.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.effectiveCombinedChamberMulAction {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) : MulAction (EffectiveCombinedSymmetry v) (ChargeZero.ChargeChamber Δ)

The effective combined symmetry group acts on chamber labels. This action is deliberately not asserted faithful; see the module docstring.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.effectiveCombinedChamber_smul_coe {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {Δ : Set Λ} (hΔ : ChargeZero.IsAutStable Δ) (p : GLTilde × AutPairQuot v) (cc : ChargeZero.ChargeChamber Δ) : ↑p • cc = chamberSmul hΔ p cc

On a representative of the effective quotient, the descended action is the original combined action on chamber labels.