Primitive coordinates on arbitrary factor-category objects #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveFactorCoordinateEquiv
{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))
:
(S.factorObject (S.primitiveKilledLabels D) (S.primitiveMultiplicityInput D).source ⟶ X) ≃ₗ[k] ↥(idempotentCoordinate e X.as.obj)
The source-Hom space of a factor object is the e-coordinate of its underlying finite module.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveFactorCoordinateEquiv_map
{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))
(f : S.ambientAddPoint (S.primitiveSourceLabel D) ⟶ X.as)
:
(S.primitiveFactorCoordinateEquiv D X) ((S.factorFunctor (S.primitiveKilledLabels D)).map f) = (S.primitiveSourceHomCoordinateEquiv D X.as.obj) f.hom
The factor coordinate identification agrees with evaluation on any chosen ambient representative of a source map.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSourceHomCoordinateEquiv_comp
{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)
{V W : FinitelyGeneratedCategory A}
(f : S.fgObj (S.primitiveSourceLabel D) ⟶ V)
(q : V ⟶ W)
:
(S.primitiveSourceHomCoordinateEquiv D W) (CategoryTheory.CategoryStruct.comp f q) = (idempotentCoordinateMap e q) ((S.primitiveSourceHomCoordinateEquiv D V) f)
Evaluation is natural for a morphism of ambient finite modules.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveFactorCoordinateEquiv_comp_map
{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 Y : S.FactorCategory (S.primitiveKilledLabels D))
(f : S.factorObject (S.primitiveKilledLabels D) (S.primitiveMultiplicityInput D).source ⟶ X)
(q : X.as ⟶ Y.as)
:
(S.primitiveFactorCoordinateEquiv D Y)
(CategoryTheory.CategoryStruct.comp f ((S.factorFunctor (S.primitiveKilledLabels D)).map q)) = (idempotentCoordinateMap e q.hom) ((S.primitiveFactorCoordinateEquiv D X) f)
Naturality of factor coordinates for a specified ambient representative of a factor morphism.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsFactorMap_coordinate
{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))
(f : S.factorObject (S.primitiveKilledLabels D) (S.primitiveMultiplicityInput D).source ⟶ X)
:
(S.primitiveFactorCoordinateEquiv D (S.generatedRelationsFactorObj D X R))
(CategoryTheory.CategoryStruct.comp f (S.generatedRelationsFactorMap D X R)) = (idempotentCoordinateMap e (quotientFGMap X.as.obj (generatedCoordinateRelations e X.as.obj R)))
((S.primitiveFactorCoordinateEquiv D X) f)
The new factor quotient map induces the canonical coordinate quotient.