Geometric representation categories and coherent local transport

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionCategoryTheory.MonoidalCategory.MonoidalLeftAction.pseudofunctorEquiv#

Left actions of Discrete M on categories correspond bijectively to pseudofunctors LocallyDiscrete (SingleObj M) ⥤ᵖ Cat: an action on C is sent to pseudofunctor M C, and a pseudofunctor F to the action F.monoidalLeftAction on its value at the unique object.

CategoryTheory.MonoidalCategory.MonoidalLeftAction.pseudofunctorEquiv.{w, v, u} (M : Type u)
  [Monoid M] :
  (C : CategoryTheory.Cat) ×
      CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete M) ↑C ≃
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.SingleObj M))
      CategoryTheory.Cat
Lean

Formalized in Tau Ceti as CategoryTheory.MonoidalCategory.MonoidalLeftAction.pseudofunctorEquiv.

Sources
LeanCategoryTheory.MonoidalCategory.MonoidalLeftAction.pseudofunctorEquiv

DefinitionCategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransEquiv#

Equivariant functors are the strong transformations between the pseudofunctors attached to the actions: functors C ⥤ D equipped with a left-linear structure for the actions of Discrete M correspond to strong transformations pseudofunctor M C ⟶ pseudofunctor M D. The correspondence keeps the lineators: the naturality isomorphisms of strongTrans M F have components the lineators of F.

CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransEquiv.{w, v, u} (M : Type u)
  [Monoid M] (C D : Type w) [CategoryTheory.Category.{v, w} C] [CategoryTheory.Category.{v, w} D]
  [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete M) C]
  [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete M) D] :
  (F : CategoryTheory.Functor C D) × F.LeftLinear (CategoryTheory.Discrete M) ≃
    (CategoryTheory.MonoidalCategory.MonoidalLeftAction.pseudofunctor M C).StrongTrans
      (CategoryTheory.MonoidalCategory.MonoidalLeftAction.pseudofunctor M D)
Lean

Formalized in Tau Ceti as CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransEquiv.

Sources
LeanCategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransEquiv

DefinitionCategoryTheory.MonoidalCategory.MonoidalLeftAction.modificationEquiv#

Equivariant natural transformations F₁ ⟶ F₂ correspond to modifications strongTrans M F₁ ⟶ strongTrans M F₂.

CategoryTheory.MonoidalCategory.MonoidalLeftAction.modificationEquiv.{w, v, u} (M : Type u)
  [Monoid M] {C D : Type w} [CategoryTheory.Category.{v, w} C] [CategoryTheory.Category.{v, w} D]
  [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete M) C]
  [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete M) D]
  (F₁ F₂ : CategoryTheory.Functor C D) [F₁.LeftLinear (CategoryTheory.Discrete M)]
  [F₂.LeftLinear (CategoryTheory.Discrete M)] :
  { τ // CategoryTheory.NatTrans.IsLeftLinear τ (CategoryTheory.Discrete M) } ≃
    (CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTrans M F₁).Modification
      (CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTrans M F₂)
Lean

Formalized in Tau Ceti as CategoryTheory.MonoidalCategory.MonoidalLeftAction.modificationEquiv.

Sources
LeanCategoryTheory.MonoidalCategory.MonoidalLeftAction.modificationEquiv

TheoremTauCeti.centralUnitIso_associativity_iff#

The associativity condition of a pseudofunctor out of LocallyDiscrete (SingleObj G) with identity 1-cells and central compositors centralUnitIso C (c (h, g)) at g ≫ h = h * g, evaluated at (g, h, j), is the 2-cocycle identity c (j * h, g) * c (j, h) = c (h, g) * c (j, h * g) of c at (j, h, g).

TauCeti.centralUnitIso_associativity_iff.{w, v, u} {G : Type u} [Monoid G] (C : Type w)
  [CategoryTheory.Category.{v, w} C] (c : G × G → (CategoryTheory.CatCenter C)ˣ) (g h j : G) :
  CategoryTheory.CategoryStruct.comp (TauCeti.centralUnitIso C (c (j, h * g))).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (TauCeti.centralUnitIso C (c (h, g))).hom
            (CategoryTheory.CategoryStruct.id ↧C))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id ↧C)
                (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C)).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id ↧C)
                (TauCeti.centralUnitIso C (c (j, h))).inv)
              (TauCeti.centralUnitIso C (c (j * h, g))).inv))) =
      CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id ↧C) ↔
    c (j * h, g) * c (j, h) = c (h, g) * c (j, h * g)
Lean

Formalized in Tau Ceti as TauCeti.centralUnitIso_associativity_iff.

Sources
LeanTauCeti.centralUnitIso_associativity_iff

TheoremTauCeti.centralUnitIso_naturality_comp_iff#

The composition condition of a strong transformation with identity components and naturality 2-cells centralUnitIso C (b g), between pseudofunctors with identity 1-cells and central compositors centralUnitIso C (c (h, g)) and centralUnitIso C (c' (h, g)) at g ≫ h = h * g, evaluated at (g, h), states that c' is c multiplied by the coboundary of b at (h, g).

TauCeti.centralUnitIso_naturality_comp_iff.{w, v, u} {G : Type u} [Monoid G] (C : Type w)
  [CategoryTheory.Category.{v, w} C] (b : G → (CategoryTheory.CatCenter C)ˣ)
  (c c' : G × G → (CategoryTheory.CatCenter C)ˣ) (g h : G) :
  CategoryTheory.CategoryStruct.comp (TauCeti.centralUnitIso C (b (h * g))).hom
        (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id ↧C)
          (TauCeti.centralUnitIso C (c' (h, g))).hom) =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (TauCeti.centralUnitIso C (c (h, g))).hom
          (CategoryTheory.CategoryStruct.id ↧C))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id ↧C)
              (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id ↧C)
              (TauCeti.centralUnitIso C (b h)).hom)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id ↧C)
                  (CategoryTheory.CategoryStruct.id ↧C) (CategoryTheory.CategoryStruct.id ↧C)).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerRight (TauCeti.centralUnitIso C (b g)).hom
                  (CategoryTheory.CategoryStruct.id ↧C))
                (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id ↧C)
                    (CategoryTheory.CategoryStruct.id ↧C)
                    (CategoryTheory.CategoryStruct.id ↧C)).hom)))) ↔
    c' (h, g) = b h * b g / b (h * g) * c (h, g)
Lean

Formalized in Tau Ceti as TauCeti.centralUnitIso_naturality_comp_iff.

Sources
LeanTauCeti.centralUnitIso_naturality_comp_iff

DefinitionTauCeti.DerivationExtension.innerEquiv#

Changing a derivation by an inner derivation does not change its self-extension: when δ' = δ + ad b, the map (u, v) ↦ (u + b • v, v) is an isomorphism E_δ(M) ≃ E_δ'(M).

TauCeti.DerivationExtension.innerEquiv.{u, v, u_1} {R : Type u_1} [CommRing R] {A : Type u} [Ring A]
  [Algebra R A] {δ δ' : ↥(TauCeti.derivationLieAlgebra R A)} {b : A} (M : Type v) [AddCommGroup M]
  [_root_.Module A M] (h : δ' = δ + (TauCeti.innerDerivation R) b) :
  TauCeti.DerivationExtension δ M ≃ₗ[A] TauCeti.DerivationExtension δ' M
Lean

Formalized in Tau Ceti as TauCeti.DerivationExtension.innerEquiv.

Sources
LeanTauCeti.DerivationExtension.innerEquiv
Uses 1
Statement usesTauCeti.DerivationExtension

TheoremTauCeti.isObjectwiseCongruenceInvariant_iff_of_equivalence#

Objectwise congruence invariance is independent of an equivariant presentation of the category. Only the forward functor of the equivalence needs a specified lineator.

TauCeti.isObjectwiseCongruenceInvariant_iff_of_equivalence.{u_1, v_1, u_2, v_2, u_3} {H : Type u_1}
  [Group H] {K : ℕ → Subgroup H} {C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C]
  [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) C] {D : Type u_3}
  [CategoryTheory.Category.{v_2, u_3} D]
  [CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) D] (e : C ≌ D)
  [e.functor.LeftLinear (CategoryTheory.Discrete H)] :
  TauCeti.IsObjectwiseCongruenceInvariant K C ↔ TauCeti.IsObjectwiseCongruenceInvariant K D
Lean

Formalized in Tau Ceti as TauCeti.isObjectwiseCongruenceInvariant_iff_of_equivalence.

Sources
LeanTauCeti.isObjectwiseCongruenceInvariant_iff_of_equivalence

DefinitionMonoidHom.restrictScalarsMonoidalLeftAction#

The left action of a monoid H on ModuleCat A by twisting along a homomorphism a : H →* RingAut A: an element h acts by restricting scalars along (a h)⁻¹. The associator (g * h) ⊙ₗ M ≅ g ⊙ₗ h ⊙ₗ M and the unitor 1 ⊙ₗ M ≅ M are the comparison isomorphisms of restriction of scalars, with identity underlying linear maps.

MonoidHom.restrictScalarsMonoidalLeftAction.{v, u, u_1} {H : Type u_1} [Monoid H] {A : Type u}
  [Ring A] (a : H →* RingAut A) :
  CategoryTheory.MonoidalCategory.MonoidalLeftAction (CategoryTheory.Discrete H) (ModuleCat A)
Lean

Formalized in Tau Ceti as MonoidHom.restrictScalarsMonoidalLeftAction.

Sources
LeanMonoidHom.restrictScalarsMonoidalLeftAction

StructureTauCeti.DerivationExtension#

The self-extension E_δ(M) of a module M attached to a derivation δ: pairs (u, v) of elements of M, on which a acts by a • (u, v) = (a • u + δ a • v, a • v). The first coordinate carries the submodule M and the second the quotient M.

TauCeti.DerivationExtension.{u, v, u_1} {R : Type u_1} [CommRing R] {A : Type u} [Ring A]
  [Algebra R A] (δ : ↥(TauCeti.derivationLieAlgebra R A)) (M : Type v) : Type v
Lean

Formalized in Tau Ceti as TauCeti.DerivationExtension.

Sources
LeanTauCeti.DerivationExtension
Used by 1
Used byTauCeti.DerivationExtension.innerEquiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.