Boundary markers of a primitive new mesh

For a new right mesh M → U → N in the primitive quotient, this file constructs the inverse ambient marker p_M = τ_A⁻¹M. It proves that p_M survives the quotient by mod (A/AeA) and is tau-projective there. Thus it is the projective boundary marker paired with the already constructed tau-injective marker q_N = τ_A N.

The survival proof is categorical. If p_M were an A/AeA-module, extension closure would put the ambient AR sequence ending at p_M inside the literal quotient subcategory. Its first map and Hoshino's relative first map would then be minimal left almost split with the same source. Uniqueness and short exactness identify their endpoints, contradicting survival of q_N.

theorem QuotientSubmoduleEquidistribution.IsLeftAlmostSplit.fullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (f : X ⟶ Y) (hf : IsLeftAlmostSplit f.hom) : IsLeftAlmostSplit f

An ambient left almost-split morphism remains left almost split after restricting both endpoints to a full subcategory.

theorem QuotientSubmoduleEquidistribution.IsLeftMinimal.fullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (f : X ⟶ Y) (hf : IsLeftMinimal f.hom) : IsLeftMinimal f

Ambient left minimality remains left minimal after restricting both endpoints to a full subcategory.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.kernel_ι_isLeftMinimal_of_splitEpi_end_isIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {E Z : D} (f : E ⟶ Z) [CategoryTheory.Epi f] (hf : IsRightAlmostSplit f) (hk : IsLeftAlmostSplit (CategoryTheory.Limits.kernel.ι f)) (hiso : ∀ (d : Z ⟶ Z), CategoryTheory.IsSplitEpi d → CategoryTheory.IsIso d) : IsLeftMinimal (CategoryTheory.Limits.kernel.ι f)

A left almost-split kernel inclusion is left minimal when every split epimorphic endomorphism of the right endpoint is invertible.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.leftMarkerAmbientLabel_not_mem {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) : leftMarkerAmbientLabel H he N ∉ S.primitiveKilledLabels D

The inverse marker p_M = τ_A⁻¹M of the source of a new quotient mesh survives the factor by mod (A/AeA).

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.leftMarker {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) : S.SurvivingLabel (S.primitiveKilledLabels D)

The surviving left marker bundled as an object label of the primitive factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.leftMarker_ambient_not_projective {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) : ¬CategoryTheory.Projective (S.fgObj ↑(leftMarker H he N))

The inverse ambient translate defining p_M is not projective in mod A. Its projectivity is created only after passing to the factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.leftMarker_isProjective {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) : (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).IsProjective (leftMarker H he N)

The inverse marker p_M is tau-projective in the primitive factor: its ambient translate is the killed quotient source M.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.leftMarkerProjectiveLabel {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) : S.FactorProjectiveLabel (S.primitiveKilledLabels D)

The factor-projective boundary label supplied by a new mesh endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.leftMarker_primitiveMultiplicity_eq_one {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] (B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D)) (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : S.primitiveMultiplicity D ↑(leftMarker H he N) = 1

The boundary coordinate theorem gives the marker multiplicity [p_M : S_e] = 1.