The injective boundary of the finite functor category

For an object with local endomorphism ring, restriction to the categorical radical gives the canonical quotient D Hom(-,X) ⟶ D rad(-,X). Finite coefficient duality identifies its opposite with the projective radical inclusion over Cᵒᵖ, so this quotient is left almost split.

def MagnitudeConjecture.CoveringHom.radicalHomPrecomp {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {Y Z X : C} (f : Y ⟶ Z) : ↥(CategoryTheory.radicalHomSubmodule k Z X) →ₗ[k] ↥(CategoryTheory.radicalHomSubmodule k Y X)

Precomposition acts contravariantly on the radical Hom subspaces.

noncomputable def MagnitudeConjecture.CoveringHom.dualRadicalLinearYoneda {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 coefficient dual of the contravariant radical representable rad(-,X).

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

instance MagnitudeConjecture.CoveringHom.dualRadicalLinearYoneda_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 (dualRadicalLinearYoneda X)

noncomputable def MagnitudeConjecture.CoveringHom.dualRadicalLinearYonedaLinearModule {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 dual radical representable as an additive linear module.

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

Restriction of functionals along rad(-,X) ⊆ Hom(-,X).

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

Bundled linear-module form of radical restriction.

instance MagnitudeConjecture.CoveringHom.dualLinearYonedaRadicalProjection_epi {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X : C) : CategoryTheory.Epi (dualLinearYonedaRadicalProjection X)

theorem MagnitudeConjecture.CoveringHom.dualRadicalLinearYoneda_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 (dualLinearYonedaLinearModule X)) : IsFiniteDimensionalModule k (dualRadicalLinearYonedaLinearModule X)

The dual radical quotient is finite whenever the ambient dual corepresentable is finite.

noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalDualRadicalLinearYoneda {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 (dualLinearYonedaLinearModule X)) : FiniteDimensionalModuleCategory k

The finite dual radical quotient.

noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaRadicalProjection {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 (dualLinearYonedaLinearModule X)) : finiteDimensionalDualLinearYoneda X hX ⟶ finiteDimensionalDualRadicalLinearYoneda X hX

Radical restriction in the finite module category.

instance MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaRadicalProjection_epi {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 (dualLinearYonedaLinearModule X)) : CategoryTheory.Epi (finiteDimensionalDualLinearYonedaRadicalProjection X hX)

Identification after coefficient duality

theorem MagnitudeConjecture.CoveringHom.isRadicalMorphism_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} (f : X ⟶ Y) : QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f.op ↔ QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f

The categorical radical is invariant under passage to the opposite category.

def MagnitudeConjecture.CoveringHom.homOpLinearEquiv {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) : (X ⟶ Y) ≃ₗ[k] Opposite.op Y ⟶ Opposite.op X

Opposite passage as a linear equivalence on a Hom space.

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

Opposite passage as a linear equivalence on radical Hom spaces.

noncomputable def MagnitudeConjecture.CoveringHom.coefficientDualDualLinearYonedaIso {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 (dualLinearYonedaLinearModule X)) : coefficientDualModule (dualLinearYonedaLinearModule X) ≅ linearCoyonedaLinearModule (Opposite.op X)

After coefficient duality, a finite dual corepresentable becomes the corresponding representable over the opposite category.

noncomputable def MagnitudeConjecture.CoveringHom.coefficientDualDualRadicalLinearYonedaIso {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 (dualLinearYonedaLinearModule X)) : coefficientDualModule (dualRadicalLinearYonedaLinearModule X) ≅ radicalLinearCoyonedaLinearModule (Opposite.op X)

After coefficient duality, the finite dual radical quotient becomes the radical subrepresentable over the opposite category.

theorem MagnitudeConjecture.CoveringHom.oppositeLinearCoyoneda_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 (dualLinearYonedaLinearModule X)) : IsFiniteDimensionalModule k (linearCoyonedaLinearModule (Opposite.op X))

Finiteness of a dual corepresentable over C implies finiteness of the corresponding representable over Cᵒᵖ.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCoefficientDualDualLinearYonedaIso {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 (dualLinearYonedaLinearModule X)) : finiteCoefficientDualFunctor.obj (Opposite.op (finiteDimensionalDualLinearYoneda X hX)) ≅ finiteDimensionalLinearCoyoneda (Opposite.op X) ⋯

Finite-module form of the coefficient-dual identification of a dual corepresentable with the opposite representable.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCoefficientDualDualRadicalLinearYonedaIso {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 (dualLinearYonedaLinearModule X)) : finiteCoefficientDualFunctor.obj (Opposite.op (finiteDimensionalDualRadicalLinearYoneda X hX)) ≅ finiteDimensionalLinearCoyonedaRadical (Opposite.op X) ⋯

Finite-module form of the coefficient-dual identification of the dual radical quotient with the opposite radical representable.

theorem MagnitudeConjecture.CoveringHom.finiteCoefficientDualDualLinearYoneda_radical_compatibility {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 (dualLinearYonedaLinearModule X)) : CategoryTheory.CategoryStruct.comp (finiteCoefficientDualFunctor.map (finiteDimensionalDualLinearYonedaRadicalProjection X hX).op) (finiteCoefficientDualDualLinearYonedaIso X hX).hom = CategoryTheory.CategoryStruct.comp (finiteCoefficientDualDualRadicalLinearYonedaIso X hX).hom (finiteDimensionalLinearCoyonedaRadicalInclusion (Opposite.op X) ⋯)

Under the two coefficient-dual identifications, dualized radical restriction is exactly the inclusion of the radical representable.

The canonical left almost-split quotient

def MagnitudeConjecture.CoveringHom.endMulOppositeEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : (CategoryTheory.End X)ᵐᵒᵖ ≃+* CategoryTheory.End (Opposite.op X)

Endomorphisms of an opposite object are the multiplicative opposite of the original endomorphism ring.

theorem MagnitudeConjecture.CoveringHom.mulOpposite_isLocalRing {R : Type v} [Ring R] [IsLocalRing R] : IsLocalRing Rᵐᵒᵖ

The multiplicative opposite of a local ring is local.

theorem MagnitudeConjecture.CoveringHom.opposite_end_isLocalRing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (Y : Cᵒᵖ) : IsLocalRing (CategoryTheory.End Y)

Local endomorphism rings pass from a category to its opposite.

theorem MagnitudeConjecture.CoveringHom.leftAlmostSplit_of_op_isRightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] {Z E : C} {f : Z ⟶ E} (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f.op) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f

If the opposite of a morphism is right almost split, the original morphism is left almost split.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaRadicalProjection_isLeftAlmostSplit {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : C) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (finiteDimensionalDualLinearYonedaRadicalProjection X ⋯)

Radical restriction from a finite dual corepresentable is the canonical left almost-split morphism starting at that indecomposable injective.

The canonical simple socle

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaSocle {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 (dualLinearYonedaLinearModule X)) : FiniteDimensionalModuleCategory k

The simple socle coordinate of a finite dual corepresentable, realized as the kernel of its canonical left almost-split radical quotient.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaSocleInclusion {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 (dualLinearYonedaLinearModule X)) : finiteDimensionalDualLinearYonedaSocle X hX ⟶ finiteDimensionalDualLinearYoneda X hX

The canonical socle inclusion into a finite dual corepresentable.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaSocle_simple {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : C) : CategoryTheory.Simple (finiteDimensionalDualLinearYonedaSocle X ⋯)

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaSocleInclusion_ne_zero {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (X : C) : finiteDimensionalDualLinearYonedaSocleInclusion X ⋯ ≠ 0

The canonical simple socle inclusion of a finite dual corepresentable is nonzero.