Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleIyamaSubobjectReduction

Reduction of Iyama realization to subobject closure #

Finite biproducts of the distinguished sink represent all full-support poset spaces. Since every poset space embeds into its full-support envelope, essential surjectivity of the primitive incidence functor follows from the single hereditary-torsionfree statement that its essential image is closed under subobjects.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sinkBiproduct {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} (D : S.PrimitiveMultiplicityInput K) (n : ℕ) :
S.FactorCategory K

The finite biproduct of copies of the distinguished sink.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.precomposition_surjective_to_sinkBiproduct {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (hsink : D.multiplicity ↑D.sink = 1) (n : ℕ) (t : T) :
    Function.Surjective ⇑(R.representableData.precomposition t (sinkBiproduct D n))

    Precomposition from every non-root boundary projective onto a finite biproduct of sinks is surjective.

    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedSinkBiproductCoordinateEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (hsink : D.multiplicity ↑D.sink = 1) (Y : PosetSpace.Obj k T) :
    (R.representableData.obj (sinkBiproduct D (Module.finrank k Y.carrier))).carrier ≃ₗ[k] Y.carrier

    Coordinates on the represented sink biproduct, followed by a basis of the requested finite-dimensional ambient space.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sinkBiproductObjIsoFullSupport {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (hsink : D.multiplicity ↑D.sink = 1) (Y : PosetSpace.Obj k T) :
      R.representableData.obj (sinkBiproduct D (Module.finrank k Y.carrier)) ≅ PosetSpace.fullSupport Y

      A finite biproduct of the distinguished sink represents the full-support envelope of any finite poset space.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.fullSupport_mem_essentialImage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (hsink : D.multiplicity ↑D.sink = 1) (Y : PosetSpace.Obj k T) :
        ∃ (X : S.FactorCategory K), Nonempty (R.representableData.obj X ≅ PosetSpace.fullSupport Y)

        All full-support poset spaces lie in the essential image of the primitive representable functor.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representable_essSurj_of_closedUnderSubobjects {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (hsink : D.multiplicity ↑D.sink = 1) (hclosed : R.representableData.EssentialImageClosedUnderSubobjects) (Y : PosetSpace.Obj k T) :
        ∃ (X : S.FactorCategory K), Nonempty (R.representableData.obj X ≅ Y)

        Iyama essential surjectivity is reduced to its hereditary-torsionfree content: closure of the restricted-Yoneda image under subobjects.