Lemma 2.9 for an arbitrary finite-dimensional algebra #
lem:projective-evaluation-criterion (graded-category.tex): "Let Λ be a
finite-dimensional algebra over any field, let e be an idempotent, and put Λ_e = eΛe. Assume
Hom_Λ(T, Λ) = Ext¹_Λ(T, Λ) = 0 whenever Te = 0. Then P ↦ Pe is fully faithful on proj Λ.
If gl.dim Λ ≤ 2 and every finite-dimensional injective Λ_e-module is Qe for some projective
Λ-module Q, this functor is an equivalence proj Λ ≃ mod Λ_e. In particular, Λ_e is
representation-finite. It suffices to check the two vanishings on the simple Λ-modules killed
by e."
Conventions. The manuscript's right Λ-modules are the left modules over R = Λᵐᵒᵖ, and Me is
ε M for ε = op e; so we work with left modules over an arbitrary finite-dimensional algebra
R and an idempotent ε. Λ_e is Mathlib's corner ring hε.Corner (ε R ε, with unit ε),
and ε M is a Λ_e-module (EP); evaluation is EPmap. Ext¹_R(T, Q) = 0 is taken in Yoneda
form: every extension 0 → Q → E → T → 0 splits (ExtVan). gl.dim R ≤ 2 is used, as in the
proof, through "a second syzygy is projective": the kernel of a map between finitely generated
projectives is projective.
The proof is the source's, without tensor products (as in ProjectiveEvaluation.lean): a map
g : εM → εQ is defined on the submodule generated by εM by ∑ λ_i m_i ↦ ∑ λ_i g(m_i), well
defined because the discrepancy is a submodule of Q killed by ε; it extends to M because
M / R εM is killed by ε (Ext¹); injectivity is the Hom-vanishing for M / R εM.
def
MultiplicativeBasisDeformations.EvalCriterion.Killed
{R : Type u}
[Ring R]
(ε : R)
(M : Type u_1)
[AddCommGroup M]
[Module R M]
:
A module killed by ε.
Instances For
def
MultiplicativeBasisDeformations.EvalCriterion.SplitsFor
(k : Type u)
[Field k]
(R : Type u)
[Ring R]
[Algebra k R]
(T Q : Type u)
[AddCommGroup T]
[Module R T]
[AddCommGroup Q]
[Module R Q]
:
Ext¹_R(T, Q) = 0 in Yoneda form: every extension 0 → Q → E → T → 0 of
finite-dimensional modules splits.
Instances For
Yoneda splitting gives the extension form (pushout) #
def
MultiplicativeBasisDeformations.EvalCriterion.pushRel
{R : Type u}
[Ring R]
{Q : Type u}
[AddCommGroup Q]
[Module R Q]
{M : Type u}
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(g : ↥N →ₗ[R] Q)
:
Submodule R (Q × M)
The pushout relations (g n, -n).
Instances For
theorem
MultiplicativeBasisDeformations.EvalCriterion.extend_of_splits
{k : Type u}
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{Q : Type u}
[AddCommGroup Q]
[Module k Q]
[Module R Q]
[IsScalarTower k R Q]
[FiniteDimensional k Q]
{M : Type u}
[AddCommGroup M]
[Module k M]
[Module R M]
[IsScalarTower k R M]
[FiniteDimensional k M]
(N : Submodule R M)
(h : SplitsFor k R (M ⧸ N) Q)
(g : ↥N →ₗ[R] Q)
:
∃ (g' : M →ₗ[R] Q), ∀ (n : ↥N), g' ↑n = g n
Splitting of the pushout extends maps.
Transfer to finitely generated projectives #
theorem
MultiplicativeBasisDeformations.EvalCriterion.homVan_retract
{k : Type u}
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
{F Q : Type u}
[AddCommGroup F]
[Module R F]
[AddCommGroup Q]
[Module R Q]
(s : Q →ₗ[R] F)
(r : F →ₗ[R] Q)
(hrs : r ∘ₗ s = LinearMap.id)
(h : HomVan k ε F)
:
HomVan k ε Q
theorem
MultiplicativeBasisDeformations.EvalCriterion.extExt_retract
{k : Type u}
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
{F Q : Type u}
[AddCommGroup F]
[Module R F]
[AddCommGroup Q]
[Module R Q]
(s : Q →ₗ[R] F)
(r : F →ₗ[R] Q)
(hrs : r ∘ₗ s = LinearMap.id)
(h : ExtExt k ε F)
:
ExtExt k ε Q
theorem
MultiplicativeBasisDeformations.EvalCriterion.exists_retract
{R : Type u}
[Ring R]
{Q : Type u}
[AddCommGroup Q]
[Module R Q]
[Module.Finite R Q]
[Module.Projective R Q]
:
∃ (n : ℕ) (s : Q →ₗ[R] Fin n → R) (r : (Fin n → R) →ₗ[R] Q), r ∘ₗ s = LinearMap.id
A finitely generated projective module is a retract of some R^n.
theorem
MultiplicativeBasisDeformations.EvalCriterion.van_proj
{k : Type u}
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
{Q : Type u}
[AddCommGroup Q]
[Module R Q]
[FiniteDimensional k R]
[Module.Finite R Q]
[Module.Projective R Q]
(h0 : HomVan k ε R)
(h1 : ExtVan k ε R)
:
The vanishings transfer from R to every finitely generated projective.
The corner Λ_e and the evaluation M ↦ εM #
theorem
MultiplicativeBasisDeformations.EvalCriterion.corner_left
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
(c : hε.Corner)
:
ε * ↑c = ↑c
theorem
MultiplicativeBasisDeformations.EvalCriterion.corner_right
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
(c : hε.Corner)
:
↑c * ε = ↑c
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.corner_one
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
:
↑1 = ε
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.corner_mul
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
(a b : hε.Corner)
:
↑(a * b) = ↑a * ↑b
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.corner_add
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
(a b : hε.Corner)
:
↑(a + b) = ↑a + ↑b
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.corner_zero
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
:
↑0 = 0
def
MultiplicativeBasisDeformations.EvalCriterion.cor
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
(r : R)
:
hε.Corner
The corner element ε r ε.
Instances For
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.cor_val
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
(r : R)
:
↑(cor hε r) = ε * r * ε
def
MultiplicativeBasisDeformations.EvalCriterion.EPsub
{R : Type u}
[Ring R]
(ε : R)
(M : Type u)
[AddCommGroup M]
[Module R M]
:
AddSubgroup M
εM as an additive group.
Instances For
def
MultiplicativeBasisDeformations.EvalCriterion.EP
{R : Type u}
[Ring R]
{ε : R}
(_hε : IsIdempotentElem ε)
(M : Type u)
[AddCommGroup M]
[Module R M]
:
Type u
εM as a Λ_e-module: the evaluation of M.
Instances For
@[instance_reducible]
instance
MultiplicativeBasisDeformations.EvalCriterion.instAddCommGroupEP
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
(M : Type u)
[AddCommGroup M]
[Module R M]
:
AddCommGroup (EP hε M)
theorem
MultiplicativeBasisDeformations.EvalCriterion.EP_spec
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
{M : Type u}
[AddCommGroup M]
[Module R M]
(m : EP hε M)
:
ε • ↑m = ↑m
@[instance_reducible]
instance
MultiplicativeBasisDeformations.EvalCriterion.instModuleCornerEP
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
{M : Type u}
[AddCommGroup M]
[Module R M]
:
Module hε.Corner (EP hε M)
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.EP_smul_val
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
{M : Type u}
[AddCommGroup M]
[Module R M]
(c : hε.Corner)
(m : EP hε M)
:
↑(c • m) = ↑c • ↑m
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.EP_add_val
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
{M : Type u}
[AddCommGroup M]
[Module R M]
(a b : EP hε M)
:
↑(a + b) = ↑a + ↑b
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.EP_zero_val
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
{M : Type u}
[AddCommGroup M]
[Module R M]
:
↑0 = 0
def
MultiplicativeBasisDeformations.EvalCriterion.epOf
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
{M : Type u}
[AddCommGroup M]
[Module R M]
(m : M)
:
EP hε M
The element ε m of εM.
Instances For
def
MultiplicativeBasisDeformations.EvalCriterion.EPmap
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
{M : Type u}
[AddCommGroup M]
[Module R M]
{N : Type u}
[AddCommGroup N]
[Module R N]
(f : M →ₗ[R] N)
:
Evaluation of a map: restriction to εM.
Instances For
Full faithfulness on projectives #
theorem
MultiplicativeBasisDeformations.EvalCriterion.fd_sub
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{Q : Type u}
[AddCommGroup Q]
[Module k Q]
[Module R Q]
[IsScalarTower k R Q]
[FiniteDimensional k Q]
(L : Submodule R Q)
:
FiniteDimensional k ↥L
theorem
MultiplicativeBasisDeformations.EvalCriterion.killed_quot
{R : Type u}
[Ring R]
{ε : R}
{M : Type u}
[AddCommGroup M]
[Module R M]
(N : Submodule R M)
(hN : ∀ (m : M), ε • m ∈ N)
:
Killed ε (M ⧸ N)
A submodule containing εM has quotient killed by ε.
def
MultiplicativeBasisDeformations.EvalCriterion.genE
{R : Type u}
[Ring R]
(M : Type u)
[AddCommGroup M]
[Module R M]
(ε : R)
:
Submodule R M
The submodule generated by εM.
Instances For
theorem
MultiplicativeBasisDeformations.EvalCriterion.smul_mem_genE
{R : Type u}
[Ring R]
{ε : R}
(hε : IsIdempotentElem ε)
{M : Type u}
[AddCommGroup M]
[Module R M]
(m : M)
:
ε • m ∈ genE M ε
theorem
MultiplicativeBasisDeformations.EvalCriterion.EPmap_injective
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
{M Q : Type u}
[AddCommGroup M]
[Module k M]
[Module R M]
[IsScalarTower k R M]
[FiniteDimensional k M]
[AddCommGroup Q]
[Module k Q]
[Module R Q]
[IsScalarTower k R Q]
[FiniteDimensional k Q]
(hQ0 : HomVan k ε Q)
:
Function.Injective fun (f : M →ₗ[R] Q) => EPmap hε f
Evaluation is faithful when Hom_R(T, Q) = 0 for T killed by ε.
theorem
MultiplicativeBasisDeformations.EvalCriterion.EPmap_surjective
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
{M Q : Type u}
[AddCommGroup M]
[Module k M]
[Module R M]
[IsScalarTower k R M]
[FiniteDimensional k M]
[AddCommGroup Q]
[Module k Q]
[Module R Q]
[IsScalarTower k R Q]
[FiniteDimensional k Q]
(hQ0 : HomVan k ε Q)
(hQ1 : ExtExt k ε Q)
(g : EP hε M →ₗ[hε.Corner] EP hε Q)
:
∃ (f : M →ₗ[R] Q), EPmap hε f = g
Evaluation is full when moreover Ext¹_R(T, Q) = 0 for T killed by ε
(graded-category.tex, without the tensor product).
It suffices to check the simples #
def
MultiplicativeBasisDeformations.EvalCriterion.SimpleVan
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
(ε : R)
:
The two vanishings on the simple modules killed by ε.
Instances For
theorem
MultiplicativeBasisDeformations.EvalCriterion.extExt_of_simple
{k : Type u}
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
{ε : R}
(h : SimpleVan k ε)
(d : ℕ)
(M : Type u)
[AddCommGroup M]
[Module k M]
[Module R M]
[IsScalarTower k R M]
[FiniteDimensional k M]
(N : Submodule R M)
:
Module.finrank k M - Module.finrank k ↥N = d →
Killed ε (M ⧸ N) → ∀ (g : ↥N →ₗ[R] R), ∃ (g' : M →ₗ[R] R), ∀ (n : ↥N), g' ↑n = g n
Extension from submodules with quotient killed by ε, by induction on the codimension:
extend to a maximal submodule (induction), then across the simple quotient.
The corner over k and the injective module D(Λ_e) #
@[instance_reducible]
instance
MultiplicativeBasisDeformations.EvalCriterion.cornerModuleK
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
Module k hε.Corner
@[simp]
theorem
MultiplicativeBasisDeformations.EvalCriterion.corner_smul_val
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
(c : k)
(x : hε.Corner)
:
↑(c • x) = c • ↑x
instance
MultiplicativeBasisDeformations.EvalCriterion.instIsScalarTowerCorner_multiplicativeBasisDeformations
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
IsScalarTower k hε.Corner hε.Corner
def
MultiplicativeBasisDeformations.EvalCriterion.valK
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
hε.Corner →ₗ[k] R
The inclusion Λ_e → R over k.
Instances For
instance
MultiplicativeBasisDeformations.EvalCriterion.instFiniteDimensionalCorner_multiplicativeBasisDeformations
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
[FiniteDimensional k R]
:
FiniteDimensional k hε.Corner
def
MultiplicativeBasisDeformations.EvalCriterion.mulRightK
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
(a : hε.Corner)
:
hε.Corner →ₗ[k] hε.Corner
Right multiplication on Λ_e, over k.
Instances For
def
MultiplicativeBasisDeformations.EvalCriterion.DC
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
Type u
D(Λ_e) = Hom_k(Λ_e, k).
Instances For
@[instance_reducible]
instance
MultiplicativeBasisDeformations.EvalCriterion.instAddCommGroupDC
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
AddCommGroup (DC k hε)
@[instance_reducible]
instance
MultiplicativeBasisDeformations.EvalCriterion.instModuleDC
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
Module k (DC k hε)
@[instance_reducible]
instance
MultiplicativeBasisDeformations.EvalCriterion.instFunLikeDCCorner
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
FunLike (DC k hε) hε.Corner k
@[instance_reducible]
instance
MultiplicativeBasisDeformations.EvalCriterion.instModuleCornerDC
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
Module hε.Corner (DC k hε)
D(Λ_e) as a left Λ_e-module: (a φ)(s) = φ(s a).
theorem
MultiplicativeBasisDeformations.EvalCriterion.DC_smul_apply
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
(a : hε.Corner)
(φ : DC k hε)
(s : hε.Corner)
:
(have this := a • φ;
this)
s = (have this := φ;
this)
(s * a)
instance
MultiplicativeBasisDeformations.EvalCriterion.instIsScalarTowerCornerDC
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
IsScalarTower k hε.Corner (DC k hε)
instance
MultiplicativeBasisDeformations.EvalCriterion.instFiniteDimensionalDC
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
[FiniteDimensional k R]
:
FiniteDimensional k (DC k hε)
def
MultiplicativeBasisDeformations.EvalCriterion.ev1
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
DC k hε →ₗ[k] k
Evaluation at 1.
Instances For
theorem
MultiplicativeBasisDeformations.EvalCriterion.DC_injective
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
Module.Injective hε.Corner (DC k hε)
D(Λ_e) is injective (Baer's criterion: extend x ↦ g(x)(1) over k).
Essential surjectivity #
def
MultiplicativeBasisDeformations.EvalCriterion.orbK
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
{X : Type u}
[AddCommGroup X]
[Module k X]
[Module hε.Corner X]
[IsScalarTower k hε.Corner X]
(x : X)
:
hε.Corner →ₗ[k] X
s ↦ s x, over k.
Instances For
theorem
MultiplicativeBasisDeformations.EvalCriterion.exists_embed
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
{ε : R}
(hε : IsIdempotentElem ε)
{X : Type u}
[AddCommGroup X]
[Module k X]
[Module hε.Corner X]
[IsScalarTower k hε.Corner X]
[FiniteDimensional k X]
:
∃ (n : ℕ) (ι : X →ₗ[hε.Corner] Fin n → DC k hε), Function.Injective ⇑ι
Every finite-dimensional Λ_e-module embeds in some D(Λ_e)ⁿ.
theorem
MultiplicativeBasisDeformations.EvalCriterion.essSurj
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
{ε : R}
(hε : IsIdempotentElem ε)
(h0 : HomVan k ε R)
(h1 : ExtVan k ε R)
(hgl :
∀ (P₀ P₁ : Type u) [inst : AddCommGroup P₀] [inst_1 : Module k P₀] [inst_2 : Module R P₀] [IsScalarTower k R P₀]
[FiniteDimensional k P₀] [Module.Projective R P₀] [inst_6 : AddCommGroup P₁] [inst_7 : Module k P₁]
[inst_8 : Module R P₁] [IsScalarTower k R P₁] [FiniteDimensional k P₁] [Module.Projective R P₁] (f : P₀ →ₗ[R] P₁),
Module.Projective R ↥f.ker)
(hinj :
∀ (I : Type u) [inst : AddCommGroup I] [inst_1 : Module k I] [inst_2 : Module hε.Corner I]
[IsScalarTower k hε.Corner I] [FiniteDimensional k I],
Module.Injective hε.Corner I →
∃ (Q : Type u) (x : AddCommGroup Q) (x_1 : Module k Q) (x_2 : Module R Q) (_ : IsScalarTower k R Q) (_ :
FiniteDimensional k Q) (_ : Module.Projective R Q), Nonempty (EP hε Q ≃ₗ[hε.Corner] I))
(X : Type u)
[AddCommGroup X]
[Module k X]
[Module hε.Corner X]
[IsScalarTower k hε.Corner X]
[FiniteDimensional k X]
:
Essential surjectivity (graded-category.tex): under the vanishings, if
gl.dim R ≤ 2 (kernels of maps between finitely generated projectives are projective) and every
finite-dimensional injective Λ_e-module is εQ for a projective Q, every
finite-dimensional Λ_e-module is εP for a finite-dimensional projective P.
Primitive decomposition of the unit #
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.EvalCriterion.Rf
{R : Type u}
[Ring R]
(f : R)
:
Submodule R R
The left ideal R f.
Instances For
theorem
MultiplicativeBasisDeformations.EvalCriterion.mem_Rf
{R : Type u}
[Ring R]
{f x : R}
:
x ∈ Rf f ↔ ∃ (a : R), a * f = x
theorem
MultiplicativeBasisDeformations.EvalCriterion.self_mem_Rf
{R : Type u}
[Ring R]
(f : R)
:
f ∈ Rf f
theorem
MultiplicativeBasisDeformations.EvalCriterion.exists_primitive
{k : Type u}
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
(d : ℕ)
(f : R)
:
IsIdempotentElem f →
Module.finrank k ↥(Rf f) = d →
∃ (n : ℕ) (g : Fin n → R),
(∀ (i : Fin n), IsIdempotentElem (g i)) ∧ (∀ (i j : Fin n), i ≠ j → g i * g j = 0) ∧ ∑ i : Fin n, g i = f ∧ (∀ (i : Fin n), g i * f = g i ∧ f * g i = g i) ∧ ∀ (i : Fin n), MBDVendor.QSE.Foundation.IsIndecomposableModule R ↥(Rf (g i))
Every idempotent is a finite orthogonal sum of idempotents g with R g
indecomposable, by induction on the dimension of R f.
Λ_e is representation-finite #
theorem
MultiplicativeBasisDeformations.EvalCriterion.exists_unit_of_sum
{S : Type u_1}
[Ring S]
[IsLocalRing S]
{ι : Type u_2}
(s : Finset ι)
(t : ι → S)
(h : IsUnit (∑ i ∈ s, t i))
:
∃ i ∈ s, IsUnit (t i)
theorem
MultiplicativeBasisDeformations.EvalCriterion.exchange
{k : Type u}
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
{P : Type u}
[AddCommGroup P]
[Module k P]
[Module R P]
[IsScalarTower k R P]
[FiniteDimensional k P]
[Module.Projective R P]
(hP : MBDVendor.QSE.Foundation.IsIndecomposableModule R P)
{n : ℕ}
(g : Fin n → R)
(hsum : ∑ i : Fin n, g i = 1)
(hgd : ∀ (i : Fin n), MBDVendor.QSE.Foundation.IsIndecomposableModule R ↥(Rf (g i)))
:
∃ (i : Fin n), Nonempty (P ≃ₗ[R] ↥(Rf (g i)))
Exchange: an indecomposable finite-dimensional projective module is isomorphic to one of
the indecomposable summands R g_i of a decomposition of 1.
theorem
MultiplicativeBasisDeformations.EvalCriterion.indec_of_EP
{k : Type u}
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
{ε : R}
(hε : IsIdempotentElem ε)
(h0 : HomVan k ε R)
{P : Type u}
[AddCommGroup P]
[Module k P]
[Module R P]
[IsScalarTower k R P]
[FiniteDimensional k P]
[Module.Projective R P]
{X : Type u}
[AddCommGroup X]
[Module hε.Corner X]
(e : EP hε P ≃ₗ[hε.Corner] X)
(hX : MBDVendor.QSE.Foundation.IsIndecomposableModule hε.Corner X)
:
A projective whose evaluation is indecomposable is indecomposable: a summand with zero
evaluation is projective and killed by ε, hence zero by the Hom-vanishing.
Lemma 2.9 #
def
MultiplicativeBasisDeformations.EvalCriterion.GlDimLeTwo
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
:
gl.dim R ≤ 2, in the form used: kernels of maps between finite-dimensional projectives
(second syzygies) are projective.
Instances For
def
MultiplicativeBasisDeformations.EvalCriterion.InjLift
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
{ε : R}
(hε : IsIdempotentElem ε)
:
Every finite-dimensional injective Λ_e-module is εQ for a projective Q.
Instances For
theorem
MultiplicativeBasisDeformations.EvalCriterion.repFinite
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
{ε : R}
(hε : IsIdempotentElem ε)
(h0 : HomVan k ε R)
(h1 : ExtVan k ε R)
(hgl : GlDimLeTwo k)
(hinj : InjLift k hε)
:
∃ (n : ℕ) (L : Fin n → Submodule R R),
∀ (X : Type u) [inst : AddCommGroup X] [inst_1 : Module k X] [inst_2 : Module hε.Corner X]
[IsScalarTower k hε.Corner X] [FiniteDimensional k X],
MBDVendor.QSE.Foundation.IsIndecomposableModule hε.Corner X → ∃ (i : Fin n), Nonempty (EP hε ↥(L i) ≃ₗ[hε.Corner] X)
Λ_e is representation-finite: finitely many left ideals R g_i whose evaluations
represent every finite-dimensional indecomposable Λ_e-module.
theorem
MultiplicativeBasisDeformations.EvalCriterion.projectiveEvaluationCriterion
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
{ε : R}
(hε : IsIdempotentElem ε)
(h0 : HomVan k ε R)
(h1 : ExtVan k ε R)
:
(∀ (M Q : Type u) [inst : AddCommGroup M] [inst_1 : Module k M] [inst_2 : Module R M] [IsScalarTower k R M]
[FiniteDimensional k M] [inst_5 : AddCommGroup Q] [inst_6 : Module k Q] [inst_7 : Module R Q] [IsScalarTower k R Q]
[FiniteDimensional k Q] [Module.Projective R Q], Function.Bijective fun (f : M →ₗ[R] Q) => EPmap hε f) ∧ (GlDimLeTwo k →
InjLift k hε →
(∀ (X : Type u) [inst : AddCommGroup X] [inst_1 : Module k X] [inst_2 : Module hε.Corner X]
[IsScalarTower k hε.Corner X] [FiniteDimensional k X],
∃ (P : Type u) (x : AddCommGroup P) (x_1 : Module k P) (x_2 : Module R P) (_ : IsScalarTower k R P) (_ :
FiniteDimensional k P) (_ : Module.Projective R P), Nonempty (EP hε P ≃ₗ[hε.Corner] X)) ∧ ∃ (n : ℕ) (L : Fin n → Submodule R R),
∀ (X : Type u) [inst : AddCommGroup X] [inst_1 : Module k X] [inst_2 : Module hε.Corner X]
[IsScalarTower k hε.Corner X] [FiniteDimensional k X],
MBDVendor.QSE.Foundation.IsIndecomposableModule hε.Corner X →
∃ (i : Fin n), Nonempty (EP hε ↥(L i) ≃ₗ[hε.Corner] X))
Lemma 2.9 (lem:projective-evaluation-criterion), for any finite-dimensional algebra
R over any field and any idempotent ε (right Λ-modules: R = Λᵐᵒᵖ, ε = op e). Assume
Hom_R(T, R) = Ext¹_R(T, R) = 0 for all finite-dimensional T with εT = 0. Then
(1) P ↦ εP is fully faithful on finite-dimensional projectives (even from any M);
(2) if gl.dim R ≤ 2 and every finite-dimensional injective Λ_e-module is εQ for a
projective Q, it is essentially surjective onto finite-dimensional Λ_e-modules, and
Λ_e = εRε is representation-finite.
theorem
MultiplicativeBasisDeformations.EvalCriterion.projectiveEvaluationCriterion_of_simple
(k : Type u)
[Field k]
{R : Type u}
[Ring R]
[Algebra k R]
[FiniteDimensional k R]
{ε : R}
(h : SimpleVan k ε)
:
It suffices to check the two vanishings on the simple modules killed by ε.