The projective boundary of the finite functor category

For an object with local endomorphism ring, the categorical radical rad(X,-) is a linear subfunctor of the covariant representable Hom(X,-). When the representable is finite, its inclusion is the canonical right almost-split morphism ending at that indecomposable projective.

noncomputable def MagnitudeConjecture.CoveringHom.radicalLinearCoyoneda {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Functor C (ModuleCat k)

The covariant categorical-radical subfunctor of a representable.

instance MagnitudeConjecture.CoveringHom.radicalLinearCoyoneda_additive {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : (radicalLinearCoyoneda X).Additive

instance MagnitudeConjecture.CoveringHom.radicalLinearCoyoneda_linear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Functor.Linear k (radicalLinearCoyoneda X)

noncomputable def MagnitudeConjecture.CoveringHom.radicalLinearCoyonedaLinearModule {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : LinearModuleCategory k

The radical representable bundled as an additive linear module.

noncomputable def MagnitudeConjecture.CoveringHom.radicalLinearCoyonedaInclusionNatTrans {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : radicalLinearCoyoneda X ⟶ (CategoryTheory.linearCoyoneda k C).obj (Opposite.op X)

The canonical inclusion rad(X,-) ⟶ Hom(X,-) as an ordinary natural transformation.

def MagnitudeConjecture.CoveringHom.radicalLinearCoyonedaSourceEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) {X Z : C} (e : X ≅ Z) : ↥(CategoryTheory.radicalHomSubmodule k X Y) ≃ₗ[k] ↥(CategoryTheory.radicalHomSubmodule k Z Y)

Precomposition by an isomorphism transports the radical Hom subspace.

@[simp]

theorem MagnitudeConjecture.CoveringHom.radicalLinearCoyonedaSourceEquiv_apply_val {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) {X Z : C} (e : X ≅ Z) (f : ↥(CategoryTheory.radicalHomSubmodule k X Y)) : ↑((radicalLinearCoyonedaSourceEquiv Y e) f) = CategoryTheory.CategoryStruct.comp e.inv ↑f

@[simp]

theorem MagnitudeConjecture.CoveringHom.radicalLinearCoyoneda_map_apply_val {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) {Y Z : C} (f : Y ⟶ Z) (q : ↥(CategoryTheory.radicalHomSubmodule k X Y)) : ↑((CategoryTheory.ConcreteCategory.hom ((radicalLinearCoyoneda X).map f)) q) = CategoryTheory.CategoryStruct.comp (↑q) f

noncomputable def MagnitudeConjecture.CoveringHom.radicalLinearCoyonedaMapIso {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Z : C} (e : X ≅ Z) : radicalLinearCoyoneda X ≅ radicalLinearCoyoneda Z

An isomorphism of representing objects transports their radical representables by precomposition.

theorem MagnitudeConjecture.CoveringHom.radicalLinearCoyonedaMapIso_hom_comp_inclusion {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {X Z : C} (e : X ≅ Z) : CategoryTheory.CategoryStruct.comp (radicalLinearCoyonedaMapIso e).hom (radicalLinearCoyonedaInclusionNatTrans Z) = CategoryTheory.CategoryStruct.comp (radicalLinearCoyonedaInclusionNatTrans X) ((CategoryTheory.linearCoyoneda k C).mapIso e.symm.op).hom

Transport of a radical representable along a representing-object isomorphism commutes with its inclusion into the full representable.

noncomputable def MagnitudeConjecture.CoveringHom.radicalLinearCoyonedaInclusion {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : radicalLinearCoyonedaLinearModule X ⟶ linearCoyonedaLinearModule X

The canonical inclusion rad(X,-) ⟶ Hom(X,-), bundled in the category of additive linear modules.

instance MagnitudeConjecture.CoveringHom.radicalLinearCoyonedaInclusion_mono {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Mono (radicalLinearCoyonedaInclusion X)

theorem MagnitudeConjecture.CoveringHom.radicalLinearCoyoneda_isFiniteDimensionalModule {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) (hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : IsFiniteDimensionalModule k (radicalLinearCoyonedaLinearModule X)

The radical subfunctor of a finite representable is again a finite module.

noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaRadical {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) (hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensionalModuleCategory k

The finite categorical radical of a finite representable.

noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaRadicalInclusion {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) (hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : finiteDimensionalLinearCoyonedaRadical X hX ⟶ finiteDimensionalLinearCoyoneda X hX

The finite radical inclusion into a finite representable.

instance MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaRadicalInclusion_mono {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) (hX : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Mono (finiteDimensionalLinearCoyonedaRadicalInclusion X hX)

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaRadicalInclusion_isRightAlmostSplit {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : C) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (finiteDimensionalLinearCoyonedaRadicalInclusion X ⋯)

The radical inclusion of an indecomposable finite representable is right almost split.