Projective irreducibles and first radical layers

The internal irreducible quotient between selected indecomposable projectives is identified with the Hom space into the first radical layer of the target. For a biserial complete primitive-projective presentation this gives the ordinary-quiver out-degree bound.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryProjectiveFGHom {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) : S.fgObj y.label ⟶ S.fgObj x.label

The underlying finitely generated module map of a morphism in the selected projective subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.range_le_jacobson_of_mem_projectiveRadical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) (hf : f ∈ S.projectiveRadicalSubmodule x y) : (ModuleCat.Hom.hom (S.ordinaryProjectiveFGHom f).hom).range ≤ Module.jacobson Aᵐᵒᵖ ↑(S.fgObj x.label)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_projectiveRadical_of_range_le_jacobson {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) (hf : (ModuleCat.Hom.hom (S.ordinaryProjectiveFGHom f).hom).range ≤ Module.jacobson Aᵐᵒᵖ ↑(S.fgObj x.label)) : f ∈ S.projectiveRadicalSubmodule x y

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_projectiveRadical_iff_range_le_jacobson {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x) : f ∈ S.projectiveRadicalSubmodule x y ↔ (ModuleCat.Hom.hom (S.ordinaryProjectiveFGHom f).hom).range ≤ Module.jacobson Aᵐᵒᵖ ↑(S.fgObj x.label)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalBoundaryHomEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : ↥(S.projectiveRadicalSubmodule x y) ≃ₗ[k] S.fgObj y.label ⟶ S.projectiveBoundaryRadical x.label

Radical maps between selected projectives are canonically the maps into the boundary radical of the target projective.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveBoundaryRadicalTop {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : S.ProjectiveLabel) : FGModuleCat Aᵐᵒᵖ

The first radical layer of a selected projective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalToBoundaryTopHom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : ↥(S.projectiveRadicalSubmodule x y) →ₗ[k] S.fgObj y.label ⟶ S.projectiveBoundaryRadicalTop x

A radical projective map, factored through the boundary radical, and then projected to the first radical layer.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalToBoundaryTopHom_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Function.Surjective ⇑(S.projectiveRadicalToBoundaryTopHom x y)

Projectivity of the source makes the map from radical morphisms onto maps into the first boundary-radical layer surjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalToBoundaryTopHom_comp_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y z : S.ProjectiveLabel} (g : S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj z) (h : S.ordinaryProjectiveObj z ⟶ S.ordinaryProjectiveObj x) (hg : g ∈ S.projectiveRadicalSubmodule z y) (hh : h ∈ S.projectiveRadicalSubmodule x z) : (S.projectiveRadicalToBoundaryTopHom x y) ⟨CategoryTheory.CategoryStruct.comp g h, ⋯⟩ = 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRadicalSquareInRadical_le_ker_boundaryTop {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : S.projectiveRadicalSquareInRadicalSubmodule x y ≤ (S.projectiveRadicalToBoundaryTopHom x y).ker

Every product of two radical maps between selected projectives vanishes after passage to the first radical layer of the target.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveIrrToBoundaryTopHom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : S.projectiveIrreducibleHomSpace x y →ₗ[k] S.fgObj y.label ⟶ S.projectiveBoundaryRadicalTop x

The canonical map from the internal projective irreducible quotient to maps into the first radical layer.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveIrrToBoundaryTopHom_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Function.Surjective ⇑(S.projectiveIrrToBoundaryTopHom x y)

Every map from a selected projective into the first radical layer lifts to an internal irreducible class.

theorem MagnitudeConjecture.MinimalProjectivePresentation.kernel_le_jacobson {R : Type u} [Ring R] [IsNoetherianRing R] {M : FGModuleCat R} (P : MinimalProjectivePresentation M) : (ModuleCat.Hom.hom P.f.hom).ker ≤ Module.jacobson R ↑P.p

The kernel of a projective cover lies in the Jacobson radical of its projective source.

theorem MagnitudeConjecture.MinimalProjectivePresentation.comap_jacobson_eq {R : Type u} [Ring R] [IsNoetherianRing R] {M : FGModuleCat R} (P : MinimalProjectivePresentation M) : Submodule.comap (ModuleCat.Hom.hom P.f.hom) (Module.jacobson R ↑M) = Module.jacobson R ↑P.p

A projective cover pulls the Jacobson radical of its target back to the Jacobson radical of its projective source.

theorem MagnitudeConjecture.MinimalProjectivePresentation.map_jacobson_eq {R : Type u} [Ring R] [IsNoetherianRing R] {M : FGModuleCat R} (P : MinimalProjectivePresentation M) : Submodule.map (ModuleCat.Hom.hom P.f.hom) (Module.jacobson R ↑P.p) = Module.jacobson R ↑M

A projective cover maps the Jacobson radical of its source onto that of its target.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.boundaryRestrictedModule {k A : Type u} [Field k] [Ring A] [Algebra k A] (X : FinitelyGeneratedCategory A) : Module k ↑X

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.boundaryRestrictedScalarTower {k A : Type u} [Field k] [Ring A] [Algebra k A] (X : FinitelyGeneratedCategory A) : IsScalarTower k Aᵐᵒᵖ ↑X

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.boundaryHom_comp_inclusion_mem_projectiveRadicalSquare {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : S.ProjectiveLabel} (a : S.fgObj y.label ⟶ S.projectiveBoundaryRadical x.label) (ha : (ModuleCat.Hom.hom a.hom).range ≤ Module.jacobson Aᵐᵒᵖ ↑(S.projectiveBoundaryRadical x.label)) : CategoryTheory.InducedCategory.homMk (CategoryTheory.CategoryStruct.comp a (S.projectiveBoundaryRadicalInclusion x.label)) ∈ S.projectiveRadicalSquareSubmodule x y

A map into the boundary radical whose image lies in its Jacobson radical becomes a product of two radical maps in the selected-projective subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ker_boundaryTop_le_projectiveRadicalSquareInRadical {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : (S.projectiveRadicalToBoundaryTopHom x y).ker ≤ S.projectiveRadicalSquareInRadicalSubmodule x y

A radical map killed on the first boundary-radical layer already lies in the square of the radical formed inside the selected-projective category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ker_projectiveRadicalToBoundaryTopHom {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : (S.projectiveRadicalToBoundaryTopHom x y).ker = S.projectiveRadicalSquareInRadicalSubmodule x y

The kernel of restriction to the first boundary-radical layer is exactly the internal square of the selected-projective radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveIrrToBoundaryTopHom_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : Function.Injective ⇑(S.projectiveIrrToBoundaryTopHom x y)

The map from internal irreducible classes to the first boundary-radical layer is injective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveIrrBoundaryTopHomEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) : S.projectiveIrreducibleHomSpace x y ≃ₗ[k] S.fgObj y.label ⟶ S.projectiveBoundaryRadicalTop x

Internal irreducible maps into a selected projective are canonically the maps from the source projective into the first radical layer of the target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sum_finrank_projectiveIrreducibleHomSpace_eq_boundaryTop_finrank {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (P : S.PrimitiveProjectivePresentation) (x : S.ProjectiveLabel) : ∑ y : S.ProjectiveLabel, Module.finrank k (S.projectiveIrreducibleHomSpace x y) = Module.finrank k ↑(S.projectiveBoundaryRadicalTop x)

Summing the dimensions of all internal irreducible maps into a selected projective recovers the dimension of its first radical layer.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.boundaryRadicalTop_length_le_two_of_isBiserial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsNoetherianRing A] (P : S.PrimitiveProjectivePresentation) (hP : P.IsBiserial) (x : S.ProjectiveLabel) : Module.length Aᵐᵒᵖ ↑(S.projectiveBoundaryRadicalTop x) ≤ 2

Biseriality of the complete primitive presentation bounds the composition length of the first radical layer of each selected projective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.boundaryRadicalTop_finrank_le_two_of_isBiserial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsNoetherianRing A] [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hP : P.IsBiserial) (x : S.ProjectiveLabel) : Module.finrank k ↑(S.projectiveBoundaryRadicalTop x) ≤ 2

Over the algebraically closed ground field, the first radical layer of a biserial selected projective has vector-space dimension at most two.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryStar_card_le_two_of_primitiveProjectivePresentation_isBiserial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsNoetherianRing A] [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hP : P.IsBiserial) (x : S.ProjectiveLabel) : Nat.card (Quiver.Star x) ≤ 2

A biserial complete primitive presentation has ordinary-quiver out-degree at most two at every selected projective.