Twisting modules by automorphisms

For Lemma 4.13 (lem:scalar-object-values, scalar-normalization.tex): "A weight scales morphism lines and thus defines an automorphism of L. These automorphisms act on the indecomposable module classes with any fixed finite support, by precomposing their actions with the scalar automorphism. […] only finitely many indecomposable classes supported in S occur. Their permutation image is finite, abelian and divisible, hence trivial."

For an automorphism σ of a representation-finite algebra, the twist M ↦ M^σ permutes the finitely many indecomposable classes, so a fixed power N (the order of the permutation group) of any automorphism fixes every class (twist_pow_iso). With the divisibility of weights this gives the triviality of the action.

def MultiplicativeBasisDeformations.opHom {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) : Bᵐᵒᵖ →+* Bᵐᵒᵖ

The ring automorphism of Bᵐᵒᵖ induced by an algebra automorphism.

noncomputable def MultiplicativeBasisDeformations.twist {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) (M : RightModuleCat B) : RightModuleCat B

The twist of a right module by an automorphism: m · b = m · σ(b).

noncomputable def MultiplicativeBasisDeformations.twistF {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) : CategoryTheory.Functor (RightModuleCat B) (RightModuleCat B)

The twist as a functor.

noncomputable def MultiplicativeBasisDeformations.twistEquiv {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) : RightModuleCat B ≌ RightModuleCat B

The twist is an equivalence.

theorem MultiplicativeBasisDeformations.twistEquiv_functor {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) : (twistEquiv σ).functor = twistF σ

instance MultiplicativeBasisDeformations.instFullRightModuleCatTwistF {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) : (twistF σ).Full

instance MultiplicativeBasisDeformations.instFaithfulRightModuleCatTwistF {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) : (twistF σ).Faithful

instance MultiplicativeBasisDeformations.instAdditiveRightModuleCatTwistF {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) : (twistF σ).Additive

theorem MultiplicativeBasisDeformations.twist_smul {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) (M : RightModuleCat B) (b : Bᵐᵒᵖ) (m : ↑(twist σ M)) : b • m = MulOpposite.op (σ (MulOpposite.unop b)) • have this := m; this

def MultiplicativeBasisDeformations.twistK {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) (M : RightModuleCat B) : ↑M →ₗ[k] ↑(twist σ M)

The identity map M → M^σ is k-linear.

theorem MultiplicativeBasisDeformations.twist_finite {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (σ : B ≃ₐ[k] B) (M : RightModuleCat B) [Module.Finite k ↑M] : Module.Finite k ↑(twist σ M)

theorem MultiplicativeBasisDeformations.twist_isFiniteIndecomposable {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [FiniteDimensional k B] (σ : B ≃ₐ[k] B) {M : RightModuleCat B} (hM : IsFiniteIndecomposable k B M) : IsFiniteIndecomposable k B (twist σ M)

theorem MultiplicativeBasisDeformations.twist_mul {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [FiniteDimensional k B] (σ τ : B ≃ₐ[k] B) (M : RightModuleCat B) : Nonempty (twist (σ * τ) M ≅ twist τ (twist σ M))

Twisting twice.

theorem MultiplicativeBasisDeformations.twist_one {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [FiniteDimensional k B] (M : RightModuleCat B) : Nonempty (twist 1 M ≅ M)

theorem MultiplicativeBasisDeformations.twist_iso {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [FiniteDimensional k B] (σ : B ≃ₐ[k] B) {M M' : RightModuleCat B} (e : M ≅ M') : Nonempty (twist σ M ≅ twist σ M')

theorem MultiplicativeBasisDeformations.twist_reflect {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [FiniteDimensional k B] (σ : B ≃ₐ[k] B) {M M' : RightModuleCat B} (e : twist σ M ≅ twist σ M') : Nonempty (M ≅ M')

theorem MultiplicativeBasisDeformations.twist_pow_iso {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] [FiniteDimensional k B] (hB : IsRepresentationFinite k B) : ∃ (N : ℕ), 0 < N ∧ ∀ (τ : B ≃ₐ[k] B) (M : RightModuleCat B), IsFiniteIndecomposable k B M → Nonempty (twist (τ ^ N) M ≅ M)

A fixed power of every automorphism of a representation-finite algebra fixes every indecomposable class (the permutation image is a finite group).