Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleCoordinateEvaluationImage

Indexed coordinate images under generated-relations quotients #

source
def MagnitudeConjecture.RightModule.coordinateEvaluation {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) (Q : FinitelyGeneratedCategory A) (v : ↥(idempotentCoordinate e Q)) (X : FinitelyGeneratedCategory A) :
(Q ⟶ X) →ₗ[k] ↥(idempotentCoordinate e X)

Evaluation at a chosen vector of Qe, with values in Xe.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.coordinateEvaluation_eq_precomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} (he : IsIdempotentElem e) (Q X : FinitelyGeneratedCategory A) (u : rightIdealFGObj e ⟶ Q) (f : Q ⟶ X) :
    (coordinateEvaluation e Q ((rightIdealHomCoordinateEquiv he Q) u) X) f = (rightIdealHomCoordinateEquiv he X) (CategoryTheory.CategoryStruct.comp u f)

    Evaluation is precomposition from eA expressed in idempotent coordinates.

    source
    def MagnitudeConjecture.RightModule.coordinateEvaluationImage {k A : Type u} [Field k] [Ring A] [Algebra k A] (e : A) (Q : FinitelyGeneratedCategory A) (v : ↥(idempotentCoordinate e Q)) (X : FinitelyGeneratedCategory A) :
    Submodule k ↥(idempotentCoordinate e X)

    The indexed subspace generated by evaluating maps out of Q at v.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.coordinateEvaluation_comp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (Q : FinitelyGeneratedCategory A) (v : ↥(idempotentCoordinate e Q)) {X Y : FinitelyGeneratedCategory A} (f : Q ⟶ X) (q : X ⟶ Y) :
      (coordinateEvaluation e Q v Y) (CategoryTheory.CategoryStruct.comp f q) = (idempotentCoordinateMap e q) ((coordinateEvaluation e Q v X) f)

      Evaluation commutes with passage along a module morphism.

      source
      theorem MagnitudeConjecture.RightModule.coordinateEvaluationImage_map_eq_of_lift {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) (Q : FinitelyGeneratedCategory A) (v : ↥(idempotentCoordinate e Q)) {X Y : FinitelyGeneratedCategory A} (q : X ⟶ Y) (hlift : ∀ (f : Q ⟶ Y), ∃ (g : Q ⟶ X), CategoryTheory.CategoryStruct.comp g q = f) :
      Submodule.map (idempotentCoordinateMap e q) (coordinateEvaluationImage e Q v X) = coordinateEvaluationImage e Q v Y

      Lifting every map from Q identifies its indexed subspace in the target with the image of the indexed subspace in the source.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsQuotient_coordinateImage {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 : ↥(idempotentCoordinate e (S.fgObj ↑↑p))) (V : FinitelyGeneratedCategory A) (R : Submodule k ↥(idempotentCoordinate e V)) :
      Submodule.map (idempotentCoordinateMap e (quotientFGMap V (generatedCoordinateRelations e V R))) (coordinateEvaluationImage e (S.fgObj ↑↑p) v V) = coordinateEvaluationImage e (S.fgObj ↑↑p) v (quotientFGObj V (generatedCoordinateRelations e V R))

      The indexed subspace of the actual generated-relations quotient is the image of the presentation's indexed subspace.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.generatedRelationsQuotient_coordinateImage_target {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)] [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {e : A} (D : PrimitiveIdempotentData e) (p : S.FactorProjectiveLabel (S.primitiveKilledLabels D)) (v : ↥(idempotentCoordinate e (S.fgObj ↑↑p))) (V : FinitelyGeneratedCategory A) {W : Type u} [AddCommGroup W] [Module k W] (π : ↥(idempotentCoordinate e V) →ₗ[k] W) (hπ : Function.Surjective ⇑π) :
      Submodule.map (↑(S.directedGeneratedRelations_coordinateEquivTarget H D V π hπ)) (coordinateEvaluationImage e (S.fgObj ↑↑p) v (quotientFGObj V (generatedCoordinateRelations e V π.ker))) = Submodule.map π (coordinateEvaluationImage e (S.fgObj ↑↑p) v V)

      Under Me≃W, the quotient indexed subspace is exactly π of the presentation indexed subspace.