Opposite primitive-projective presentations

Regular Hom-duality converts a complete primitive-projective presentation of a finite-dimensional algebra into one for the opposite algebra. On the selected projective categories it is an anti-equivalence preserving the radical and its square. Hence it reverses ordinary-quiver arrows and converts the outgoing degree bound for biserial presentations into the corresponding incoming bound.

theorem MagnitudeConjecture.RightModule.rightIdealHomCoordinateEquiv_comp_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e f g : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (a : rightIdealFGObj e ⟶ rightIdealFGObj f) (b : rightIdealFGObj f ⟶ rightIdealFGObj g) : ↑↑((rightIdealHomCoordinateEquiv he (rightIdealFGObj g)) (CategoryTheory.CategoryStruct.comp a b)) = ↑↑((rightIdealHomCoordinateEquiv hf (rightIdealFGObj g)) b) * ↑↑((rightIdealHomCoordinateEquiv he (rightIdealFGObj f)) a)

theorem MagnitudeConjecture.RightModule.leftIdealHom_apply_val {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e f : A} (hf : IsIdempotentElem f) (h : leftIdealFGObj f ⟶ leftIdealFGObj e) (z : ↑(leftIdealFGObj f)) : ↑((ModuleCat.Hom.hom h.hom) z) = ↑z * ↑((ModuleCat.Hom.hom h.hom) (leftIdealGenerator f))

def MagnitudeConjecture.RightModule.rightIdealIsoOfLeftIdealIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (i : leftIdealFGObj e ≅ leftIdealFGObj f) : rightIdealFGObj e ≅ rightIdealFGObj f

An isomorphism between primitive left ideals induces one between the corresponding primitive right ideals.

def MagnitudeConjecture.RightModule.regularHomDualRightIdealLinearEquiv {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) : regularHomDualCarrier (rightIdealFGObj e) ≃ₗ[A] ↥(leftIdeal e)

Evaluation at the generator identifies the regular Hom-dual of eA with the corresponding left ideal Ae.

def MagnitudeConjecture.RightModule.regularHomDualRightIdealIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) : regularHomDualFGObj k (rightIdealFGObj e) ≅ leftIdealFGObj e

Categorical form of the regular-Hom identification Hom_A(eA,A) ≅ Ae.

@[simp]

theorem MagnitudeConjecture.RightModule.regularHomDualMap_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {P Q T : FGModuleCat Aᵐᵒᵖ} (d : P ⟶ Q) (e : Q ⟶ T) : regularHomDualMap (CategoryTheory.CategoryStruct.comp d e) = CategoryTheory.CategoryStruct.comp (regularHomDualMap e) (regularHomDualMap d)

@[simp]

theorem MagnitudeConjecture.RightModule.regularHomDualMap_id {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (P : FGModuleCat Aᵐᵒᵖ) : regularHomDualMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (regularHomDualFGObj k P)

@[simp]

theorem MagnitudeConjecture.RightModule.regularHomDualMap_add {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {P Q : FGModuleCat Aᵐᵒᵖ} (d e : P ⟶ Q) : regularHomDualMap (d + e) = regularHomDualMap d + regularHomDualMap e

@[simp]

theorem MagnitudeConjecture.RightModule.regularHomDualMap_smul {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {P Q : FGModuleCat Aᵐᵒᵖ} (c : k) (d : P ⟶ Q) : regularHomDualMap (c • d) = c • regularHomDualMap d

def MagnitudeConjecture.RightModule.regularHomDualMapIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {P Q : FGModuleCat Aᵐᵒᵖ} (i : P ≅ Q) : regularHomDualFGObj k Q ≅ regularHomDualFGObj k P

Regular Hom sends an isomorphism of right modules to the reversed isomorphism of left modules.

theorem MagnitudeConjecture.RightModule.regularHomDualMap_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (P Q : FGModuleCat Aᵐᵒᵖ) [CategoryTheory.Projective Q] : Function.Injective fun (d : P ⟶ Q) => regularHomDualMap d

Regular Hom-duality is faithful on finite projective right modules.

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeIdempotents_complete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : CompleteOrthogonalIdempotents P.oppositeIdempotent

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositePrimitive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : PrimitiveIdempotentData (P.oppositeIdempotent p)

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveCoordinateIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : rightIdealFGObj (P.oppositeIdempotent p) ≅ S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate p).label

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveCoordinate_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : Function.Surjective P.oppositeProjectiveCoordinate

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveCoordinate_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : Function.Injective P.oppositeProjectiveCoordinate

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

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

The primitive projective presentation of the opposite algebra obtained by opposing and then reindexing the original complete primitive family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositePresentation_isBiserial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing A] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hP : P.IsBiserial) : P.oppositePresentation.IsBiserial

Biseriality is symmetric under passage to the opposite primitive projective presentation.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeRegularEquivalence_preimage_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {X Y : FGModuleCat Aᵐᵒᵖᵐᵒᵖ} (f : MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeRegularEquivalence✝.functor.obj X ⟶ MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeRegularEquivalence✝.functor.obj Y) (x : ↑X) : (ModuleCat.Hom.hom (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeRegularEquivalence✝.functor.preimage f).hom) x = (ModuleCat.Hom.hom f.hom) x

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveRegularHomIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeRegularEquivalence✝.functor.obj (rightIdealFGObj (P.oppositeIdempotent p)) ≅ regularHomDualFGObj k (S.fgObj p.label)

The opposite principal projective at p, after restriction along the double-opposite equivalence, is the regular Hom-dual of the original selected projective at p.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.fgObj q.label ⟶ S.fgObj p.label) : S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate p).label ⟶ S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate q).label

The morphism map of regular Hom-duality, realized between the selected projectives on the two sides.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMap_literal_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.fgObj q.label ⟶ S.fgObj p.label) (x : ↥(rightIdeal (P.oppositeIdempotent p))) : ↑((ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (P.oppositeProjectiveCoordinateIso p).hom (CategoryTheory.CategoryStruct.comp (P.oppositeProjectiveMap f) (P.oppositeProjectiveCoordinateIso q).inv)).hom) x) = MulOpposite.op (MulOpposite.unop ↑x * ↑((ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (P.primitiveProjectiveIso q).hom (CategoryTheory.CategoryStruct.comp f (P.primitiveProjectiveIso p).inv)).hom) (rightIdealGenerator (P.idempotent q))))

In literal principal-projective coordinates, regular Hom-duality sends an element of the opposite right ideal to right multiplication by the original projective-map coordinate.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMap_id {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : P.oppositeProjectiveMap (CategoryTheory.CategoryStruct.id (S.fgObj p.label)) = CategoryTheory.CategoryStruct.id (S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate p).label)

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMap_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q r : S.ProjectiveLabel} (f : S.fgObj q.label ⟶ S.fgObj p.label) (g : S.fgObj r.label ⟶ S.fgObj q.label) : P.oppositeProjectiveMap (CategoryTheory.CategoryStruct.comp g f) = CategoryTheory.CategoryStruct.comp (P.oppositeProjectiveMap f) (P.oppositeProjectiveMap g)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMapPreimage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (h : S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate p).label ⟶ S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate q).label) : S.fgObj q.label ⟶ S.fgObj p.label

Recover the original projective morphism from its realized regular-Hom dual.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMap_preimage {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (h : S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate p).label ⟶ S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate q).label) : P.oppositeProjectiveMap (P.oppositeProjectiveMapPreimage h) = h

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMapPreimage_map {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.fgObj q.label ⟶ S.fgObj p.label) : P.oppositeProjectiveMapPreimage (P.oppositeProjectiveMap f) = f

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMap_add {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f g : S.fgObj q.label ⟶ S.fgObj p.label) : P.oppositeProjectiveMap (f + g) = P.oppositeProjectiveMap f + P.oppositeProjectiveMap g

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveMap_smul {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (c : k) (f : S.fgObj q.label ⟶ S.fgObj p.label) : P.oppositeProjectiveMap (c • f) = c • P.oppositeProjectiveMap f

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveHomLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) : (S.fgObj q.label ⟶ S.fgObj p.label) ≃ₗ[k] S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate p).label ⟶ S.contragredientSkeleton.fgObj (P.oppositeProjectiveCoordinate q).label

Regular Hom-duality is a linear equivalence on every selected projective Hom space.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : CategoryTheory.Functor S.ProjectiveCategoryᵒᵖ S.contragredientSkeleton.ProjectiveCategory

Regular Hom-duality on the selected projectives, realized in the opposite algebra's selected projective category.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveFunctor_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : P.oppositeProjectiveFunctor.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveFunctor_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : CategoryTheory.Functor.Linear k P.oppositeProjectiveFunctor

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveFunctorFullyFaithful {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : P.oppositeProjectiveFunctor.FullyFaithful

Regular Hom-duality is fully faithful on the selected projective subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.oppositeProjectiveFunctor_obj_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) : Function.Surjective P.oppositeProjectiveFunctor.obj

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

Regular Hom-duality is an equivalence from the opposite selected projective category to the selected projectives of the opposite algebra.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveOppositeHomLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) : (S.ordinaryProjectiveObj q ⟶ S.ordinaryProjectiveObj p) ≃ₗ[k] S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate p) ⟶ S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate q)

The Hom-space form of the selected-projective anti-equivalence.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveOppositeHomLinearEquiv_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj q ⟶ S.ordinaryProjectiveObj p) : (P.projectiveOppositeHomLinearEquiv p q) f = P.oppositeProjectiveFunctor.map f.op

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveOppositeHomLinearEquiv_mem_radical_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj q ⟶ S.ordinaryProjectiveObj p) : (P.projectiveOppositeHomLinearEquiv p q) f ∈ S.contragredientSkeleton.projectiveNilpotentRadicalData.ideal.hom (S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate p)) (S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate q)) ↔ f ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj q) (S.ordinaryProjectiveObj p)

The selected-projective anti-equivalence preserves and reflects the categorical radical.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveOppositeHomLinearEquiv_mem_radicalSquare_of_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (f : S.ordinaryProjectiveObj q ⟶ S.ordinaryProjectiveObj p) (hf : f ∈ (S.projectiveNilpotentRadicalData.ideal.pow 2).hom (S.ordinaryProjectiveObj q) (S.ordinaryProjectiveObj p)) : (P.projectiveOppositeHomLinearEquiv p q) f ∈ (S.contragredientSkeleton.projectiveNilpotentRadicalData.ideal.pow 2).hom (S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate p)) (S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate q))

The selected-projective anti-equivalence sends the square of the projective radical into the opposite projective radical square.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveOppositeHomLinearEquiv_symm_mem_radicalSquare_of_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) {p q : S.ProjectiveLabel} (h : S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate p) ⟶ S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate q)) (hh : h ∈ (S.contragredientSkeleton.projectiveNilpotentRadicalData.ideal.pow 2).hom (S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate p)) (S.contragredientSkeleton.ordinaryProjectiveObj (P.oppositeProjectiveCoordinate q))) : (P.projectiveOppositeHomLinearEquiv p q).symm h ∈ (S.projectiveNilpotentRadicalData.ideal.pow 2).hom (S.ordinaryProjectiveObj q) (S.ordinaryProjectiveObj p)

Reflection of the radical square under the selected-projective anti-equivalence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveRadicalOppositeLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) : ↥(S.projectiveRadicalSubmodule p q) ≃ₗ[k] ↥(S.contragredientSkeleton.projectiveRadicalSubmodule (P.oppositeProjectiveCoordinate q) (P.oppositeProjectiveCoordinate p))

Restriction of the selected-projective anti-equivalence to radical Hom spaces.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveRadicalOppositeLinearEquiv_mem_square_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) (f : ↥(S.projectiveRadicalSubmodule p q)) : (P.projectiveRadicalOppositeLinearEquiv p q) f ∈ S.contragredientSkeleton.projectiveRadicalSquareInRadicalSubmodule (P.oppositeProjectiveCoordinate q) (P.oppositeProjectiveCoordinate p) ↔ f ∈ S.projectiveRadicalSquareInRadicalSubmodule p q

The radical anti-equivalence carries the square-inside-radical submodule onto the corresponding opposite submodule.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveIrreducibleOppositeLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) : S.projectiveIrreducibleHomSpace p q ≃ₗ[k] S.contragredientSkeleton.projectiveIrreducibleHomSpace (P.oppositeProjectiveCoordinate q) (P.oppositeProjectiveCoordinate p)

Regular Hom-duality descends from radical morphisms to irreducible projective morphisms.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.finrank_projectiveIrreducibleHomSpace_eq_opposite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p q : S.ProjectiveLabel) : Module.finrank k (S.projectiveIrreducibleHomSpace p q) = Module.finrank k (S.contragredientSkeleton.projectiveIrreducibleHomSpace (P.oppositeProjectiveCoordinate q) (P.oppositeProjectiveCoordinate p))

Opposite regular Hom-duality preserves the dimensions of irreducible projective-morphism spaces, with source and target reversed.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ordinaryCostar_card_eq_oppositeStar_card {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (x : S.ProjectiveLabel) : Nat.card (Quiver.Costar x) = Nat.card (Quiver.Star (P.oppositeProjectiveCoordinate x))

The incoming ordinary-quiver degree over the original algebra is the outgoing degree at the corresponding projective over the opposite algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.ordinaryCostar_card_le_two_of_isBiserial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsNoetherianRing A] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) [IsAlgClosed k] (hP : P.IsBiserial) (x : S.ProjectiveLabel) : Nat.card (Quiver.Costar x) ≤ 2

Biseriality bounds the incoming as well as the outgoing ordinary-quiver degree at every selected projective.