Lemma 2.9: vanishing on modules killed by e #
lem:projective-evaluation-criterion (graded-category.tex): "Assume
Hom_Λ(T, Λ) = Ext¹_Λ(T, Λ) = 0 whenever Te = 0. … It suffices to check the
two vanishings on the simple Λ-modules killed by e. … composition series and
the long exact sequences extend the two vanishings from the simples to every
module killed by e." In the proof of Proposition 2.10 the simples killed by
e are the tops L_x at nonprojective labels, where the vanishings come from
the exact right meshes (MeshData.hom_top_eq_zero, MeshData.extend_top).
Here e is the sum of the idempotents at the projective labels; a module is
killed by e when every projective idempotent acts by zero. Ext¹ = 0 is used
in extension form: maps into R_w extend from a submodule with quotient
killed by e.
instance
MultiplicativeBasisDeformations.CatAlg.instFiniteDimensionalRepOfHom
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
{F : ι → 𝒞}
(X : 𝒞)
[∀ (y : ι), FiniteDimensional k (F y ⟶ X)]
:
FiniteDimensional k (Rep F X)
def
MultiplicativeBasisDeformations.CatAlg.MeshData.KilledSub
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
(D : MeshData F L)
{M : Type u_1}
[AddCommGroup M]
[Module (Alg F) M]
(U : Submodule (Alg F) M)
:
A submodule with quotient killed by the projective idempotents.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.exists_atom_le
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{T : Type u_1}
[AddCommGroup T]
[Module k T]
[Module (Alg F) T]
[IsScalarTower k (Alg F) T]
[FiniteDimensional k T]
{N : Submodule (Alg F) T}
(hN : N ≠ ⊥)
:
∃ (S : Submodule (Alg F) T), IsAtom S ∧ S ≤ N
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.top_mk_ne_zero
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{L : LocalFamily F}
(x : ι)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.idem_smul_top_mk
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{L : LocalFamily F}
(x : ι)
:
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.exists_iso_top_nonproj
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{L : LocalFamily F}
(D : MeshData F L)
{S : Type u_1}
[AddCommGroup S]
[Module (Alg F) S]
[IsSimpleModule (Alg F) S]
(hS : ∀ (x : ι), D.proj x → ∀ (s : S), idem x • s = 0)
:
A simple module on which the projective idempotents act by zero is a top at a nonprojective label.
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.hom_eq_zero_of_killed
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{L : LocalFamily F}
(D : MeshData F L)
{T : Type u_1}
[AddCommGroup T]
[Module k T]
[Module (Alg F) T]
[IsScalarTower k (Alg F) T]
[FiniteDimensional k T]
(hT : ∀ (x : ι), D.proj x → ∀ (t : T), idem x • t = 0)
(w : ι)
(θ : T →ₗ[Alg F] Rep F (F w))
:
θ = 0
Hom(T, R_w) = 0 for T killed by e.
def
MultiplicativeBasisDeformations.CatAlg.MeshData.ExtP
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{M : Type u_1}
[AddCommGroup M]
[Module (Alg F) M]
(w : ι)
(U V : Submodule (Alg F) M)
(h : U ≤ V)
:
Maps into R_w extend from U to V.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.ExtP.trans
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{M : Type u_1}
[AddCommGroup M]
[Module (Alg F) M]
{w : ι}
{U V W : Submodule (Alg F) M}
{h₁ : U ≤ V}
{h₂ : V ≤ W}
(e₁ : ExtP w U V h₁)
(e₂ : ExtP w V W h₂)
:
ExtP w U W ⋯
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.extP_of_top
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{L : LocalFamily F}
(D : MeshData F L)
{M : Type u_1}
[AddCommGroup M]
[Module k M]
[Module (Alg F) M]
[IsScalarTower k (Alg F) M]
(w : ι)
{U V : Submodule (Alg F) M}
(h : U ≤ V)
(x : ι)
(hx : ¬D.proj x)
(e : (↥V ⧸ Submodule.comap V.subtype U) ≃ₗ[Alg F] L.Top x)
:
ExtP w U V h
One step: a simple quotient at a nonprojective label.
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.extP_top_of_killed
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{L : LocalFamily F}
(D : MeshData F L)
{M : Type u_1}
[AddCommGroup M]
[Module k M]
[Module (Alg F) M]
[IsScalarTower k (Alg F) M]
[FiniteDimensional k M]
(w : ι)
(U : Submodule (Alg F) M)
(hU : D.KilledSub U)
:
ExtP w U ⊤ ⋯
Ext¹(T, R_w) = 0 for T killed by e, in extension form.