Documentation

TauCeti.CategoryTheory.Equivalence.Artin

Artin actions by autoequivalences #

A family of autoequivalences indexed by the vertices of a simple graph determines an action of the graph Artin group as soon as nonadjacent generators commute and adjacent generators satisfy the three-term braid relation, both up to natural isomorphism. Passing to TauCeti.AutoequivalenceClass turns these natural isomorphisms into equalities, so the graph Artin presentation supplies an honest group homomorphism.

This is the categorical form in which braid complexes act on a homotopy or derived category: one first proves the generator functors are autoequivalences and constructs the two rank-two natural isomorphisms, then applies SimpleGraph.artinAutoequivalenceAction.

For an arbitrary Coxeter matrix, two supplied Artin actions agree after transport through a category equivalence precisely when that equivalence naturally intertwines their specified generator functors.

Main definitions #

Main results #

source
noncomputable def SimpleGraph.artinAutoequivalenceAction {V : Type u} (G : SimpleGraph V) {C : Type v} [CategoryTheory.Category.{w, v} C] (E : V → (C ≌ C)) (commute : ∀ {i j : V}, i ≠ j → ¬G.Adj i j → Nonempty (((E i).trans (E j)).functor ≅ ((E j).trans (E i)).functor)) (braid : ∀ {i j : V}, G.Adj i j → Nonempty (((E i).trans ((E j).trans (E i))).functor ≅ ((E j).trans ((E i).trans (E j))).functor)) :
TauCeti.ArtinGroup G.coxeterMatrix →* TauCeti.AutoequivalenceClass C

A family of autoequivalences satisfying the graph's commuting and braid relations up to natural isomorphism determines a homomorphism from the graph Artin group to the group of autoequivalence classes.

The relation hypotheses are parenthesized using Equivalence.trans. Thus the adjacent relation compares the functors represented by Eᵢ ⋙ (Eⱼ ⋙ Eᵢ) and Eⱼ ⋙ (Eᵢ ⋙ Eⱼ); no strict associativity of functor composition is assumed.

Instances For
    source
    @[simp]
    theorem SimpleGraph.artinAutoequivalenceAction_gen {V : Type u} (G : SimpleGraph V) {C : Type v} [CategoryTheory.Category.{w, v} C] (E : V → (C ≌ C)) (commute : ∀ {i j : V}, i ≠ j → ¬G.Adj i j → Nonempty (((E i).trans (E j)).functor ≅ ((E j).trans (E i)).functor)) (braid : ∀ {i j : V}, G.Adj i j → Nonempty (((E i).trans ((E j).trans (E i))).functor ≅ ((E j).trans ((E i).trans (E j))).functor)) (i : V) :
    (G.artinAutoequivalenceAction E commute braid) (TauCeti.ArtinGroup.gen G.coxeterMatrix i) = (E i).toAutoequivalenceClass

    The Artin action sends a standard generator to the class of its indexing autoequivalence.

    source
    @[simp]
    theorem SimpleGraph.artinAutoequivalenceAction_gen_inv {V : Type u} (G : SimpleGraph V) {C : Type v} [CategoryTheory.Category.{w, v} C] (E : V → (C ≌ C)) (commute : ∀ {i j : V}, i ≠ j → ¬G.Adj i j → Nonempty (((E i).trans (E j)).functor ≅ ((E j).trans (E i)).functor)) (braid : ∀ {i j : V}, G.Adj i j → Nonempty (((E i).trans ((E j).trans (E i))).functor ≅ ((E j).trans ((E i).trans (E j))).functor)) (i : V) :
    (G.artinAutoequivalenceAction E commute braid) (TauCeti.ArtinGroup.gen G.coxeterMatrix i)⁻¹ = (E i).symm.toAutoequivalenceClass

    The inverse of a standard Artin generator acts by the inverse autoequivalence.

    source
    theorem CategoryTheory.Equivalence.autoequivalenceClassCongr_comp_artin_eq_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {B : Type u_1} {M : CoxeterMatrix B} (e : C ≌ D) (ρ₀ : TauCeti.ArtinGroup M →* TauCeti.AutoequivalenceClass C) (S : B → (C ≌ C)) (hS : ∀ (i : B), ρ₀ (TauCeti.ArtinGroup.gen M i) = (S i).toAutoequivalenceClass) (ρ : TauCeti.ArtinGroup M →* TauCeti.AutoequivalenceClass D) (F : B → (D ≌ D)) (hF : ∀ (i : B), ρ (TauCeti.ArtinGroup.gen M i) = (F i).toAutoequivalenceClass) :
    e.autoequivalenceClassCongr.toMonoidHom.comp ρ₀ = ρ ↔ ∀ (i : B), Nonempty (e.functor.comp (F i).functor ≅ (S i).functor.comp e.functor)

    Transport of an Artin action agrees with a target action precisely when the supplied equivalence naturally intertwines their generator representatives.