Minimal projective presentations under finite orbit push-down

Finite skeletal orbit push-down preserves radical maps from indecomposable modules with trivial deck stabilizer. Applying this entrywise to a minimal finite-representable presentation proves that its pushed augmentation remains right minimal. The only presentation-specific input is trivial stabilizer for the representing summands.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteProjectiveRepresentableSum_projective {k : Type uK} [Field k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {G : Type uG} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (Q : CategoryTheory.Mat_ Cᵒᵖ) : CategoryTheory.Projective ((D.orbitSkeletonFiniteProjectiveRepresentableSumFunctor hP).obj Q)

The finite sums of representables on the orbit skeleton are projective.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteProjectiveRepresentableSumOrbitSkeletonPushdown_projective {k : Type uK} [Field k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {G : Type uG} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (Q : CategoryTheory.Mat_ Cᵒᵖ) : CategoryTheory.Projective (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj ((finiteProjectiveRepresentableSumFunctor hP).obj Q))

Orbit push-down of a finite sum of projective representables is projective, via the literal downstairs representable comparison.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_isRadicalMorphism {k : Type uK} [Field k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {G : Type uG} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (M N : FiniteDimensionalModuleCategory k) (f : M ⟶ N) (hM : CategoryTheory.Indecomposable M) : (∀ (a : Additive G), Nonempty (M ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj M) → a = 0) → QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f → QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (D.finiteDimensionalModuleOrbitSkeletonPushdown.map f)

Finite skeletal orbit push-down preserves radical morphisms whose source is indecomposable and has trivial deck stabilizer.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_finBiproduct_isRadicalMorphism {k : Type uK} [Field k] {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {G : Type uG} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] {I J : Type} [Fintype I] [Fintype J] (M : I → FiniteDimensionalModuleCategory k) (N : J → FiniteDimensionalModuleCategory k) (f : ⨁ M ⟶ ⨁ N) (hM : ∀ (i : I), CategoryTheory.Indecomposable (M i)) : (∀ (i : I) (a : Additive G), Nonempty (M i ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj (M i)) → a = 0) → QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism f → QuotientSubmoduleEquidistribution.CategoricalRadical.IsRadicalMorphism (D.finiteDimensionalModuleOrbitSkeletonPushdown.map f)

Finite skeletal orbit push-down preserves a radical map between finite biproducts when each source summand is indecomposable with trivial deck stabilizer.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_minimalFiniteRepresentablePresentation_rightMinimal {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) {M : FiniteDimensionalModuleCategory k} (Q : MinimalFiniteRepresentablePresentation hP M) : QuotientSubmoduleEquidistribution.IsRightMinimal (D.finiteDimensionalModuleOrbitSkeletonPushdown.map Q.f)

Orbit push-down preserves any minimal finite-representable projective cover under freeness on isomorphism classes. A fresh two-step presentation supplies the radical differential; uniqueness of projective covers transports the result to the specified cover.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_minimalProjectivePresentation {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) {M : FiniteDimensionalModuleCategory k} (Q : MinimalFiniteRepresentablePresentation hP M) : MinimalProjectivePresentation (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M)

The pushed form of a minimal finite-representable projective cover.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_twoStepMinimalProjectivePresentation {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) {M : FiniteDimensionalModuleCategory k} (Q : TwoStepMinimalFiniteRepresentablePresentation hP M) : TwoStepMinimalProjectivePresentation (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M)

Orbit push-down of a literal two-step minimal presentation, with the preserved-kernel isomorphism built into its first cover target.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_twoStepMinimalProjectivePresentation_differential {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) {M : FiniteDimensionalModuleCategory k} (Q : TwoStepMinimalFiniteRepresentablePresentation hP M) : (D.finiteDimensionalModuleOrbitSkeletonPushdown_twoStepMinimalProjectivePresentation hP hlocal hfree Q).differential = D.finiteDimensionalModuleOrbitSkeletonPushdown.map Q.toTwoStepFiniteRepresentablePresentation.differential

The first differential in the pushed two-step minimal presentation is literally the image of the upstairs differential.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonTwoStepMinimalProjectivePresentation {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) {M : FiniteDimensionalModuleCategory k} (Q : TwoStepMinimalFiniteRepresentablePresentation hP M) : TwoStepMinimalProjectivePresentation (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M)

Recoordinate the pushed two-step presentation by the canonical isomorphisms with literal finite sums of representables on the orbit skeleton.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonTwoStepMinimalProjectivePresentation_differential {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] [IsCancelSMul G C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) {M : FiniteDimensionalModuleCategory k} (Q : TwoStepMinimalFiniteRepresentablePresentation hP M) : (D.orbitSkeletonTwoStepMinimalProjectivePresentation hP hlocal hfree Q).differential = (D.orbitSkeletonFiniteProjectiveRepresentableSumFunctor hP).map Q.toTwoStepFiniteRepresentablePresentation.matrixDifferential

The literal orbit-skeleton presentation has the pushed representing matrix as its first differential.