The quotient used in generated-relations realization #
def
MagnitudeConjecture.RightModule.quotientFGShortComplex
{A : Type u}
[Ring A]
[IsNoetherianRing Aᵐᵒᵖ]
(V : FinitelyGeneratedCategory A)
(K : Submodule Aᵐᵒᵖ ↑V)
:
CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)
The canonical submodule-quotient sequence of finite right modules.
Instances For
theorem
MagnitudeConjecture.RightModule.quotientFGShortComplex_shortExact
{A : Type u}
[Ring A]
[IsNoetherianRing Aᵐᵒᵖ]
(V : FinitelyGeneratedCategory A)
(K : Submodule Aᵐᵒᵖ ↑V)
:
(quotientFGShortComplex V K).ShortExact
The finite submodule-quotient sequence is short exact.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsQuotient_hom_lift
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
[CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)]
{e : A}
(D : PrimitiveIdempotentData e)
(p : S.FactorProjectiveLabel (S.primitiveKilledLabels D))
(V : FinitelyGeneratedCategory A)
(R : Submodule k ↥(idempotentCoordinate e V))
(f : S.fgObj ↑↑p ⟶ quotientFGObj V (generatedCoordinateRelations e V R))
:
∃ (g : S.fgObj ↑↑p ⟶ V), CategoryTheory.CategoryStruct.comp g (quotientFGMap V (generatedCoordinateRelations e V R)) = f
Every map from a factor tau-projective to the generated-relations quotient lifts to its presentation module.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directedGeneratedRelations_coordinateEquivTarget
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
[IsAlgClosed k]
(H : S.HasAcyclicNonzeroNonisomorphisms)
{e : A}
(D : PrimitiveIdempotentData e)
(V : FinitelyGeneratedCategory A)
{W : Type u}
[AddCommGroup W]
[Module k W]
(π : ↥(idempotentCoordinate e V) →ₗ[k] W)
(hπ : Function.Surjective ⇑π)
:
↥(idempotentCoordinate e (quotientFGObj V (generatedCoordinateRelations e V π.ker))) ≃ₗ[k] W
The generated-relations quotient realizes a prescribed coordinate surjection in the directed primitive setup.