Cyclic images of restricted representables

This file extracts the finite-length radical induction used for stable representables into a form valid for an arbitrary finite functor. The target-specific input is only a natural map from one indecomposable representable; its image has that representable as a minimal projective cover, and the image of the representable radical is its categorical radical.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : CoveringHom.FiniteDimensionalModuleCategory k

The image generated by a map from one restricted indecomposable representable into an arbitrary finite functor.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImageInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : S.finiteRepresentableImage i p ⟶ G

The inclusion of a cyclic representable image into its ambient finite functor.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImageInclusion_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : CategoryTheory.Mono (S.finiteRepresentableImageInclusion i p)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImagePresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ S.finiteRepresentableImage i p

The canonical epimorphism from the representing projective onto its cyclic image.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImagePresentation_comp_inclusion {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : CategoryTheory.CategoryStruct.comp (S.finiteRepresentableImagePresentation i p) (S.finiteRepresentableImageInclusion i p) = p

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImagePresentation_comp_inclusion_assoc {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) {Z : CoveringHom.FiniteDimensionalModuleCategory k} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.finiteRepresentableImagePresentation i p) (CategoryTheory.CategoryStruct.comp (S.finiteRepresentableImageInclusion i p) h) = CategoryTheory.CategoryStruct.comp p h

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImagePresentation_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : CategoryTheory.Epi (S.finiteRepresentableImagePresentation i p)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImagePresentation_ne_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hp : p ≠ 0) : S.finiteRepresentableImagePresentation i p ≠ 0

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImageMinimalProjectivePresentation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hp : p ≠ 0) : MinimalProjectivePresentation (S.finiteRepresentableImage i p)

A nonzero cyclic image has its chosen indecomposable representable as a minimal projective cover.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImageRadical_isRadicalSubobject {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) : IsUniserialObject.IsRadicalSubobject (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteRepresentableImagePresentation i p)))

The pushed-forward representable radical is a radical subobject of a cyclic image.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImageRadical_ne_top {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hp : p ≠ 0) : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteRepresentableImagePresentation i p)) ≠ ⊤

For a nonzero generator, its pushed-forward representable radical is a proper subobject of the cyclic image.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImage_isUniserial_of_radical {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hrad : IsUniserialObject (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteRepresentableImagePresentation i p))))) : IsUniserialObject (S.finiteRepresentableImage i p)

If the pushed-forward radical of a cyclic image is uniserial, so is the whole image.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRepresentableImage_isUniserial_of_closedRadicalSuccessors {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {G : CoveringHom.FiniteDimensionalModuleCategory k} (Good : (i : S.IndecCategory) → (S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) → Prop) (hsuccessor : ∀ (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G), Good i p → p ≠ 0 → ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteRepresentableImagePresentation i p)))) → ∃ (j : S.IndecCategory) (q : S.finiteRestrictedContravariantRepresentable (S.fgObj j) ⟶ G), Good j q ∧ q ≠ 0 ∧ Nonempty (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (S.finiteRestrictedContravariantRepresentableRadicalInclusion i) (S.finiteRepresentableImagePresentation i p))) ≅ S.finiteRepresentableImage j q)) (i : S.IndecCategory) (p : S.finiteRestrictedContravariantRepresentable (S.fgObj i) ⟶ G) (hgood : Good i p) (hp : p ≠ 0) : IsUniserialObject (S.finiteRepresentableImage i p)

Finite-length radical induction for any class of cyclic images.