Simple tops of indecomposable projective modules

The original simple module S_x = P_x / rad P_x of a projective label (graded-category.tex) and the identity dim Hom_A(P_y, S_x) = δ_{xy} used in the proof of Proposition 2.10. The code adapts general module theory from the magnitude-conjecture formalization (Algebra/RightModuleSimpleTop.lean and Algebra/RightModuleBasicSimpleDimension.lean), stated here for an IndSkeleton.

theorem MultiplicativeBasisDeformations.fgModule_simple_of_isSimpleModule {R : Type u} [Ring R] [IsNoetherianRing R] (X : FGModuleCat R) [IsSimpleModule R ↑X] : CategoryTheory.Simple X

A simple module carried by FGModuleCat is a simple object.

def MultiplicativeBasisDeformations.IndSkeleton.radQuot {A : Type u} [Ring A] (P : ModCat A) : ModCat A

The quotient of a finite module by its module Jacobson radical.

def MultiplicativeBasisDeformations.IndSkeleton.radQuotProj {A : Type u} [Ring A] (P : ModCat A) : P ⟶ radQuot P

The quotient map to the module-Jacobson-radical quotient.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.top {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x : Fin S.n) : ModCat A

The radical quotient S_x = P_x / rad P_x.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.topProj {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x : Fin S.n) : S.fg x ⟶ S.top x

The projection P_x → S_x.

instance MultiplicativeBasisDeformations.IndSkeleton.topProj_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x : Fin S.n) : CategoryTheory.Epi (S.topProj x)

theorem MultiplicativeBasisDeformations.IndSkeleton.topProj_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (hx : CategoryTheory.Projective (S.fg x)) : S.topProj x ≠ 0

theorem MultiplicativeBasisDeformations.IndSkeleton.top_isSimpleModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (hx : CategoryTheory.Projective (S.fg x)) : IsSimpleModule Aᵐᵒᵖ ↑(S.top x)

theorem MultiplicativeBasisDeformations.IndSkeleton.top_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : Fin S.n) (hx : CategoryTheory.Projective (S.fg x)) : CategoryTheory.Indecomposable (S.top x)

theorem MultiplicativeBasisDeformations.IndSkeleton.hom_top_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (p q : Fin S.n) (hp : CategoryTheory.Projective (S.fg p)) (hq : CategoryTheory.Projective (S.fg q)) (hqp : q ≠ p) (f : S.fg q ⟶ S.top p) : f = 0

A distinct indecomposable projective has no map to the simple top of p.

theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_hom_top_self {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) [IsAlgClosed k] (p : Fin S.n) (hp : CategoryTheory.Projective (S.fg p)) : Module.finrank k (S.fg p ⟶ S.top p) = 1

The projective P_p maps one-dimensionally to its simple top.

theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_hom_top {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) [IsAlgClosed k] (p q : Fin S.n) (hp : CategoryTheory.Projective (S.fg p)) (hq : CategoryTheory.Projective (S.fg q)) : Module.finrank k (S.fg q ⟶ S.top p) = if q = p then 1 else 0

dim Hom_A(P_q, S_p) = δ_{qp}.