The primitive projective boundary is an incidence category #
The root projective and the non-root projectives indexed by T form the
incidence category of the poset obtained by adjoining a new least element to
the dual of T. This file records that statement without introducing a
second category: boundaryLE q r is exactly the condition for a morphism
from the boundary object indexed by q to the one indexed by r.
The normalized morphisms are the root identity, the chosen maps P ⟶ P_t,
and the normalized incidence maps P_t ⟶ P_s. Every boundary morphism is a
unique scalar multiple of the corresponding normalized morphism, and all
off-incidence Hom spaces vanish.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryUnit_spans
{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 : Option T)
(a : R.representableData.source ⟶ R.representableData.boundaryFamily q)
:
∃ (c : k), c • R.representableData.boundaryUnit q = a
The root identity and each chosen P ⟶ P_t span the corresponding
root-to-boundary Hom space.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryIncidenceMap
{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 : Option T}
(hqr : PosetSpace.boundaryLE q r)
:
The normalized boundary morphism attached to an incidence relation.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryUnit_comp_boundaryIncidenceMap
{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 : Option T}
(hqr : PosetSpace.boundaryLE q r)
:
CategoryTheory.CategoryStruct.comp (R.representableData.boundaryUnit q) (R.boundaryIncidenceMap hqr) = R.representableData.boundaryUnit r
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryUnit_comp_boundaryIncidenceMap_assoc
{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 : Option T}
(hqr : PosetSpace.boundaryLE q r)
{Z : S.FactorCategory K}
(h : R.representableData.boundaryFamily r ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (R.representableData.boundaryUnit q)
(CategoryTheory.CategoryStruct.comp (R.boundaryIncidenceMap hqr) h) = CategoryTheory.CategoryStruct.comp (R.representableData.boundaryUnit r) h
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryIncidenceMap_ne_zero
{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 : Option T}
(hqr : PosetSpace.boundaryLE q r)
:
R.boundaryIncidenceMap hqr ≠ 0
Every normalized boundary incidence morphism is nonzero.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.projective_to_source_eq_zero
{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)
(t : T)
(f : R.projective t ⟶ R.representableData.source)
:
f = 0
There are no morphisms from a non-root boundary projective back to the
root. A nonzero such map together with P ⟶ P_t would give a directed
two-cycle between distinct surviving labels.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryHom_eq_zero_of_not_le
{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)
{q r : Option T}
(hqr : ¬PosetSpace.boundaryLE q r)
(f : R.representableData.boundaryFamily q ⟶ R.representableData.boundaryFamily r)
:
f = 0
Off the augmented incidence relation, the corresponding boundary Hom space is zero.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.exists_smul_boundaryIncidenceMap_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)
{q r : Option T}
(hqr : PosetSpace.boundaryLE q r)
(f : R.representableData.boundaryFamily q ⟶ R.representableData.boundaryFamily r)
:
∃ (c : k), c • R.boundaryIncidenceMap hqr = f
Every morphism along the augmented incidence relation is a scalar multiple of its normalized incidence morphism.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryIncidenceMap_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)
{q r s : Option T}
(hqr : PosetSpace.boundaryLE q r)
(hrs : PosetSpace.boundaryLE r s)
:
CategoryTheory.CategoryStruct.comp (R.boundaryIncidenceMap hqr) (R.boundaryIncidenceMap hrs) = R.boundaryIncidenceMap ⋯
The normalized boundary morphisms have literal incidence composition.
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryIncidenceMap_refl
{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 : Option T)
:
R.boundaryIncidenceMap ⋯ = CategoryTheory.CategoryStruct.id R.representableData.boundaryFamily q
The normalized boundary morphism of a reflexive incidence relation is the identity.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryIncidenceScalarLinearMap
{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 : Option T}
(hqr : PosetSpace.boundaryLE q r)
:
k →ₗ[k] R.representableData.boundaryFamily q ⟶ R.representableData.boundaryFamily r
Scalar multiples of a normalized boundary incidence morphism, as a linear map from the coefficient field.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryHomCoordinateEquiv
{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 : Option T}
(hqr : PosetSpace.boundaryLE q r)
:
(R.representableData.boundaryFamily q ⟶ R.representableData.boundaryFamily r) ≃ₗ[k] k
Every on-incidence boundary Hom space is canonically one-dimensional, with the normalized incidence morphism as basis vector.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryHomCoordinateEquiv_symm_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)
{q r : Option T}
(hqr : PosetSpace.boundaryLE q r)
(c : k)
:
(R.boundaryHomCoordinateEquiv hqr).symm c = c • R.boundaryIncidenceMap hqr
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryHomCoordinateEquiv_incidenceMap
{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 : Option T}
(hqr : PosetSpace.boundaryLE q r)
:
(R.boundaryHomCoordinateEquiv hqr) (R.boundaryIncidenceMap hqr) = 1
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryHomCoordinateEquiv_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)
{q r s : Option T}
(hqr : PosetSpace.boundaryLE q r)
(hrs : PosetSpace.boundaryLE r s)
(f : R.representableData.boundaryFamily q ⟶ R.representableData.boundaryFamily r)
(g : R.representableData.boundaryFamily r ⟶ R.representableData.boundaryFamily s)
:
(R.boundaryHomCoordinateEquiv ⋯) (CategoryTheory.CategoryStruct.comp f g) = (R.boundaryHomCoordinateEquiv hqr) f * (R.boundaryHomCoordinateEquiv hrs) g
Boundary coordinates multiply under composition exactly as incidence coefficients do.