The modules V_X̃ over finite subcategories of L #
Lemma 4.8 and the first step of Lemma 4.13 (scalar-normalization.tex). L is the graded covering category on the lifted
projective vertices (grading0). For a lifted object X̃ = (X, h) and a finite
set T of lifted projective vertices, V_X̃ restricted to T is a module over
the covering algebra cov T (VM): its value at z = (p, g) is the degree
g⁻¹h part of C(P_p, X), and L acts by composition. When T contains the
support of V_X̃ it is finite-dimensional and indecomposable: "Height gives
End(V_X̃) = k, so the modules are indecomposable" (VM_isFiniteIndecomposable,
via Lemma 4.8).
Restricting a grading to a subfamily #
def
MultiplicativeBasisDeformations.CatAlg.HomGrading.comp
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
(Dg : HomGrading F G)
{κ : Type}
[Fintype κ]
[DecidableEq κ]
(σ : κ → ι)
:
HomGrading (F ∘ σ) G
The restriction of a grading to a subfamily.
Instances For
def
MultiplicativeBasisDeformations.CatAlg.HeightData.comp
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{Dg : HomGrading F G}
(H : HeightData Dg)
{κ : Type}
[Fintype κ]
[DecidableEq κ]
(σ : κ → ι)
(hσ : Function.Injective σ)
:
HeightData (Dg.comp σ)
The restriction of height data to a subfamily with distinct labels.
Instances For
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.CatAlg.MeshData.grading0
{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]
{L : LocalFamily F}
(D : MeshData F L)
(Dg : HomGrading F G)
:
HomGrading D.F0 G
The grading of L: the deck grading on the projective labels.
Instances For
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.CatAlg.MeshData.sT
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
{L : LocalFamily F}
(D : MeshData F L)
(T : Finset (D.PV × G))
:
↥T → D.PV × G
The finite set T as objects of L.
Instances For
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.CatAlg.MeshData.covT
{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]
{L : LocalFamily F}
(D : MeshData F L)
(Dg : HomGrading F G)
(T : Finset (D.PV × G))
:
The covering algebra of T.
Instances For
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.CatAlg.MeshData.VX
{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]
{L : LocalFamily F}
(D : MeshData F L)
(Dg : HomGrading F G)
(T : Finset (D.PV × G))
(X : ι × G)
:
Type u
V_X̃ on T: at z = (p, g) the degree g⁻¹h part of C(P_p, X).
Instances For
def
MultiplicativeBasisDeformations.CatAlg.MeshData.ρ
{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]
{L : LocalFamily F}
(D : MeshData F L)
(Dg : HomGrading F G)
(T : Finset (D.PV × G))
:
Elements of the covering algebra as matrices.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.ρ_mem
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
(b : (↥(D.covT Dg T))ᵐᵒᵖ)
(p q : ↥T)
:
def
MultiplicativeBasisDeformations.CatAlg.MeshData.ιV
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
:
The underlying morphisms.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.ιV_injective
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
:
Function.Injective ⇑ιV
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.smul_mem
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
(b : (↥(D.covT Dg T))ᵐᵒᵖ)
(m : D.VX Dg T X)
(p : ↥T)
:
@[instance_reducible]
instance
MultiplicativeBasisDeformations.CatAlg.MeshData.instSMulMulOppositeSubtypeAlgProdPVMemFinsetCompF0LabSTSubalgebraCovTVX
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.ιV_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
(b : (↥(D.covT Dg T))ᵐᵒᵖ)
(m : D.VX Dg T X)
:
@[instance_reducible]
instance
MultiplicativeBasisDeformations.CatAlg.MeshData.instModuleMulOppositeSubtypeAlgProdPVMemFinsetCompF0LabSTSubalgebraCovTVX
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
:
def
MultiplicativeBasisDeformations.CatAlg.MeshData.VM
{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]
{L : LocalFamily F}
(D : MeshData F L)
(Dg : HomGrading F G)
(T : Finset (D.PV × G))
(X : ι × G)
:
RightModuleCat ↥(D.covT Dg T)
The module V_X̃|_T over the covering algebra.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.algebraMap_smul_VX
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
(c : k)
(m : D.VX Dg T X)
:
(algebraMap k (↥(D.covT Dg T))ᵐᵒᵖ) c • m = c • m
def
MultiplicativeBasisDeformations.CatAlg.MeshData.VMK
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
:
The identity from the native k-structure.
Instances For
instance
MultiplicativeBasisDeformations.CatAlg.MeshData.VM_finite
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
:
Module.Finite k ↑(D.VM Dg T X)
Matrix units and components #
def
MultiplicativeBasisDeformations.CatAlg.MeshData.unitE
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
(T : Finset (D.PV × G))
(q' q : ↥T)
(u : F ↑(↑q').1 ⟶ F ↑(↑q).1)
(hu : Dg.IsHom ((↑q').2⁻¹ * (↑q).2) u)
:
↥(D.covT Dg T)
The matrix unit of a morphism u : q' → q of L between objects of T.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.ρ_unitE
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(q' q : ↥T)
(u : F ↑(↑q').1 ⟶ F ↑(↑q).1)
(hu : Dg.IsHom ((↑q').2⁻¹ * (↑q).2) u)
(p r : ↥T)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.VX_sum_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{κ : Type}
(s : Finset κ)
(g : κ → D.VX Dg T X)
(p : ↥T)
:
(∑ i ∈ s, g i) p = ∑ i ∈ s, g i p
def
MultiplicativeBasisDeformations.CatAlg.MeshData.singleV
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
(q : ↥T)
:
A component concentrated at one object of T.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.singleV_same
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(q : ↥T)
(m : ↥(Dg.part ((↑q).2⁻¹ * X.2) (↑(↑q).1) X.1))
:
(singleV q) m q = m
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.singleV_ne
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{q p : ↥T}
(h : p ≠ q)
(m : ↥(Dg.part ((↑q).2⁻¹ * X.2) (↑(↑q).1) X.1))
:
(singleV q) m p = 0
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.unitE_smul_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(q' q : ↥T)
(u : F ↑(↑q').1 ⟶ F ↑(↑q).1)
(hu : Dg.IsHom ((↑q').2⁻¹ * (↑q).2) u)
(y : D.VX Dg T X)
(p : ↥T)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.unitE_smul_single
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(q' q : ↥T)
(u : F ↑(↑q').1 ⟶ F ↑(↑q).1)
(hu : Dg.IsHom ((↑q').2⁻¹ * (↑q).2) u)
(m : ↥(Dg.part ((↑q).2⁻¹ * X.2) (↑(↑q).1) X.1))
(hum : CategoryTheory.CategoryStruct.comp u ↑m ∈ Dg.part ((↑q').2⁻¹ * X.2) (↑(↑q').1) X.1)
:
def
MultiplicativeBasisDeformations.CatAlg.MeshData.IsScaled
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
(d : D.PV × G → D.PV × G → k)
{Y : ι × G}
(f : D.VX Dg T X →ₗ[k] D.VX Dg T Y)
:
Maps V_X̃ → V_Ỹ that scale the action of matrix units by d.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.IsScaled.concentrated
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{d : D.PV × G → D.PV × G → k}
{Y : ι × G}
{f : D.VX Dg T X →ₗ[k] D.VX Dg T Y}
(hf : IsScaled d f)
(q : ↥T)
(m : ↥(Dg.part ((↑q).2⁻¹ * X.2) (↑(↑q).1) X.1))
{p : ↥T}
(hp : p ≠ q)
:
f ((singleV q) m) p = 0
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.IsScaled.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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{d : D.PV × G → D.PV × G → k}
{Y : ι × G}
{f : D.VX Dg T X →ₗ[k] D.VX Dg T Y}
(hf : IsScaled d f)
(y : D.VX Dg T X)
(p : ↥T)
:
f y p = f ((singleV p) (y p)) p
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.IsScaled.nat
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{d : D.PV × G → D.PV × G → k}
{Y : ι × G}
{f : D.VX Dg T X →ₗ[k] D.VX Dg T Y}
(hf : IsScaled d f)
(q' q : ↥T)
(u : F ↑(↑q').1 ⟶ F ↑(↑q).1)
(hu : Dg.IsHom ((↑q').2⁻¹ * (↑q).2) u)
(m : ↥(Dg.part ((↑q).2⁻¹ * X.2) (↑(↑q).1) X.1))
(hum : CategoryTheory.CategoryStruct.comp u ↑m ∈ Dg.part ((↑q').2⁻¹ * X.2) (↑(↑q').1) X.1)
:
Natural families from module maps #
def
MultiplicativeBasisDeformations.CatAlg.MeshData.Supp
{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]
{L : LocalFamily F}
{D : MeshData F L}
(Dg : HomGrading F G)
(T : Finset (D.PV × G))
(X : ι × G)
:
T contains the support of V_X̃.
Instances For
structure
MultiplicativeBasisDeformations.CatAlg.MeshData.ScFam
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
(d : D.PV × G → D.PV × G → k)
(X Y : ι × G)
:
Type u
A family of maps C̃(P_z, X̃) → C̃(P_z, Ỹ) scaled by d along L.
- φ (z : D.PV × G) : (F ↑z.1 ⟶ F X.1) →ₗ[k] F ↑z.1 ⟶ F Y.1
Instances For
def
MultiplicativeBasisDeformations.CatAlg.MeshData.ScFam.toNatFam
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{X Y : ι × G}
(N : ScFam (fun (x x_1 : D.PV × G) => 1) X Y)
:
D.NatFam Dg X Y
An unscaled family is natural.
Instances For
def
MultiplicativeBasisDeformations.CatAlg.MeshData.famOf
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
(T : Finset (D.PV × G))
{X Y : ι × G}
(f : D.VX Dg T X →ₗ[k] D.VX Dg T Y)
(z : D.PV × G)
:
(F ↑z.1 ⟶ F X.1) →ₗ[k] F ↑z.1 ⟶ F Y.1
The components of a map V_X̃|_T → V_Ỹ|_T, extended by zero.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.famOf_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{Y : ι × G}
(f : D.VX Dg T X →ₗ[k] D.VX Dg T Y)
{z : D.PV × G}
(hz : z ∈ T)
{m : F ↑z.1 ⟶ F X.1}
(hm : m ∈ Dg.part (z.2⁻¹ * X.2) (↑z.1) X.1)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.famOf_mem
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{Y : ι × G}
(f : D.VX Dg T X →ₗ[k] D.VX Dg T Y)
(z : D.PV × G)
(m : F ↑z.1 ⟶ F X.1)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.eq_zero_of_supp
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(hX : Supp Dg T X)
{z : D.PV × G}
(hz : z ∉ T)
{m : F ↑z.1 ⟶ F X.1}
(hm : m ∈ Dg.part (z.2⁻¹ * X.2) (↑z.1) X.1)
:
m = 0
def
MultiplicativeBasisDeformations.CatAlg.MeshData.scFamOf
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{d : D.PV × G → D.PV × G → k}
{Y : ι × G}
{f : D.VX Dg T X →ₗ[k] D.VX Dg T Y}
(hX : Supp Dg T X)
(hY : Supp Dg T Y)
(hf : IsScaled d f)
:
ScFam d X Y
A scaled module map gives a scaled family.
Instances For
Indecomposability #
def
MultiplicativeBasisDeformations.CatAlg.MeshData.homK
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X Y : ι × G}
(θ : D.VM Dg T X ⟶ D.VM Dg T Y)
:
A module map as a k-linear map for the native structures.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.homK_isScaled
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{Y : ι × G}
(θ : D.VM Dg T X ⟶ D.VM Dg T Y)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.end_eq_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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(H : HeightData Dg)
(hX : Supp Dg T X)
(θ : D.VM Dg T X ⟶ D.VM Dg T X)
:
∃ (c : k), ∀ (y : D.VX Dg T X), (ModuleCat.Hom.hom θ) y = c • y
Endomorphisms of V_X̃ are scalars ("Height gives End(V_X̃) = k").
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.exists_ne_zero
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(hX : Supp Dg T X)
(h1 : CategoryTheory.CategoryStruct.id (F X.1) ≠ 0)
:
∃ (y : D.VX Dg T X), y ≠ 0
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.VM_isFiniteIndecomposable
{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]
{L : LocalFamily F}
{D : MeshData F L}
{Dg : HomGrading F G}
{T : Finset (D.PV × G)}
{X : ι × G}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(H : HeightData Dg)
(hX : Supp Dg T X)
(h1 : CategoryTheory.CategoryStruct.id (F X.1) ≠ 0)
:
IsFiniteIndecomposable k (↥(D.covT Dg T)) (D.VM Dg T X)
V_X̃|_T is finite-dimensional and indecomposable.