Closure and polynomial consequences of an aligned biduality

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.qToSClosureRelabeling {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedBiduality τ) : σ.qClosure.RelabelingEquiv τ.sClosure

Quotient closure on the source is relabeled submodule closure on the target.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.sToQClosureRelabeling {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedBiduality τ) : σ.sClosure.RelabelingEquiv τ.qClosure

Submodule closure on the source is relabeled quotient closure on the target.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.sClosure_isClosed_iff_qClosure_image {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedBiduality τ) (T : Set ι) : σ.sClosure.IsClosed T ↔ τ.qClosure.IsClosed (⇑D.forward.labelEquiv '' T)

A support is submodule-closed exactly when its dual image is quotient-closed.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.quotientToSubmoduleClosedOrderIso {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedBiduality τ) : ClosureOperator.Closeds σ.qClosure ≃o ClosureOperator.Closeds τ.sClosure

Duality gives the paper's order isomorphism from quotient-closed supports to submodule-closed supports.

def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.quotientToSubobjectClosedAdditiveSubcategoryOrderIso {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedBiduality τ) : QuotientClosedAdditiveSubcategory ≃o SubobjectClosedAdditiveSubcategory

The paper-facing duality isomorphism from literal quotient-closed additive subcategories to literal subobject-closed additive subcategories.

@[simp]

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.ncard_support_quotientToSubobjectClosedAdditiveSubcategoryOrderIso {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedBiduality τ) (C : QuotientClosedAdditiveSubcategory) : (τ.support ↑((quotientToSubobjectClosedAdditiveSubcategoryOrderIso σ τ D) C)).ncard = (σ.support ↑C).ncard

Duality preserves the number of indecomposable isomorphism classes in every literal quotient-closed subcategory.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.quotientToSubmoduleLevelPolynomial_eq {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedBiduality τ) [Finite ι] [Finite κ] : σ.qClosure.levelPolynomial = τ.sClosure.levelPolynomial

In finite type, duality identifies the quotient and submodule level-generating polynomials.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.submoduleToQuotientLevelPolynomial_eq {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedBiduality τ) [Finite ι] [Finite κ] : σ.sClosure.levelPolynomial = τ.qClosure.levelPolynomial

The reverse exchange of level-generating polynomials.