def QuotientSubmoduleEquidistribution.Contragredient.ofCarrierIso (R : Type u) [Ring R] (M : FGModuleCat R) : M ≅ FGModuleCat.of R ↑M

Every bundled finitely generated module is canonically isomorphic to the FGModuleCat.of object built from its carrier. The two objects have the same elements and action, but are not definitionally equal because an arbitrary object retains its original ModuleCat wrapper.

@[reducible]

def QuotientSubmoduleEquidistribution.Contragredient.dualOpModule (K R : Type u) [Field K] [Ring R] [Algebra K R] (X : Type u) [AddCommGroup X] [Module K X] [Module Rᵐᵒᵖ X] [IsScalarTower K Rᵐᵒᵖ X] : Module R (Module.Dual K X)

The dual of an Rᵐᵒᵖ-module, regarded directly as an R-module.

theorem QuotientSubmoduleEquidistribution.Contragredient.dualOpIsScalarTower (K R : Type u) [Field K] [Ring R] [Algebra K R] (X : Type u) [AddCommGroup X] [Module K X] [Module Rᵐᵒᵖ X] [IsScalarTower K Rᵐᵒᵖ X] : IsScalarTower K R (Module.Dual K X)

def QuotientSubmoduleEquidistribution.Contragredient.dualOpFGObj (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (M : FGModuleCat Rᵐᵒᵖ) : FGModuleCat R

The reverse contragredient object, with the canonical identification R ≃ Rᵐᵒᵖᵐᵒᵖ built into its action.

def QuotientSubmoduleEquidistribution.Contragredient.dualOpMap {K R : Type u} [Field K] [Ring R] [Algebra K R] {X Y : Type u} [AddCommGroup X] [Module K X] [Module Rᵐᵒᵖ X] [IsScalarTower K Rᵐᵒᵖ X] [AddCommGroup Y] [Module K Y] [Module Rᵐᵒᵖ Y] [IsScalarTower K Rᵐᵒᵖ Y] (g : X →ₗ[Rᵐᵒᵖ] Y) : Module.Dual K Y →ₗ[R] Module.Dual K X

The dual map, with source and target regarded as R-modules.

def QuotientSubmoduleEquidistribution.Contragredient.reverseDualFunctor (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : CategoryTheory.Functor (FGModuleCat Rᵐᵒᵖ)ᵒᵖ (FGModuleCat R)

The reverse contragredient functor.

@[instance_reducible]

def QuotientSubmoduleEquidistribution.Contragredient.moduleKOfFGModule (K R : Type u) [Field K] [Ring R] [Algebra K R] (M : FGModuleCat R) : Module K ↑M

@[instance_reducible]

def QuotientSubmoduleEquidistribution.Contragredient.moduleKOfFGModuleOp (K R : Type u) [Field K] [Ring R] [Algebra K R] (M : FGModuleCat Rᵐᵒᵖ) : Module K ↑M

theorem QuotientSubmoduleEquidistribution.Contragredient.towerKROfFGModule (K R : Type u) [Field K] [Ring R] [Algebra K R] (M : FGModuleCat R) : IsScalarTower K R ↑M

theorem QuotientSubmoduleEquidistribution.Contragredient.towerKROfFGModuleOp (K R : Type u) [Field K] [Ring R] [Algebra K R] (M : FGModuleCat Rᵐᵒᵖ) : IsScalarTower K Rᵐᵒᵖ ↑M

def QuotientSubmoduleEquidistribution.Contragredient.forwardInnerDualEquiv (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (M : FGModuleCat R) : ↑((dualFunctor K R).obj (Opposite.op M)) ≃ₗ[K] Module.Dual K ↑M

The K-module on the forward contragredient object, obtained by restricting its Rᵐᵒᵖ-action, is canonically the ordinary K-linear dual. The underlying function is the identity; the proof records the non-definitional scalar-action comparison.

def QuotientSubmoduleEquidistribution.Contragredient.forwardCanonicalToCompositeEquiv (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (M : FGModuleCat R) : Module.Dual K (Module.Dual K ↑M) ≃ ↑((reverseDualFunctor K R).obj (Opposite.op ((dualFunctor K R).obj (Opposite.op M))))

As plain types, the concrete forward-then-reverse object is the usual double dual after correcting the inner restricted-scalar structure.

def QuotientSubmoduleEquidistribution.Contragredient.forwardBidualMap (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (M : FGModuleCat R) : ↑M →ₗ[R] ↑((reverseDualFunctor K R).obj (Opposite.op ((dualFunctor K R).obj (Opposite.op M))))

Evaluation into the actual forward-then-reverse object, linear over R.

theorem QuotientSubmoduleEquidistribution.Contragredient.forwardBidualMap_bijective (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (M : FGModuleCat R) : Function.Bijective ⇑(forwardBidualMap K R M)

The concrete evaluation map is bijective. The proof factors its underlying function through ordinary finite-dimensional biduality and the restricted-scalar correction above.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.forwardBidualLinearEquiv (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (M : FGModuleCat R) : ↑M ≃ₗ[R] ↑((reverseDualFunctor K R).obj (Opposite.op ((dualFunctor K R).obj (Opposite.op M))))

Evaluation as an R-linear equivalence with the actual composite object.

def QuotientSubmoduleEquidistribution.Contragredient.fgModuleIsoOfLinearEquiv (R : Type u) [Ring R] {M N : FGModuleCat R} (e : ↑M ≃ₗ[R] ↑N) : M ≅ N

Turn a linear equivalence between the carriers of two arbitrary FGModuleCat objects into a categorical isomorphism, without replacing either object by an FGModuleCat.of wrapper.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.forwardBidualIso (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (M : FGModuleCat R) : M ≅ (reverseDualFunctor K R).obj (Opposite.op ((dualFunctor K R).obj (Opposite.op M)))

Objectwise biduality for the forward-then-reverse composite.

def QuotientSubmoduleEquidistribution.Contragredient.forwardDoubleDualFunctor (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : CategoryTheory.Functor (FGModuleCat R) (FGModuleCat R)

The covariant forward-then-reverse double-dual functor.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.forwardBidualNatIso (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : CategoryTheory.Functor.id (FGModuleCat R) ≅ forwardDoubleDualFunctor K R

Finite-dimensional bidual evaluation is natural for the concrete forward-then-reverse functor.

def QuotientSubmoduleEquidistribution.Contragredient.reverseInnerDualEquiv (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (N : FGModuleCat Rᵐᵒᵖ) : ↑((reverseDualFunctor K R).obj (Opposite.op N)) ≃ₗ[K] Module.Dual K ↑N

The reverse contragredient object has the ordinary K-linear dual as its underlying K-module after comparing its K-action restricted from R with the canonical action.

def QuotientSubmoduleEquidistribution.Contragredient.reverseCanonicalToCompositeEquiv (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (N : FGModuleCat Rᵐᵒᵖ) : Module.Dual K (Module.Dual K ↑N) ≃ ↑((dualFunctor K R).obj (Opposite.op ((reverseDualFunctor K R).obj (Opposite.op N))))

As plain types, the reverse-then-forward object is the usual double dual after correcting the inner restricted-scalar structure.

def QuotientSubmoduleEquidistribution.Contragredient.reverseBidualMap (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (N : FGModuleCat Rᵐᵒᵖ) : ↑N →ₗ[Rᵐᵒᵖ] ↑((dualFunctor K R).obj (Opposite.op ((reverseDualFunctor K R).obj (Opposite.op N))))

Evaluation into the actual reverse-then-forward object, linear over Rᵐᵒᵖ.

theorem QuotientSubmoduleEquidistribution.Contragredient.reverseBidualMap_bijective (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (N : FGModuleCat Rᵐᵒᵖ) : Function.Bijective ⇑(reverseBidualMap K R N)

The reverse concrete evaluation map is bijective.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.reverseBidualLinearEquiv (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (N : FGModuleCat Rᵐᵒᵖ) : ↑N ≃ₗ[Rᵐᵒᵖ] ↑((dualFunctor K R).obj (Opposite.op ((reverseDualFunctor K R).obj (Opposite.op N))))

Reverse evaluation as an Rᵐᵒᵖ-linear equivalence.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.reverseBidualIso (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] (N : FGModuleCat Rᵐᵒᵖ) : N ≅ (dualFunctor K R).obj (Opposite.op ((reverseDualFunctor K R).obj (Opposite.op N)))

Objectwise biduality for the reverse-then-forward composite.

def QuotientSubmoduleEquidistribution.Contragredient.reverseDoubleDualFunctor (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : CategoryTheory.Functor (FGModuleCat Rᵐᵒᵖ) (FGModuleCat Rᵐᵒᵖ)

The covariant reverse-then-forward double-dual functor.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.reverseBidualNatIso (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : CategoryTheory.Functor.id (FGModuleCat Rᵐᵒᵖ) ≅ reverseDoubleDualFunctor K R

Reverse bidual evaluation is natural.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.oppositeForwardBidualNatIso (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : CategoryTheory.Functor.id (FGModuleCat R)ᵒᵖ ≅ (dualFunctor K R).comp (reverseDualFunctor K R).rightOp

The forward bidual natural isomorphism, viewed on the opposite category in the orientation required for a categorical equivalence.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.dualityEquivalence (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : (FGModuleCat R)ᵒᵖ ≌ FGModuleCat Rᵐᵒᵖ

Same-universe contragredient duality between the opposite category of finitely generated R-modules and finitely generated Rᵐᵒᵖ-modules. Equivalence.mk adjointifies the supplied unit, so no additional choice-dependent triangle calculation is needed.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.reverseDualityEquivalence (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] : (FGModuleCat Rᵐᵒᵖ)ᵒᵖ ≌ FGModuleCat R

The reverse same-universe equivalence, with the concrete reverse dual as its forward functor.

theorem QuotientSubmoduleEquidistribution.Contragredient.indecomposable_map_anti (R : Type u) [Ring R] {S : Type u} [Ring S] (E : (FGModuleCat R)ᵒᵖ ≌ FGModuleCat S) {M : FGModuleCat R} (hM : Foundation.IsIndecomposableModule R ↑M) : Foundation.IsIndecomposableModule S ↑(E.functor.obj (Opposite.op M))

An anti-equivalence of finitely generated module categories preserves the project foundation's module-level indecomposability predicate.

theorem QuotientSubmoduleEquidistribution.Contragredient.dualFunctor_indec (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] {M : FGModuleCat R} (hM : Foundation.IsIndecomposableModule R ↑M) : Foundation.IsIndecomposableModule Rᵐᵒᵖ ↑((dualFunctor K R).obj (Opposite.op M))

Contragredient duality preserves indecomposability in the forward direction.

theorem QuotientSubmoduleEquidistribution.Contragredient.reverseDualFunctor_indec (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] {N : FGModuleCat Rᵐᵒᵖ} (hN : Foundation.IsIndecomposableModule Rᵐᵒᵖ ↑N) : Foundation.IsIndecomposableModule R ↑((reverseDualFunctor K R).obj (Opposite.op N))

Contragredient duality preserves indecomposability in the reverse direction.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.dualMapLabel (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] [IsNoetherianRing Rᵐᵒᵖ] {ι : Type v} {κ : Type w} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton Rᵐᵒᵖ κ) (i : ι) : κ

The target label selected for the dual of a source representative.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.dualMapObjIso (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] [IsNoetherianRing Rᵐᵒᵖ] {ι : Type v} {κ : Type w} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton Rᵐᵒᵖ κ) (i : ι) : (dualFunctor K R).obj (Opposite.op (σ.obj i)) ≅ τ.obj (dualMapLabel K R σ τ i)

The chosen target representative is isomorphic to the forward dual.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.reverseMapLabel (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] [IsNoetherianRing Rᵐᵒᵖ] {ι : Type v} {κ : Type w} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton Rᵐᵒᵖ κ) (j : κ) : ι

The source label selected for the reverse dual of a target representative.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.reverseMapObjIso (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] [IsNoetherianRing Rᵐᵒᵖ] {ι : Type v} {κ : Type w} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton Rᵐᵒᵖ κ) (j : κ) : (reverseDualFunctor K R).obj (Opposite.op (τ.obj j)) ≅ σ.obj (reverseMapLabel K R σ τ j)

The chosen source representative is isomorphic to the reverse dual.

theorem QuotientSubmoduleEquidistribution.Contragredient.reverseMapLabel_dualMapLabel (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] [IsNoetherianRing Rᵐᵒᵖ] {ι : Type v} {κ : Type w} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton Rᵐᵒᵖ κ) (i : ι) : reverseMapLabel K R σ τ (dualMapLabel K R σ τ i) = i

Forward and reverse label selection compose to the identity on the source skeleton.

theorem QuotientSubmoduleEquidistribution.Contragredient.dualMapLabel_reverseMapLabel (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] [IsNoetherianRing Rᵐᵒᵖ] {ι : Type v} {κ : Type w} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton Rᵐᵒᵖ κ) (j : κ) : dualMapLabel K R σ τ (reverseMapLabel K R σ τ j) = j

Forward and reverse label selection compose to the identity on the target skeleton.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.dualLabelEquiv (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] [IsNoetherianRing Rᵐᵒᵖ] {ι : Type v} {κ : Type w} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton Rᵐᵒᵖ κ) : ι ≃ κ

The induced equivalence of arbitrary complete duplicate-free chosen indecomposable skeletons.

noncomputable def QuotientSubmoduleEquidistribution.Contragredient.alignedBiduality (K R : Type u) [Field K] [Ring R] [Algebra K R] [FiniteDimensional K R] [IsNoetherianRing R] [IsNoetherianRing Rᵐᵒᵖ] {ι : Type v} {κ : Type w} (σ : IndecomposableSkeleton R ι) (τ : IndecomposableSkeleton Rᵐᵒᵖ κ) : σ.AlignedBiduality τ

The concrete duality aligned with the two chosen skeletons.