The projective Cartan matrix of a directed module skeleton #
This file constructs the integral Cartan matrix indexed by the chosen
indecomposable projective right modules. A linear extension of the ambient
nonzero-nonisomorphism relation makes this matrix upper unitriangular, so its
inverse is again integral. It also identifies the coordinate belonging to a
literal primitive idempotent with the already constructed multiplicity
dim_k Xe.
The application is local: Appendix A of the frozen manuscript first restricts the algebra to the support of the middle term of each Auslander--Reiten sequence. Accordingly this file exposes a local-support root-pair interface whose Cartan index may vary with the sequence. It deliberately contains no ambient weak-positivity compatibility route.
Reflexive transitive reachability through nonzero nonisomorphisms.
Instances For
Cycle-freeness makes nonzero-nonisomorphism reachability a partial order.
A chosen linear extension of nonzero-nonisomorphism reachability.
Instances For
The chosen linear order extends directed reachability.
In the chosen directed order, every nonzero off-diagonal map points strictly forward.
In the directed order there are no morphisms strictly backwards.
Labels of the chosen indecomposable projective right modules. This is a
structure, rather than a subtype abbreviation, so its proof-relevant directed
order cannot accidentally reuse the numerical order on Fin S.n.
- label : Fin S.n
Instances For
Labels of the chosen indecomposable injective right modules.
- label : Fin S.n
Instances For
The structured projective labels are equivalent to the corresponding subtype.
Instances For
The simple-coordinate support of a finitely generated right module, indexed by the chosen indecomposable projectives.
Instances For
A monomorphism can only enlarge projective support.
An epimorphism can only shrink projective support.
Isomorphic finitely generated modules have identical projective support.
Projective support of a finite biproduct is the union of the supports of its summands.
Regard the kernel map of the chosen nonprojective right almost-split sequence, with the same displayed middle decomposition, as a minimal left almost-split decomposition.
Instances For
The chosen middle-term decomposition represents projective support as the union of the supports of its indecomposable summands.
Both endpoint supports of an almost-split sequence lie in the support of its middle term.
If one left component of an Auslander--Reiten sequence is monic, every different right component is monic. This is the exactness step in Ringel's support argument.
Ringel's support lemma for the chosen Auslander--Reiten sequence: the support of the source, the endpoint, or one displayed indecomposable middle summand contains the supports of all the other terms.
Exactness identifies the support of the middle term with the union of the two endpoint supports.
One actual skeleton label occurring as the source, endpoint, or a middle summand is sincere on the support of the almost-split middle term.
The directed order restricted to the indecomposable projective labels.
Instances For
The integral Cartan matrix, with entry dim_k Hom(P_i,P_j).
Instances For
The projective Cartan matrix is entrywise nonnegative.
In the directed linear extension, the projective Cartan matrix is upper triangular.
Directedness and algebraic closedness give unit diagonal.
The projective Cartan determinant is one.
The integral inverse of the projective Cartan matrix.
Instances For
The displayed integral inverse is a left inverse.
The displayed integral inverse is a right inverse.
The projective-Hom dimension vector of a chosen indecomposable module.
Instances For
Projective-Hom dimension vectors are coordinatewise nonnegative.
A retract of a projective object is projective.
Every chosen indecomposable receives a nonzero map from a chosen indecomposable projective.
Every projective-Hom dimension vector is a positive integral vector.
An irreducible morphism points strictly forward in the chosen directed linear order.
Every nonzero morphism points weakly forward in the chosen directed order. This version intentionally permits coincident labels, which is what the support-algebra cycle argument in Appendix A needs.
A closed triangle of nonzero maps cannot contain an irreducible edge in a directed skeleton. The weak inequalities automatically absorb coincident terms, formalizing the manuscript's instruction to omit isomorphism edges from the displayed cycle.
A primitive idempotent determines its corresponding projective Cartan index.
Instances For
A primitive idempotent determines its corresponding injective label.
Instances For
The categorical form of the schurian corner bound used at both ambient boundaries in Appendix A.
- projectiveHom_le_one (p q : S.ProjectiveLabel) : Module.finrank k (S.fgObj p.label ⟶ S.fgObj q.label) ≤ 1
- injectiveHom_le_one (i j : S.InjectiveLabel) : Module.finrank k (S.fgObj i.label ⟶ S.fgObj j.label) ≤ 1
Instances For
The distinguished projective-Hom coordinate is exactly the literal
primitive multiplicity dim_k Xe.
The schurian projective Hom bound gives the projective clause of the primitive coordinate estimate.
The dual schurian injective Hom bound gives the injective clause of the primitive coordinate estimate.
The literal projective Cartan matrix of a directed support algebra, together with weak positivity of its Euler form, gives the numerical Cartan datum used in Appendix A.
Instances For
Concrete Cartan/root/Coxeter data for the two endpoints of one Auslander--Reiten sequence after passage to its middle-term support algebra.
The skeleton S here is the skeleton of that support algebra. In particular,
this is not an ambient compatibility interface: each sequence may instantiate
the structure with a different algebra and skeleton.
- weaklyPositive (v : S.ProjectiveLabel → ℤ) : CartanCoordinate.IsPositive v → 1 ≤ CartanCoordinate.quadraticForm S.projectiveCartanInverse v
- source_root : CartanCoordinate.quadraticForm S.projectiveCartanInverse (S.projectiveHomVector z) = 1
- translated_root : CartanCoordinate.quadraticForm S.projectiveCartanInverse (S.projectiveHomVector x) = 1
- coxeter_translate : S.projectiveHomVector x = Matrix.vecMul (S.projectiveHomVector z) (CartanCoordinate.coxeterMatrix S.projectiveCartanMatrix S.projectiveCartanInverse)
Instances For
Actual support-algebra Cartan data produces the local numerical root-pair package once the chosen simple coordinate has been identified at both endpoints.
Instances For
The concrete middle-term support-algebra data used by Appendix A.
For each ambient nonprojective label it records the support algebra, its duplicate-free finite indecomposable skeleton, the two restricted endpoint labels, and the projective coordinate corresponding to the selected simple. The Cartan/root/Coxeter field uses the actual projective Cartan matrix of that support skeleton.
- supportRing (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : Ring (self.supportAlgebra z)
- supportAlgebraMap (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : Algebra k (self.supportAlgebra z)
- supportFiniteDimensional (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : FiniteDimensional k (self.supportAlgebra z)
- supportNoetherian (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : IsNoetherianRing (self.supportAlgebra z)ᵐᵒᵖ
- skeleton (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : FiniteIndecomposableSkeleton k (self.supportAlgebra z)
- acyclic (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : (self.skeleton z).HasAcyclicNonzeroNonisomorphisms
- coordinate (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : S.primitiveSourceProjectiveLabel D ∈ S.projectiveSupport (S.minimalRightAlmostSplitAt ↑z).middle → (self.skeleton z).ProjectiveLabel
- rootPair (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) (_hsupport : S.primitiveSourceProjectiveLabel D ∈ S.projectiveSupport (S.minimalRightAlmostSplitAt ↑z).middle) : (self.skeleton z).SupportCartanRootPairData ⋯ (self.sourceLabel z) (self.translatedLabel z)
- source_coordinate (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) (hsupport : S.primitiveSourceProjectiveLabel D ∈ S.projectiveSupport (S.minimalRightAlmostSplitAt ↑z).middle) : (self.skeleton z).projectiveHomVector (self.sourceLabel z) (self.coordinate z hsupport) = ↑(S.primitiveMultiplicity D ↑z)
- translated_coordinate (z : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) (hsupport : S.primitiveSourceProjectiveLabel D ∈ S.projectiveSupport (S.minimalRightAlmostSplitAt ↑z).middle) : (self.skeleton z).projectiveHomVector (self.translatedLabel z) (self.coordinate z hsupport) = ↑(S.primitiveMultiplicity D (S.rightTranslationLabel z))
Instances For
The sequence-local support Cartan calculation gives the literal primitive coordinate estimate directly.