Scalar automorphisms act trivially on module classes #
Lemma 4.13, first step (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 […]. Their
permutation image is finite, abelian and divisible, hence trivial. Every scalar
automorphism consequently fixes each V_X̃ up to isomorphism."
For a finite set of objects s of the graded covering category, a weight d
defines the automorphism σ_d of the covering algebra cov D s scaling the
(p, q)-entry by d(s p, s q) (scaleEquiv). By divisibility of weights
(Lemma 4.11(2)) σ_d = σ_e^N for the N of twist_pow_iso, so σ_d fixes
every finite-dimensional indecomposable class (weight_twist_iso).
def
MultiplicativeBasisDeformations.CatAlg.ent
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
(s : κ → CovObj D)
(a : ↥(cov D s))
(p q : κ)
:
s p ⟶ s q
An entry of a covering algebra element as a morphism of the cover.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.ent_ext
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{a b : ↥(cov D s)}
(h : ∀ (p q : κ), ent s a p q = ent s b p q)
:
a = b
def
MultiplicativeBasisDeformations.CatAlg.scale
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
(s : κ → CovObj D)
(d : CovObj D → CovObj D → k)
(a : ↥(cov D s))
:
↥(cov D s)
Scaling the entries by a function on pairs of objects.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.ent_scale
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
(d : CovObj D → CovObj D → k)
(a : ↥(cov D s))
(p q : κ)
:
theorem
MultiplicativeBasisDeformations.CatAlg.ent_mul
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
(a b : ↥(cov D s))
(p r : κ)
:
theorem
MultiplicativeBasisDeformations.CatAlg.ent_one
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
(p q : κ)
:
theorem
MultiplicativeBasisDeformations.CatAlg.scale_mul
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(hd : Thin.IsWeight (Set.range s) d)
(a b : ↥(cov D s))
:
theorem
MultiplicativeBasisDeformations.CatAlg.scale_one
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(hd : Thin.IsWeight (Set.range s) d)
:
scale s d 1 = 1
theorem
MultiplicativeBasisDeformations.CatAlg.scale_inv_scale
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(hd : Thin.IsWeight (Set.range s) d)
(a : ↥(cov D s))
:
theorem
MultiplicativeBasisDeformations.CatAlg.scale_scale_inv
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(hd : Thin.IsWeight (Set.range s) d)
(a : ↥(cov D s))
:
theorem
MultiplicativeBasisDeformations.CatAlg.scale_add
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(a b : ↥(cov D s))
:
theorem
MultiplicativeBasisDeformations.CatAlg.scale_smul
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(c : k)
(a : ↥(cov D s))
:
def
MultiplicativeBasisDeformations.CatAlg.scaleEquiv
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(hd : Thin.IsWeight (Set.range s) d)
:
The scalar automorphism σ_d of the covering algebra.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.scaleEquiv_apply
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(hd : Thin.IsWeight (Set.range s) d)
(a : ↥(cov D s))
:
(scaleEquiv hd) a = scale s d a
theorem
MultiplicativeBasisDeformations.CatAlg.scaleEquiv_pow
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(hd : Thin.IsWeight (Set.range s) d)
(N : ℕ)
(a : ↥(cov D s))
:
(scaleEquiv hd ^ N) a = scale s (fun (o o' : CovObj D) => d o o' ^ N) a
theorem
MultiplicativeBasisDeformations.CatAlg.weight_twist_iso
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
{κ : Type}
[Fintype κ]
[DecidableEq κ]
{s : κ → CovObj D}
{d : CovObj D → CovObj D → k}
(hd : Thin.IsWeight (Set.range s) d)
[Infinite k]
[IsAlgClosed k]
(H : HeightData D)
[∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ)
(M : RightModuleCat ↥(cov D s))
(hM : IsFiniteIndecomposable k (↥(cov D s)) M)
:
Nonempty (twist (scaleEquiv hd) M ≅ M)
Weights fix every indecomposable class (Lemma 4.13, first step).