Maps between the selected representatives of Schur poset spaces #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurMap
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
{X Y : PosetSpace.Obj k B.ProjectivePoset}
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
(hY : PosetSpace.IsSchur k B.ProjectivePoset Y)
(f : X ⟶ Y)
:
S.factorObject (S.primitiveKilledLabels D) (B.directFactorSchurLabel X hX) ⟶ S.factorObject (S.primitiveKilledLabels D) (B.directFactorSchurLabel Y hY)
Transport a poset-space map to the selected factor representatives.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurMap_comp
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
{X Y Z : PosetSpace.Obj k B.ProjectivePoset}
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
(hY : PosetSpace.IsSchur k B.ProjectivePoset Y)
(hZ : PosetSpace.IsSchur k B.ProjectivePoset Z)
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
B.directFactorSchurMap hX hZ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (B.directFactorSchurMap hX hY f) (B.directFactorSchurMap hY hZ g)
Composition of maps survives the choice of representatives.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurMap_ne_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
{X Y : PosetSpace.Obj k B.ProjectivePoset}
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
(hY : PosetSpace.IsSchur k B.ProjectivePoset Y)
(f : X ⟶ Y)
(hf : f ≠ 0)
:
B.directFactorSchurMap hX hY f ≠ 0
Nonzero maps remain nonzero after transport.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorSchurLabel_ne_of_not_iso
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
{X Y : PosetSpace.Obj k B.ProjectivePoset}
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
(hY : PosetSpace.IsSchur k B.ProjectivePoset Y)
(hne : ¬Nonempty (X ≅ Y))
:
B.directFactorSchurLabel X hX ≠ B.directFactorSchurLabel Y hY
Nonisomorphic Schur spaces have distinct selected factor labels.