Generated-relations quotients inside the literal factor category #
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsFactorObj
{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)
(X : S.FactorCategory (S.primitiveKilledLabels D))
(R : Submodule k ↥(idempotentCoordinate e X.as.obj))
:
S.FactorCategory (S.primitiveKilledLabels D)
The generated-relations quotient of the underlying module of a factor object, returned to the same literal factor category.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsFactorMap
{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)
(X : S.FactorCategory (S.primitiveKilledLabels D))
(R : Submodule k ↥(idempotentCoordinate e X.as.obj))
:
X ⟶ S.generatedRelationsFactorObj D X R
The presentation-to-quotient map in the literal factor category.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsFactorMap_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))
(X : S.FactorCategory (S.primitiveKilledLabels D))
(R : Submodule k ↥(idempotentCoordinate e X.as.obj))
(f : S.factorObject (S.primitiveKilledLabels D) ↑p ⟶ S.generatedRelationsFactorObj D X R)
:
∃ (g : S.factorObject (S.primitiveKilledLabels D) ↑p ⟶ X),
CategoryTheory.CategoryStruct.comp g (S.generatedRelationsFactorMap D X R) = f
Maps from each factor tau-projective lift through the new quotient, with all objects and morphisms in the factor category used by realization.