Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Symmetry.Combined.LatticeAut

Lattice automorphisms in the combined symmetry group #

The compatible lattice automorphism carried by AutPair descends through AutPairQuot: the quotient relation fixes that component on the nose. This file exposes the descended automorphism and its interaction with the group operations.

The multiplication formula is deliberately recorded as a plain lemma rather than a bundled homomorphism. Multiplication satisfies (p * q).lam = p.lam.trans q.lam; choosing whether to regard this as a map to AddAut Λ or its opposite is a variance decision that should be made only by a consumer that needs the bundle.

The same file records that the real-linear action of a positive invertible matrix on ℂ is injective and therefore detects zero. These are the two algebraic facts needed to transport charge-vanishing walls.

source
def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.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 →+ Λ} (q : AutPairQuot v) :
Λ ≃+ Λ

The class-lattice automorphism carried by a compatible autoequivalence pair, descended to the quotient by natural isomorphism.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.lam_mk {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) :
    (mk a).lam = a.lam

    The descended lattice automorphism agrees definitionally with a representative.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.lam_mul {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 →+ Λ} (p q : AutPairQuot v) :
    (p * q).lam = p.lam.trans q.lam

    Multiplication composes the carried lattice automorphisms in action order.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.lam_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 Λ] {v : K₀ C →+ Λ} :
    lam 1 = AddEquiv.refl Λ

    The identity symmetry carries the identity lattice automorphism.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.lam_inv {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 →+ Λ} (p : AutPairQuot v) :
    p⁻¹.lam = p.lam.symm

    Inversion replaces the carried lattice automorphism by its inverse.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actC_injective (T : ↥(Matrix.GLPos (Fin 2) ℝ)) :
    Function.Injective ⇑(actC T)

    The real-linear action of an invertible positive matrix on ℂ is injective.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.actC_eq_zero_iff (T : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : ℂ) :
    (actC T) z = 0 ↔ z = 0

    The real-linear action of an invertible positive matrix detects zero.