The label-aligned contragredient finite skeleton

Finite-dimensional contragredient duality sends the chosen right-module skeleton of A to a complete duplicate-free right-module skeleton of Aᵐᵒᵖ. We retain the same finite label type, so later dualization of a new mesh reverses its endpoints without introducing a second arbitrary relabeling.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isAnnihilatedBy_primitiveIdeal_contragredient_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (M : FinitelyGeneratedCategory A) : IsAnnihilatedBy (primitiveIdeal (MulOpposite.op e)) ((QuotientSubmoduleEquidistribution.Contragredient.dualFunctor k Aᵐᵒᵖ).obj (Opposite.op M)) ↔ IsAnnihilatedBy (primitiveIdeal e) M

A module is killed by AeA exactly when its contragredient dual is killed by the opposite primitive ideal.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : FinitelyGeneratedCategory Aᵐᵒᵖ

The contragredient dual of one selected right A-module, regarded as a right Aᵐᵒᵖ-module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientFGObj_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : CategoryTheory.Indecomposable (S.contragredientFGObj i).obj

Contragredient duality preserves the indecomposability of every selected skeleton object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientFGObj_skeletal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) {i j : Fin S.n} (h : Nonempty (S.contragredientFGObj i ≅ S.contragredientFGObj j)) : i = j

The label-aligned dual family has no repeated isomorphism classes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientFGObj_complete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : Category Aᵐᵒᵖ) (hM : IsFiniteIndecomposable k Aᵐᵒᵖ M) : ∃ (i : Fin S.n), Nonempty (M ≅ (S.contragredientFGObj i).obj)

Every finite-dimensional indecomposable right Aᵐᵒᵖ-module is the dual of a uniquely labelled object of the original skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FiniteIndecomposableSkeleton k Aᵐᵒᵖ

The complete opposite-algebra skeleton obtained by dualizing S, with the same literal finite label type.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientSkeleton_n {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.contragredientSkeleton.n = S.n

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientSkeleton_fgObjIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : S.contragredientSkeleton.fgObj i ≅ S.contragredientFGObj i

The finitely generated object produced by the new skeleton is the concrete contragredient object at the same label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_contragredient_primitiveKilledLabels_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) (i : Fin S.n) : i ∈ S.contragredientSkeleton.primitiveKilledLabels ⋯ ↔ i ∈ S.primitiveKilledLabels D

A label is removed by primitive deletion in the opposite skeleton exactly when the same label is removed in the original skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredient_primitiveKilledLabels {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) : S.contragredientSkeleton.primitiveKilledLabels ⋯ = S.primitiveKilledLabels D

Primitive deletion selects literally the same finite label set after passing to the label-aligned contragredient skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientAlmostSplitSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] : QuotientSubmoduleEquidistribution.IndecomposableSkeleton Aᵐᵒᵖᵐᵒᵖ (Fin S.n)

The opposite finite skeleton in the exact interface used for finite-type almost-split sequences.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientAlignedBiduality {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] : S.almostSplitSkeleton.AlignedBiduality S.contragredientAlmostSplitSkeleton

Contragredient duality aligned with the original and opposite finite skeletons. Both directions use the identity equivalence on labels.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientAlignedBiduality_forward_label {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (i : Fin S.n) : S.contragredientAlignedBiduality.forward.labelEquiv i = i

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientAlignedBiduality_backward_label {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (i : Fin S.n) : S.contragredientAlignedBiduality.backward.labelEquiv i = i