Quotient/submodule exchange under an anti-equivalence

This is the abstract categorical interface expected from finite-dimensional k-linear duality. It deliberately does not construct that concrete duality.

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedAntiEquivalence {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) : Type (max (max (max (max (max uR uS) vR) vS) (wR + 1)) (wS + 1))

An anti-equivalence of module categories aligned with two chosen indecomposable skeletons.

• categoryEquiv : (FGModuleCat R)ᵒᵖ ≌ FGModuleCat S
• labelEquiv : ι ≃ κ
• objIso (i : ι) : self.categoryEquiv.functor.obj (Opposite.op (σ.obj i)) ≅ τ.obj (self.labelEquiv i)

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedAntiEquivalence.injective_iff_projective_image {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedAntiEquivalence τ) (i : ι) : CategoryTheory.Injective (σ.obj i) ↔ CategoryTheory.Projective (τ.obj (D.labelEquiv i))

An aligned anti-equivalence identifies injective source labels with projective target labels.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedAntiEquivalence.sumIso {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedAntiEquivalence τ) (J : FintypeCat) (a : J.obj → ι) : D.categoryEquiv.functor.obj (Opposite.op (σ.sumOver J a)) ≅ τ.sumOver J fun (j : J.obj) => D.labelEquiv (a j)

An anti-equivalence sends a displayed finite direct sum to the displayed sum of the dual representatives.

The route is: biproduct as coproduct, opposite coproduct as product, preservation of products by the equivalence, then product as biproduct.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedAntiEquivalence.facToSubObj {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedAntiEquivalence τ) {T : Set ι} {i : ι} (P : σ.FacPresentation T (σ.obj i)) : τ.SubPresentation (⇑D.labelEquiv '' T) (τ.obj (D.labelEquiv i))

A quotient presentation dualizes to a submodule presentation.

noncomputable def QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedAntiEquivalence.subToFacObj {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedAntiEquivalence τ) {T : Set ι} {i : ι} (P : σ.SubPresentation T (σ.obj i)) : τ.FacPresentation (⇑D.labelEquiv '' T) (τ.obj (D.labelEquiv i))

A submodule presentation dualizes to a quotient presentation.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedAntiEquivalence.mem_sSet_image_of_mem_qSet {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedAntiEquivalence τ) {T : Set ι} {i : ι} (hi : i ∈ σ.qSet T) : D.labelEquiv i ∈ τ.sSet (⇑D.labelEquiv '' T)

The forward half of qClosure ↔ sClosure under duality.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedAntiEquivalence.mem_qSet_image_of_mem_sSet {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) (D : σ.AlignedAntiEquivalence τ) {T : Set ι} {i : ι} (hi : i ∈ σ.sSet T) : D.labelEquiv i ∈ τ.qSet (⇑D.labelEquiv '' T)

The forward half of sClosure ↔ qClosure under duality.

structure QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality {R : Type uR} [Ring R] [IsNoetherianRing R] {S : Type uS} [Ring S] [IsNoetherianRing S] {ι : Type vR} {κ : Type vS} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton S κ) : Type (max (max (max (max (max uR uS) vR) vS) (wR + 1)) (wS + 1))

Forward and backward aligned anti-equivalences with inverse actions on the chosen skeleton labels. Finite-dimensional vector-space duality is expected to instantiate this using biduality.

• forward : σ.AlignedAntiEquivalence τ
• backward : τ.AlignedAntiEquivalence σ
• backward_label : self.backward.labelEquiv = self.forward.labelEquiv.symm

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.mem_sSet_image_iff_mem_qSet {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 ι} {i : ι} : D.forward.labelEquiv i ∈ τ.sSet (⇑D.forward.labelEquiv '' T) ↔ i ∈ σ.qSet T

Under a biduality, quotient generation on the source is equivalent to submodule generation on the target.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.mem_qSet_image_iff_mem_sSet {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 ι} {i : ι} : D.forward.labelEquiv i ∈ τ.qSet (⇑D.forward.labelEquiv '' T) ↔ i ∈ σ.sSet T

Under a biduality, submodule generation on the source is equivalent to quotient generation on the target.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.image_qClosure_eq_sClosure {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 ι) : ⇑D.forward.labelEquiv '' σ.qClosure T = τ.sClosure (⇑D.forward.labelEquiv '' T)

Duality conjugates quotient closure to submodule closure.

theorem QuotientSubmoduleEquidistribution.IndecomposableSkeleton.AlignedBiduality.image_sClosure_eq_qClosure {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 ι) : ⇑D.forward.labelEquiv '' σ.sClosure T = τ.qClosure (⇑D.forward.labelEquiv '' T)

Duality conjugates submodule closure to quotient closure.