Auslander--Reiten kernels under finite orbit push-down #
For a minimal finite-representable presentation of a nonprojective
indecomposable module, the finite Nakayama kernel is the kernel of any chosen minimal right
almost-split map. Exact orbit push-down transports that kernel, while the
finite-matrix Nakayama comparison identifies its image with the kernel of the
literal pushed Nakayama matrix. This gives the presentation-dependent
DTr/almost-split identification used in the magnitude argument.
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonNakayamaKernelIso_downstreamKernel
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{G : Type v}
[Group G]
[MulAction G C]
[IsCancelSMul 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)]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
{M : FiniteDimensionalModuleCategory k}
(Q : TwoStepMinimalFiniteRepresentablePresentation hP M)
[hExt : CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
(hM : ¬CategoryTheory.Projective (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M))
(hMind : CategoryTheory.Indecomposable (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M))
{N : FiniteDimensionalModuleCategory k}
(m : N ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M)
(hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m)
(hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m)
:
CategoryTheory.Limits.kernel
((D.orbitSkeletonFiniteNakayamaRepresentableSumFunctor hI).map Q.representingDifferential) ≅ CategoryTheory.Limits.kernel m
The kernel of the literal pushed Nakayama matrix is the kernel of any chosen minimal right almost-split map to the pushed module. This is the downstairs half of the comparison used to prove that an upstairs almost-split sequence remains almost split after orbit push-down.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonNakayamaKernelIso_pushedKernel
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{G : Type v}
[Group G]
[MulAction G C]
[IsCancelSMul 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)]
[CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X))
{M : FiniteDimensionalModuleCategory k}
(Q : TwoStepMinimalFiniteRepresentablePresentation hP M)
(hM : ¬CategoryTheory.Projective M)
(hMind : CategoryTheory.Indecomposable M)
{N : FiniteDimensionalModuleCategory k}
(m : N ⟶ M)
(hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m)
(hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m)
:
CategoryTheory.Limits.kernel
((D.orbitSkeletonFiniteNakayamaRepresentableSumFunctor hI).map Q.representingDifferential) ≅ CategoryTheory.Limits.kernel (D.finiteDimensionalModuleOrbitSkeletonPushdown.map m)
The kernel of the literal pushed Nakayama matrix is the kernel of the pushed chosen minimal right almost-split map.
Instances For
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_isRightAlmostSplit_of_indec_trivialStabilizers
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{G : Type v}
[Group G]
[MulAction G C]
[IsCancelSMul 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)]
[CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
{M : FiniteDimensionalModuleCategory k}
(Q : TwoStepMinimalFiniteRepresentablePresentation hP M)
(hM : ¬CategoryTheory.Projective M)
(hMind : CategoryTheory.Indecomposable M)
{N : FiniteDimensionalModuleCategory k}
(m : N ⟶ M)
(hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m)
(hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m)
:
(∀ (X : FiniteDimensionalModuleCategory k),
CategoryTheory.Indecomposable X →
∀ (a : Additive G),
Nonempty (X ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj X) → a = 0) →
∀ [hExtDown : CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)],
QuotientSubmoduleEquidistribution.IsRightAlmostSplit (D.finiteDimensionalModuleOrbitSkeletonPushdown.map m)
Gabriel 3.6(a), in the finite skeletal orbit model, under its exact module-theoretic stabilizer hypothesis: a minimal right-almost-split map remains right almost split after push-down.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_isRightMinimal_of_indec_trivialStabilizers
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{G : Type v}
[Group G]
[MulAction G C]
[IsCancelSMul 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)]
[CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X))
{M : FiniteDimensionalModuleCategory k}
(Q : TwoStepMinimalFiniteRepresentablePresentation hP M)
(hM : ¬CategoryTheory.Projective M)
(hMind : CategoryTheory.Indecomposable M)
{N : FiniteDimensionalModuleCategory k}
(m : N ⟶ M)
(hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m)
(hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m)
:
(∀ (X : FiniteDimensionalModuleCategory k),
CategoryTheory.Indecomposable X →
∀ (a : Additive G),
Nonempty (X ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj X) → a = 0) →
QuotientSubmoduleEquidistribution.IsRightMinimal (D.finiteDimensionalModuleOrbitSkeletonPushdown.map m)
The same exact stabilizer hypothesis makes the pushed right-almost-split map right minimal. The pushed kernel remains indecomposable, so the nonsplit pushed kernel inclusion is radical; short exactness then forces minimality of the terminal map.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_isRightAlmostSplit
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{G : Type v}
[Group G]
[MulAction G C]
[IsCancelSMul 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)]
[CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
[IsMulTorsionFree G]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
{M : FiniteDimensionalModuleCategory k}
(Q : TwoStepMinimalFiniteRepresentablePresentation hP M)
(hM : ¬CategoryTheory.Projective M)
(hMind : CategoryTheory.Indecomposable M)
{N : FiniteDimensionalModuleCategory k}
(m : N ⟶ M)
(hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m)
(hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m)
[hExtDown : CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
:
Gabriel 3.6(a), specialized to a torsion-free deck group acting freely on objects. Finite support supplies the indecomposable-module stabilizer hypothesis of the exact theorem above.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_isLeftAlmostSplit
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{G : Type v}
[Group G]
[MulAction G C]
[IsCancelSMul 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)]
[CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
[IsMulTorsionFree G]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
{L E : FiniteDimensionalModuleCategory k}
(f : L ⟶ E)
[CategoryTheory.Mono f]
(hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f)
(hmin : QuotientSubmoduleEquidistribution.IsLeftMinimal f)
(hL : CategoryTheory.Indecomposable L)
[hExtDown : CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
:
Density-free left-handed form of Gabriel 3.6(a): the push-down of a left almost-split monomorphism with indecomposable source is left almost split. The proof rotates the morphism to its right-almost-split cokernel, uses the right-handed push-down theorem, and rotates the mapped short exact sequence back.
theorem
MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonNakayamaKernel_identifies_pushedRightAlmostSplit
{k : Type v}
[Field k]
[IsAlgClosed k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{G : Type v}
[Group G]
[MulAction G C]
[IsCancelSMul 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)]
[CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
[IsMulTorsionFree G]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(hfree : IsFreeOnIsomorphismClasses)
(W : Set (FiniteDimensionalModuleCategory k))
{X Y : CoveringSeparation.WindowCategory W}
(m : X ⟶ Y)
(Q : TwoStepMinimalFiniteRepresentablePresentation hP Y.obj)
(hM : ¬CategoryTheory.Projective Y.obj)
(hMind : CategoryTheory.Indecomposable Y.obj)
(hmAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit m.hom)
(hmMin : QuotientSubmoduleEquidistribution.IsRightMinimal m.hom)
[hExtDown : CategoryTheory.HasExt (FiniteDimensionalModuleCategory k)]
:
QuotientSubmoduleEquidistribution.IsRightAlmostSplit ((D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W).map m) ∧ Nonempty
(CategoryTheory.Limits.kernel
((D.orbitSkeletonFiniteNakayamaRepresentableSumFunctor hI).map Q.representingDifferential) ≅ CategoryTheory.Limits.kernel ((D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W).map m))
On any full module window, the pushed minimal right almost-split map is right almost split downstairs, and its kernel is the kernel of the literal pushed Nakayama matrix. This is the window-shaped form of the density-free finite-skeletal Gabriel 3.6(a) theorem.