Twisting modules by ring automorphisms

Let a monoid H act on a ring A by ring automorphisms, through a monoid homomorphism a : H →* RingAut A. Twisting an A-module M by h : H means restricting its scalars along (a h)⁻¹: the twisted module T_h M has the same underlying abelian group as M, with x acting as (a h)⁻¹ x acts on M. A morphism of modules is the same map between the twisted modules. Since (a (g * h))⁻¹ = (a h)⁻¹ ∘ (a g)⁻¹, twisting by g * h is twisting by h and then by g, so that T_(g * h) = T_g ∘ T_h.

This file assembles these twists into a left action of Discrete H on ModuleCat A, in the sense of Mathlib's MonoidalLeftAction, that is, a coherent categorical action of H:

• MonoidHom.restrictScalarsMonoidalLeftAction a: the action, with action functors ModuleCat.restrictScalars (a h).symm. Its unitor and associator are the comparison isomorphisms of restriction of scalars, ModuleCat.restrictScalarsId'App and ModuleCat.restrictScalarsComp'App, whose underlying linear maps are identities. As natural isomorphisms of action functors they are ModuleCat.restrictScalarsId' and ModuleCat.restrictScalarsComp' (MonoidHom.actionUnitNatIso_restrictScalarsMonoidalLeftAction and MonoidHom.actionLeftTensorIso_restrictScalarsMonoidalLeftAction).
• The action functors are additive equivalences, and they are R-linear for an R-algebra A when H acts by R-algebra automorphisms.
• MonoidHom.twistElem: an element of M viewed in its twist, with the twisting action of A (MonoidHom.smul_twistElem) and the unitor and associator computed on such elements. When H acts by R-algebra automorphisms, MonoidHom.twistLinearEquiv identifies M with its twists as R-modules.
• A property of modules is stable under the action when it is preserved by each twist. This is the case for the discrete modules of a topological ring (TauCeti.discreteModules) when H acts by homeomorphisms, and for the smooth modules for a family of left ideals (TauCeti.smoothModules) when each twist preserves the family up to cofinality. The action then restricts to these full subcategories.
• RingHom.leftLinearRestrictScalars: restriction of scalars along a ring homomorphism intertwining two such actions is equivariant for the twisting actions, with identity lineators.

Through MonoidalLeftAction.pseudofunctor, the action is a pseudofunctor out of the one-object bicategory of H whose unit and composition comparisons are those of restriction of scalars. For a monoid G acting on A by ring automorphisms and on a type X, TauCeti.actionCategoryTwist X a is this pseudofunctor composed with the label functor ActionCategory.π of the action category G ⋉ X, so that an arrow labelled g acts by restricting scalars along (a g)⁻¹.

Implementation notes

The action is built directly from ModuleCat.restrictScalars and its comparison isomorphisms, rather than by composing Mathlib's RingCat.moduleCatRestrictScalarsPseudofunctor with a functor out of SingleObj H: along that route the action would live on a Cat object and its associator would pick up the composition comparisons of the functor SingleObj H ⥤ RingCatᵒᵖ, so that it would not be ModuleCat.restrictScalarsComp'App on the nose. The morphisms of Discrete H act by identity maps, rather than by eqToHom, so that every coherence condition is an equality of identity maps.

References

Twisting categories of modules over completed enveloping algebras by automorphisms is the categorical action of loop groups in

• Edward Frenkel, Langlands Correspondence for Loop Groups, §1.3.

@[instance_reducible]

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

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.

theorem MonoidHom.restrictScalarsMonoidalLeftAction_actionObj {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (h : CategoryTheory.Discrete H) (M : ModuleCat A) : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj h M = (ModuleCat.restrictScalars ↑(RingEquiv.symm (a h.as))).obj M

An element h acts on ModuleCat A by restricting scalars along (a h)⁻¹.

@[simp]

theorem MonoidHom.restrictScalarsMonoidalLeftAction_actionHomRight_hom_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (h : CategoryTheory.Discrete H) {M N : ModuleCat A} (f : M ⟶ N) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight h f)) x = (CategoryTheory.ConcreteCategory.hom f) x

The twist of a morphism of modules is the same map of the underlying abelian groups.

@[simp]

theorem MonoidHom.restrictScalarsMonoidalLeftAction_actionHomLeft_hom_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) {c c' : CategoryTheory.Discrete H} (f : c ⟶ c') (M : ModuleCat A) (x : ↑M) : (ModuleCat.Hom.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M)) x = x

The action of a morphism of Discrete H on a twisted module is the identity map of the underlying abelian group.

@[simp]

theorem MonoidHom.restrictScalarsMonoidalLeftAction_actionAssocIso_hom_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (g h : CategoryTheory.Discrete H) (M : ModuleCat A) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso g h M).hom) x = x

The associator of the twisting action is the identity map of the underlying abelian group.

@[simp]

theorem MonoidHom.restrictScalarsMonoidalLeftAction_actionAssocIso_inv_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (g h : CategoryTheory.Discrete H) (M : ModuleCat A) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso g h M).inv) x = x

The inverse of the associator of the twisting action is the identity map of the underlying abelian group.

@[simp]

theorem MonoidHom.restrictScalarsMonoidalLeftAction_actionUnitIso_hom_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (M : ModuleCat A) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso M).hom) x = x

The unitor of the twisting action is the identity map of the underlying abelian group.

@[simp]

theorem MonoidHom.restrictScalarsMonoidalLeftAction_actionUnitIso_inv_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (M : ModuleCat A) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso M).inv) x = x

The inverse of the unitor of the twisting action is the identity map of the underlying abelian group.

theorem MonoidHom.actionUnitNatIso_restrictScalarsMonoidalLeftAction {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) : CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso (CategoryTheory.Discrete H) (ModuleCat A) = ModuleCat.restrictScalarsId' ↑(RingEquiv.symm (a 1)) ⋯

The unit comparison of the twisting action, as a natural isomorphism of action functors, is ModuleCat.restrictScalarsId'.

theorem MonoidHom.actionLeftTensorIso_restrictScalarsMonoidalLeftAction {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (g h : H) : CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftTensorIso (ModuleCat A) { as := g } { as := h } = ModuleCat.restrictScalarsComp' ↑(RingEquiv.symm (a g)) ↑(RingEquiv.symm (a h)) ↑(RingEquiv.symm (a (g * h))) ⋯

The product comparison T_(g * h) ≅ T_h ⋙ T_g of the twisting action, as a natural isomorphism of action functors, is ModuleCat.restrictScalarsComp' for the factorization (a (g * h))⁻¹ = (a h)⁻¹ ∘ (a g)⁻¹.

instance MonoidHom.additive_actionLeft_restrictScalarsMonoidalLeftAction {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c : CategoryTheory.Discrete H) : (CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft (ModuleCat A) c).Additive

The twisting action functors are additive.

instance MonoidHom.isEquivalence_actionLeft_restrictScalarsMonoidalLeftAction {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c : CategoryTheory.Discrete H) : (CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft (ModuleCat A) c).IsEquivalence

The twisting action functors are equivalences, since they restrict scalars along ring isomorphisms.

theorem MonoidHom.linear_actionLeft_restrictScalarsMonoidalLeftAction {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (R : Type u_2) [CommSemiring R] [Algebra R A] (ha : ∀ (h : H) (r : R), (a h) ((algebraMap R A) r) = (algebraMap R A) r) (c : CategoryTheory.Discrete H) : CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft (ModuleCat A) c)

If A is an R-algebra and H acts by R-algebra automorphisms, the twisting action functors are R-linear.

def MonoidHom.twistElem {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c : CategoryTheory.Discrete H) {X : ModuleCat A} (x : ↑X) : ↑(CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c X)

An element of an A-module X, viewed in its twist c ⊙ₗ X. The twist has the same underlying abelian group, so this is the identity; it records the twisted type, so that rewriting lemmas about elements of twists stay type-correct.

@[simp]

theorem MonoidHom.twistElem_add {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c : CategoryTheory.Discrete H) {X : ModuleCat A} (x y : ↑X) : a.twistElem c (x + y) = a.twistElem c x + a.twistElem c y

Viewing elements in a twist is additive.

theorem MonoidHom.exists_twistElem_eq {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c : CategoryTheory.Discrete H) {X : ModuleCat A} (x : ↑(CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c X)) : ∃ (y : ↑X), a.twistElem c y = x

Every element of a twist is a twisted element.

theorem MonoidHom.smul_twistElem {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c : CategoryTheory.Discrete H) {X : ModuleCat A} (t : A) (x : ↑X) : t • a.twistElem c x = a.twistElem c ((RingEquiv.symm (a c.as)) t • x)

An element t acts on the twist by c as (a c)⁻¹ t acts on the module.

@[simp]

theorem MonoidHom.actionHomRight_hom_twistElem {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c : CategoryTheory.Discrete H) {X Y : ModuleCat A} (g : X ⟶ Y) (x : ↑X) : (ModuleCat.Hom.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c g)) (a.twistElem c x) = a.twistElem c ((ModuleCat.Hom.hom g) x)

The twist of a morphism acts on twisted elements as the morphism.

@[simp]

theorem MonoidHom.actionAssocIso_hom_twistElem {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c c' : CategoryTheory.Discrete H) {X : ModuleCat A} (x : ↑X) : (ModuleCat.Hom.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' X).hom) (a.twistElem (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') x) = a.twistElem c (a.twistElem c' x)

The associator of the twisting action is the identity on twisted elements.

@[simp]

theorem MonoidHom.actionAssocIso_inv_twistElem {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (c c' : CategoryTheory.Discrete H) {X : ModuleCat A} (x : ↑X) : (ModuleCat.Hom.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' X).inv) (a.twistElem c (a.twistElem c' x)) = a.twistElem (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') x

The inverse of the associator of the twisting action is the identity on twisted elements.

@[simp]

theorem MonoidHom.actionUnitIso_hom_twistElem {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) {X : ModuleCat A} (x : ↑X) : (ModuleCat.Hom.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom) (a.twistElem (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete H)) x) = x

The unitor of the twisting action is the identity on twisted elements.

theorem MonoidHom.actionUnitIso_inv_twistElem {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) {X : ModuleCat A} (x : ↑X) : (ModuleCat.Hom.hom (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).inv) x = a.twistElem (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete H)) x

The inverse of the unitor of the twisting action is the identity on twisted elements.

def MonoidHom.twistLinearEquiv {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (R : Type u_2) [CommSemiring R] [Algebra R A] (ha : ∀ (h : H) (r : R), (a h) ((algebraMap R A) r) = (algebraMap R A) r) (c : CategoryTheory.Discrete H) (M : ModuleCat A) : ↑M ≃ₗ[R] ↑(CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c M)

If A is an R-algebra and H acts by R-algebra automorphisms, an A-module and its twist are the same R-module.

@[simp]

theorem MonoidHom.twistLinearEquiv_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (R : Type u_2) [CommSemiring R] [Algebra R A] (ha : ∀ (h : H) (r : R), (a h) ((algebraMap R A) r) = (algebraMap R A) r) (c : CategoryTheory.Discrete H) {M : ModuleCat A} (x : ↑M) : (a.twistLinearEquiv R ha c M) x = a.twistElem c x

@[simp]

theorem MonoidHom.twistLinearEquiv_symm_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) (R : Type u_2) [CommSemiring R] [Algebra R A] (ha : ∀ (h : H) (r : R), (a h) ((algebraMap R A) r) = (algebraMap R A) r) (c : CategoryTheory.Discrete H) {M : ModuleCat A} (x : ↑M) : (a.twistLinearEquiv R ha c M).symm (a.twistElem c x) = x

theorem MonoidHom.twistElem_smul {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) {R : Type u_2} [CommSemiring R] [Algebra R A] (ha : ∀ (h : H) (r : R), (a h) ((algebraMap R A) r) = (algebraMap R A) r) (c : CategoryTheory.Discrete H) {M : ModuleCat A} (r : R) (x : ↑M) : a.twistElem c (r • x) = r • a.twistElem c x

If H acts by R-algebra automorphisms, twisting commutes with the action of R.

theorem MonoidHom.isStableUnderLeftAction_restrictScalarsMonoidalLeftAction_iff {H : Type u_1} [Monoid H] {A : Type u} [Ring A] {a : H →* RingAut A} {P : CategoryTheory.ObjectProperty (ModuleCat A)} : CategoryTheory.ObjectProperty.IsStableUnderLeftAction (CategoryTheory.Discrete H) P ↔ ∀ (h : H) (M : ModuleCat A), P M → P ((ModuleCat.restrictScalars ↑(RingEquiv.symm (a h))).obj M)

A property of A-modules is stable under the twisting action if and only if it is preserved by restriction of scalars along each (a h)⁻¹.

theorem MonoidHom.isStableUnderLeftAction_discreteModules {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) [TopologicalSpace A] (ha : ∀ (h : H), Continuous ⇑(RingEquiv.symm (a h))) : CategoryTheory.ObjectProperty.IsStableUnderLeftAction (CategoryTheory.Discrete H) (TauCeti.discreteModules A)

When H acts on a topological ring A by homeomorphisms, the twisting action preserves the discrete modules, so it restricts to the full subcategory of discrete A-modules.

theorem MonoidHom.isStableUnderLeftAction_smoothModules {H : Type u_1} [Monoid H] {A : Type u} [Ring A] (a : H →* RingAut A) {ι : Type u_2} (J : ι → Submodule A A) (hJ : ∀ (h : H) (i : ι), ∃ (i' : ι), J i' ≤ Ideal.comap (RingEquiv.symm (a h)) (J i)) : CategoryTheory.ObjectProperty.IsStableUnderLeftAction (CategoryTheory.Discrete H) (TauCeti.smoothModules J)

When each twist pulls every left ideal of the family J back to a superset of some member of J, the twisting action preserves the modules that are smooth for J, so it restricts to the full subcategory of smooth modules.

@[instance_reducible]

noncomputable def RingHom.leftLinearRestrictScalars {H : Type u_1} [Monoid H] {A : Type u} [Ring A] {B : Type u_2} [Ring B] (f : A →+* B) {a : H →* RingAut A} {b : H →* RingAut B} (hf : ∀ (h : H) (x : A), f ((a h) x) = (b h) (f x)) : (ModuleCat.restrictScalars f).LeftLinear (CategoryTheory.Discrete H)

If a ring homomorphism f : A →+* B intertwines actions a and b of H by ring automorphisms, then restriction of scalars along f is equivariant for the twisting actions. Twisting the restriction of a B-module by h and restricting its twist are both restriction of scalars along f ∘ (a h)⁻¹ = (b h)⁻¹ ∘ f, and the lineators are the identity maps of the underlying abelian group.

@[simp]

theorem RingHom.leftLinearRestrictScalars_μₗ_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] {B : Type u_2} [Ring B] (f : A →+* B) {a : H →* RingAut A} {b : H →* RingAut B} (hf : ∀ (h : H) (x : A), f ((a h) x) = (b h) (f x)) (c : CategoryTheory.Discrete H) (M : ModuleCat B) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxLeftLinear.μₗ (ModuleCat.restrictScalars f) c M)) x = x

The lax lineators of RingHom.leftLinearRestrictScalars are identity maps.

@[simp]

theorem RingHom.leftLinearRestrictScalars_δₗ_apply {H : Type u_1} [Monoid H] {A : Type u} [Ring A] {B : Type u_2} [Ring B] (f : A →+* B) {a : H →* RingAut A} {b : H →* RingAut B} (hf : ∀ (h : H) (x : A), f ((a h) x) = (b h) (f x)) (c : CategoryTheory.Discrete H) (M : ModuleCat B) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.OplaxLeftLinear.δₗ (ModuleCat.restrictScalars f) c M)) x = x

The oplax lineators of RingHom.leftLinearRestrictScalars are identity maps.

noncomputable def TauCeti.actionCategoryTwist {G : Type u_1} [Monoid G] (X : Type u_2) [MulAction G X] {A : Type u} [Ring A] (a : G →* RingAut A) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.ActionCategory G X)) CategoryTheory.Cat

The twisting action of G on ModuleCat A, as a pseudofunctor out of the action category G ⋉ X (an action groupoid when G is a group): an arrow labelled g acts by restricting scalars along (a g)⁻¹. It is the classifying pseudofunctor of MonoidHom.restrictScalarsMonoidalLeftAction composed with the label functor ActionCategory.π G X.

@[simp]

theorem TauCeti.actionCategoryTwist_obj {G : Type u_1} [Monoid G] {X : Type u_2} [MulAction G X] {A : Type u} [Ring A] {a : G →* RingAut A} (x : CategoryTheory.LocallyDiscrete (CategoryTheory.ActionCategory G X)) : (actionCategoryTwist X a).obj x = ↧(ModuleCat A)

theorem TauCeti.actionCategoryTwist_map_toFunctor {G : Type u_1} [Monoid G] {X : Type u_2} [MulAction G X] {A : Type u} [Ring A] {a : G →* RingAut A} {x y : CategoryTheory.LocallyDiscrete (CategoryTheory.ActionCategory G X)} (f : x ⟶ y) : ((actionCategoryTwist X a).map f).toFunctor = ModuleCat.restrictScalars ↑(RingEquiv.symm (a f.as.hom))

The transport functor of actionCategoryTwist X a along an arrow labelled g is restriction of scalars along (a g)⁻¹.

theorem TauCeti.actionCategoryTwist_mapId_app {G : Type u_1} [Monoid G] {X : Type u_2} [MulAction G X] {A : Type u} [Ring A] {a : G →* RingAut A} (x : CategoryTheory.LocallyDiscrete (CategoryTheory.ActionCategory G X)) (M : ModuleCat A) : (CategoryTheory.Cat.Hom.toNatIso ((actionCategoryTwist X a).mapId x)).app M = ModuleCat.restrictScalarsId'App ↑(RingEquiv.symm (a 1)) ⋯ M

The unit comparison of actionCategoryTwist X a is ModuleCat.restrictScalarsId'App.

theorem TauCeti.actionCategoryTwist_mapComp_app {G : Type u_1} [Monoid G] {X : Type u_2} [MulAction G X] {A : Type u} [Ring A] {a : G →* RingAut A} {x y z : CategoryTheory.LocallyDiscrete (CategoryTheory.ActionCategory G X)} (f : x ⟶ y) (g : y ⟶ z) (M : ModuleCat A) : (CategoryTheory.Cat.Hom.toNatIso ((actionCategoryTwist X a).mapComp f g)).app M = ModuleCat.restrictScalarsComp'App ↑(RingEquiv.symm (a g.as.hom)) ↑(RingEquiv.symm (a f.as.hom)) ↑(RingEquiv.symm (a (g.as.hom * f.as.hom))) ⋯ M

The composition comparison of actionCategoryTwist X a at f ≫ g, an arrow labelled by the product g.hom * f.hom, is ModuleCat.restrictScalarsComp'App for the factorization (a (g.hom * f.hom))⁻¹ = (a f.hom)⁻¹ ∘ (a g.hom)⁻¹.