The direct height grading on Schur poset spaces #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directPosetSpaceEquivalence
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
:
S.FactorCategory (S.primitiveKilledLabels D) ≌ PosetSpace.Obj k B.ProjectivePoset
The generated-relations equivalence for the canonical projective poset.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.exists_directFactorLabelIso_of_isSchur
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(X : PosetSpace.Obj k B.ProjectivePoset)
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
:
∃ (x : S.SurvivingLabel (S.primitiveKilledLabels D)),
Nonempty (B.directPosetSpaceEquivalence.inverse.obj X ≅ S.factorObject (S.primitiveKilledLabels D) x)
A Schur poset space pulls back along the primitive equivalence to one selected indecomposable factor object.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurLabel
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(X : PosetSpace.Obj k B.ProjectivePoset)
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
:
S.SurvivingLabel (S.primitiveKilledLabels D)
The selected factor label representing a Schur poset space.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurIso
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(X : PosetSpace.Obj k B.ProjectivePoset)
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
:
B.directPosetSpaceEquivalence.inverse.obj X ≅ S.factorObject (S.primitiveKilledLabels D) (B.directFactorSchurLabel X hX)
The pullback of a Schur poset space is isomorphic to its selected factor label.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurLevel
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(X : PosetSpace.Obj k B.ProjectivePoset)
:
ℕ
The direct factor height transported to a Schur poset space. Its value away from the Schur locus is irrelevant to the positive-grading interface.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurLevel_of_isSchur
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(X : PosetSpace.Obj k B.ProjectivePoset)
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
:
B.directFactorSchurLevel X = B.directFactorHeight (B.directFactorSchurLabel X hX)
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurPositiveGrading
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
:
The direct factor grading transports across the completed poset-space equivalence to a positive grading on every Schur poset space.