Relative almost-split meshes under primitive deletion

This file realizes every Hoshino mesh in the literal primitive-quotient subcategory, proves both maps are minimal almost split, and derives endpoint and source uniqueness. These are the mesh-theoretic inputs for the global gaining-pair construction.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.quotientShortComplex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : CategoryTheory.ShortComplex (PrimitiveQuotientSubcategory e)

The Hoshino relative mesh bundled in the literal primitive-quotient subcategory. Its underlying ambient short complex is fgShortComplex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.quotientShortComplex_forget {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : N.quotientShortComplex.map (PrimitiveQuotientProperty e).ι = N.fgShortComplex

The bundled quotient mesh forgets to the previously constructed ambient Hoshino complex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.quotientShortComplex_shortExact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (N : S.PrimitiveNewRightMeshEndpoint D) : N.quotientShortComplex.ShortExact

The bundled Hoshino mesh is short exact in the literal quotient subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.quotientShortComplex_g_minimalRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit N.quotientShortComplex.g ∧ QuotientSubmoduleEquidistribution.IsRightMinimal N.quotientShortComplex.g

The terminal map of the bundled quotient mesh is the Hoshino minimal right almost-split morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.quotientShortComplex_f_minimalLeftAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit N.quotientShortComplex.f ∧ QuotientSubmoduleEquidistribution.IsLeftMinimal N.quotientShortComplex.f

The initial map of the bundled quotient mesh is minimal left almost split. This is the sourcewise uniqueness input for the negative half of the new-mesh injection.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceLabel_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) : Function.Injective (sourceLabel H he)

Distinct primitive new meshes have distinct quotient sources. This is the sourcewise counterpart of endpoint extensionality and follows from uniqueness of minimal left almost-split maps in mod(A/AeA).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ext {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} {N N' : S.PrimitiveNewRightMeshEndpoint D} (h : N.label = N'.label) : N = N'

A primitive new-mesh endpoint is determined by its quotient label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.ext_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} {N N' : S.PrimitiveNewRightMeshEndpoint D} : N = N' ↔ N.label = N'.label

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.finite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} : Finite (S.PrimitiveNewRightMeshEndpoint D)

There are only finitely many primitive new-mesh endpoints.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.PositiveEndpoint {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} : Type

A positive primitive new mesh, retaining the proof of its sign.