The endomorphism algebra of the primitive boundary #
The root-plus-projective boundary is indexed by the finite poset obtained by
adjoining a bottom element to OrderDual T. Its opposite endomorphism ring
is therefore the ordinary incidence algebra of that augmented poset. This is
the ring-level form of the incidence-category calculation.
@[reducible, inline]
noncomputable abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceBoundaryFamily
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(q : PosetSpace.BoundaryIndex T)
:
S.FactorCategory K
The boundary family reindexed by its actual augmented incidence poset.
Instances For
@[reducible, inline]
noncomputable abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceBoundaryGenerator
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
:
S.FactorCategory K
The biproduct of the incidence-indexed boundary family.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndComponentAddHom
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(q r : PosetSpace.BoundaryIndex T)
:
CategoryTheory.End R.incidenceBoundaryGenerator →+ (R.incidenceBoundaryFamily q ⟶ R.incidenceBoundaryFamily r)
Taking a (q,r) component is additive in the boundary endomorphism.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndComponent
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : CategoryTheory.End R.incidenceBoundaryGenerator)
(q r : PosetSpace.BoundaryIndex T)
:
The (q,r) component of an endomorphism of the boundary generator.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndComponent_eq
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : CategoryTheory.End R.incidenceBoundaryGenerator)
(q r : PosetSpace.BoundaryIndex T)
:
R.boundaryEndComponent a q r = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι R.incidenceBoundaryFamily q)
(CategoryTheory.CategoryStruct.comp a (CategoryTheory.Limits.biproduct.π R.incidenceBoundaryFamily r))
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryMatrix
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(m : (q r : PosetSpace.BoundaryIndex T) → R.incidenceBoundaryFamily q ⟶ R.incidenceBoundaryFamily r)
:
CategoryTheory.End R.incidenceBoundaryGenerator
Assemble a universe-polymorphic matrix of boundary morphisms. Mathlib's
finite biproduct.matrix is intentionally small-universe, while the
representation-theoretic index type here lives in the algebra's universe.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndComponent_boundaryMatrix
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(m : (q r : PosetSpace.BoundaryIndex T) → R.incidenceBoundaryFamily q ⟶ R.incidenceBoundaryFamily r)
(q r : PosetSpace.BoundaryIndex T)
:
R.boundaryEndComponent (R.boundaryMatrix m) q r = m q r
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryMatrix_boundaryEndComponent
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : CategoryTheory.End R.incidenceBoundaryGenerator)
:
R.boundaryMatrix (R.boundaryEndComponent a) = a
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryBiproduct_total
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
:
∑ z : PosetSpace.BoundaryIndex T,
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π R.incidenceBoundaryFamily z)
(CategoryTheory.Limits.biproduct.ι R.incidenceBoundaryFamily z) = CategoryTheory.CategoryStruct.id R.incidenceBoundaryGenerator
The biproduct resolution of the identity, without Mathlib's small-index restriction on the corresponding convenience theorem.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndComponent_comp
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a b : CategoryTheory.End R.incidenceBoundaryGenerator)
(q r : PosetSpace.BoundaryIndex T)
:
R.boundaryEndComponent (CategoryTheory.CategoryStruct.comp a b) q r = ∑ z : PosetSpace.BoundaryIndex T,
CategoryTheory.CategoryStruct.comp (R.boundaryEndComponent a q z) (R.boundaryEndComponent b z r)
Matrix multiplication for boundary endomorphisms, stated with a universe-polymorphic finite sum.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndCoefficient
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : CategoryTheory.End R.incidenceBoundaryGenerator)
(q r : PosetSpace.BoundaryIndex T)
:
k
The scalar coordinate of one component of a boundary endomorphism.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndCoefficient_add
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a b : CategoryTheory.End R.incidenceBoundaryGenerator)
(q r : PosetSpace.BoundaryIndex T)
:
R.boundaryEndCoefficient (a + b) q r = R.boundaryEndCoefficient a q r + R.boundaryEndCoefficient b q r
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndCoordinate_component_comp
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
(a b : CategoryTheory.End R.incidenceBoundaryGenerator)
{q r : PosetSpace.BoundaryIndex T}
(hqr : q ≤ r)
(z : PosetSpace.BoundaryIndex T)
:
(R.boundaryHomCoordinateEquiv ⋯)
(CategoryTheory.CategoryStruct.comp (R.boundaryEndComponent a q z) (R.boundaryEndComponent b z r)) = R.boundaryEndCoefficient a q z * R.boundaryEndCoefficient b z r
The coordinate of a composable pair of arbitrary matrix components. If an intermediate index lies outside the interval, the corresponding component vanishes by acyclicity.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndCoefficient_comp
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
(a b : CategoryTheory.End R.incidenceBoundaryGenerator)
(q r : PosetSpace.BoundaryIndex T)
:
R.boundaryEndCoefficient (CategoryTheory.CategoryStruct.comp a b) q r = ∑ z ∈ Finset.Icc q r, R.boundaryEndCoefficient a q z * R.boundaryEndCoefficient b z r
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndToIncidence
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : CategoryTheory.End R.incidenceBoundaryGenerator)
:
IncidenceAlgebra k (PosetSpace.BoundaryIndex T)
An endomorphism of the boundary biproduct gives its incidence matrix.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceToBoundaryEnd
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : IncidenceAlgebra k (PosetSpace.BoundaryIndex T))
:
CategoryTheory.End R.incidenceBoundaryGenerator
Reassemble an incidence matrix as an endomorphism of the boundary biproduct.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndComponent_incidenceToBoundaryEnd
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : IncidenceAlgebra k (PosetSpace.BoundaryIndex T))
(q r : PosetSpace.BoundaryIndex T)
:
R.boundaryEndComponent (R.incidenceToBoundaryEnd a) q r = if hqr : q ≤ r then (R.boundaryHomCoordinateEquiv ⋯).symm (a q r) else 0
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndToIncidence_apply
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : CategoryTheory.End R.incidenceBoundaryGenerator)
(q r : PosetSpace.BoundaryIndex T)
:
(R.boundaryEndToIncidence a) q r = R.boundaryEndCoefficient a q r
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndToIncidence_incidenceToBoundaryEnd
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a : IncidenceAlgebra k (PosetSpace.BoundaryIndex T))
:
R.boundaryEndToIncidence (R.incidenceToBoundaryEnd a) = a
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceToBoundaryEnd_boundaryEndToIncidence
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
(a : CategoryTheory.End R.incidenceBoundaryGenerator)
:
R.incidenceToBoundaryEnd (R.boundaryEndToIncidence a) = a
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndToIncidence_add
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(a b : CategoryTheory.End R.incidenceBoundaryGenerator)
:
R.boundaryEndToIncidence (a + b) = R.boundaryEndToIncidence a + R.boundaryEndToIncidence b
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndToIncidence_comp
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
(a b : CategoryTheory.End R.incidenceBoundaryGenerator)
:
R.boundaryEndToIncidence (CategoryTheory.CategoryStruct.comp a b) = R.boundaryEndToIncidence a * R.boundaryEndToIncidence b
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryEndOppositeRingEquiv
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
{T : Type u}
[Fintype T]
[PartialOrder T]
(R : S.PrimitiveProjectivePosetData D T)
(H : S.HasAcyclicNonzeroNonisomorphisms)
:
(CategoryTheory.End R.incidenceBoundaryGenerator)ᵐᵒᵖ ≃+* IncidenceAlgebra k (PosetSpace.BoundaryIndex T)
The opposite endomorphism ring of the primitive boundary generator is
the incidence algebra of the augmented boundary poset. The opposite is
essential: multiplication in End is reverse categorical composition.