Occurrence bases over an algebraically closed field

For an indecomposable finite-dimensional module over an algebraically closed field, every endomorphism is scalar modulo the categorical radical. This is the precise form of Schur's lemma needed to identify repeated summands in an almost-split middle term with the dimension of the corresponding irreducible morphism space; the endomorphism itself need not be scalar.

@[instance_reducible]

def MBDVendor.QSE.IndecomposableSkeleton.restrictedModule {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) (i : Iota) : Module K ↑(sigma.obj i)

theorem MBDVendor.QSE.IndecomposableSkeleton.restrictedScalarTower {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) (i : Iota) : IsScalarTower K R ↑(sigma.obj i)

theorem MBDVendor.QSE.IndecomposableSkeleton.exists_scalar_sub_mem_radicalHom {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) (x : Iota) (f : sigma.obj x ⟶ sigma.obj x) : ∃ (a : K), ModuleCat.Hom.hom f.hom - a • LinearMap.id ∈ sigma.radicalHom x x

Over an algebraically closed field, an endomorphism of an indecomposable finite-dimensional module differs from a scalar by a radical endomorphism.

theorem MBDVendor.QSE.IndecomposableSkeleton.exists_scalar_sub_isRadicalMorphism {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) (x : Iota) (f : sigma.obj x ⟶ sigma.obj x) : ∃ (a : K), CategoricalRadical.IsRadicalMorphism (f - a • CategoryTheory.CategoryStruct.id (sigma.obj x))

Over an algebraically closed field, an endomorphism of a chosen indecomposable differs from a scalar identity by a categorical-radical morphism.

theorem MBDVendor.QSE.IndecomposableSkeleton.rightAROccurrenceToIrr_surjective_of_scalar_mod_radical {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) (hscalar : ∀ (f : sigma.obj x ⟶ sigma.obj x), ∃ (a : K), ModuleCat.Hom.hom f.hom - a • LinearMap.id ∈ sigma.radicalHom x x) : Function.Surjective ⇑(sigma.rightAROccurrenceToIrr A x)

The right almost-split occurrence coordinates span Irr when source endomorphisms are scalar modulo the radical.

noncomputable def MBDVendor.QSE.IndecomposableSkeleton.rightAROccurrenceLinearEquivOfIsAlgClosed {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : (sigma.RightAROccurrence A x → K) ≃ₗ[K] sigma.irreducibleHomSpace x z

Over an algebraically closed field, right almost-split occurrences form a basis of the corresponding irreducible-morphism space.

theorem MBDVendor.QSE.IndecomposableSkeleton.finrank_irreducibleHomSpace_eq_card_rightAROccurrence_of_isAlgClosed {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {z : Iota} (A : sigma.MinimalRightAlmostSplitDecomposition z) (x : Iota) : Module.finrank K (sigma.irreducibleHomSpace x z) = Nat.card (sigma.RightAROccurrence A x)

The dimension of Irr(x,z) is the number of occurrences of x in a minimal right almost-split middle term over an algebraically closed field.

theorem MBDVendor.QSE.IndecomposableSkeleton.leftAROccurrenceToIrr_surjective_of_scalar_mod_radical {K R : Type u} [Field K] [Ring R] [Algebra K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) (hscalar : ∀ (f : sigma.obj y ⟶ sigma.obj y), ∃ (a : K), ModuleCat.Hom.hom f.hom - a • LinearMap.id ∈ sigma.radicalHom y y) : Function.Surjective ⇑(sigma.leftAROccurrenceToIrr A y)

The left almost-split occurrence coordinates span Irr when target endomorphisms are scalar modulo the radical.

noncomputable def MBDVendor.QSE.IndecomposableSkeleton.leftAROccurrenceLinearEquivOfIsAlgClosed {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : (sigma.LeftAROccurrence A y → K) ≃ₗ[K] sigma.irreducibleHomSpace x y

Over an algebraically closed field, left almost-split occurrences form a basis of the corresponding irreducible-morphism space.

theorem MBDVendor.QSE.IndecomposableSkeleton.finrank_irreducibleHomSpace_eq_card_leftAROccurrence_of_isAlgClosed {K R : Type u} [Field K] [IsAlgClosed K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] {Iota : Type v} (sigma : IndecomposableSkeleton R Iota) {x : Iota} (A : sigma.MinimalLeftAlmostSplitDecomposition x) (y : Iota) : Module.finrank K (sigma.irreducibleHomSpace x y) = Nat.card (sigma.LeftAROccurrence A y)

The dimension of Irr(x,y) is the number of occurrences of y in a minimal left almost-split middle term over an algebraically closed field.