Deck overlap and the effective symmetry group

The two factors of the combined symmetry group overlap. With the left-action conventions of this project, the categorical shift [2] acts on stability conditions as the deck transformation deck (-1). Consequently

(deck 1, [2])

acts trivially.

This file proves that convention-sensitive statement from the slicing shift axiom, records the overlap in the kernel of the combined action, and defines the effective symmetry group to be the quotient by the full action kernel. The induced action of that quotient is faithful by construction.

The shift-functor coherence used here comes from the reusable sign-correct interface in Triangulated.ShiftFunctor. The local names below remain thin compatibility wrappers for the stability-action API.

Shift functors as triangulated equivalences

@[implicit_reducible]

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftFunctorCommShift {C : Type u} [Category.{w, u} C] [HasShift C ℤ] (n : ℤ) : (shiftFunctor C n).CommShift ℤ

A shift functor coherently commutes with every other shift.

scoped, deliberately. The underlying reusable structure is explicit so that it cannot silently compete with another CommShift choice. This wrapper keeps the historical stability-action instance local to this namespace.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftFunctorCommShift n = CategoryTheory.Pretriangulated.shiftFunctorUnsignedCommShift C n

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftTwoMapTriangleIso {C : Type u} [Category.{w, u} C] [HasShift C ℤ] [Preadditive C] : (shiftFunctor C 2).mapTriangle ≅ Pretriangulated.Triangle.shiftFunctor C 2

For the even shift [2], mapping a triangle agrees with shifting that triangle: the usual (-1)^n sign is +1.

Equations

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

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftTwoIsTriangulated {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : (shiftFunctor C 2).IsTriangulated

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftNegTwoMapTriangleIso {C : Type u} [Category.{w, u} C] [HasShift C ℤ] [Preadditive C] : (shiftFunctor C (-2)).mapTriangle ≅ Pretriangulated.Triangle.shiftFunctor C (-2)

The inverse even shift has the same sign-free triangle comparison.

Equations

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

instance CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftNegTwoIsTriangulated {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : (shiftFunctor C (-2)).IsTriangulated

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftTwoTriEquiv {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : TriEquiv C

The categorical double shift as a bundled triangulated autoequivalence.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.K₀.map_shift_neg_two {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : K₀.map (shiftFunctor C (-2)) = AddMonoidHom.id (K₀ C)

The inverse functor of [2] acts trivially on K₀.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftTwoPair {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 →+ Λ) : AutPair v

The double shift paired with the identity automorphism of the class lattice. Compatibility follows because an even shift is the identity on K₀.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deckShift_neg_one_inv_apply (φ : ℝ) : (deckShift (-1))⁻¹.toOrderIso φ = φ + 2

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.shiftTwoPair_act_eq_deck_neg_one {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] [IsTriangulated C] (v : K₀ C →+ Λ) (σ : StabilityCondition.WithClassMap C v) : (shiftTwoPair v).act σ = deck (-1) • σ

Convention check. With the contravariant autoequivalence action used on slicings, the categorical double shift acts as deck (-1), not deck 1.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deck_mul_deck (m n : ℤ) : deck m * deck n = deck (m + n)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deck_zero : deck 0 = 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deck_one_shiftTwo_combined_smul {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] [IsTriangulated C] (v : K₀ C →+ Λ) (σ : StabilityCondition.WithClassMap C v) : (deck 1, AutPairQuot.mk (shiftTwoPair v)) • σ = σ

The diagonal overlap generator (deck 1, [2]) acts trivially.

Quotient by the full action kernel

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

The permutation representation of the combined symmetry group.

Equations

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

@[reducible, inline]

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

The subgroup of all combined symmetries acting trivially.

Equations

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

@[reducible, inline]

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

The effective symmetry group is the combined group modulo its full action kernel. This may identify more than the explicit deck/shift overlap in a particular category, exactly when additional symmetries act trivially.

Equations

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

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

The faithful permutation representation of the effective quotient.

Equations

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

@[implicit_reducible]

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

Equations

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

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

The quotient action is faithful by construction.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deck_one_shiftTwo_mem_combinedActionKernel {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] [IsTriangulated C] (v : K₀ C →+ Λ) : (deck 1, AutPairQuot.mk (shiftTwoPair v)) ∈ combinedActionKernel v

The explicit deck/double-shift overlap lies in the action kernel.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.deck_one_shiftTwo_eq_one_in_effective {C : Type u} [Category.{w, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] [IsTriangulated C] (v : K₀ C →+ Λ) : ↑(deck 1, AutPairQuot.mk (shiftTwoPair v)) = 1

Hence the overlap generator becomes the identity in the effective quotient.