Literal category-algebra ideals generated by string arrows

The quotient path category is used in reversed orientation by the finite category-algebra construction. Consequently, a displayed quiver arrow induces a map between covariant representables whose pointwise images are indexed by the left continuations of that arrow. This file packages that map, its matrix coordinate in the finite category algebra, and the literal principal right ideal generated by that coordinate.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.quotientCategoryAlgebra {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : Type u

The finite category algebra attached to the quotient path category of a string presentation.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.quotientRepresentable {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (X : Category P.relations) : CoveringHom.FiniteDimensionalModuleCategory k

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModule {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) : FGModuleCat (CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯)ᵐᵒᵖ

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.vertexProjector {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) : P.quotientCategoryAlgebra

The projector onto the representable belonging to a displayed vertex.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowRepresentableMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : P.quotientRepresentable (obj P.relations x) ⟶ P.quotientRepresentable (obj P.relations y)

The map of covariant representables induced contravariantly by a displayed arrow of the quotient path category.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowRepresentableMap_app_hom {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : ModuleCat.Hom.hom ((P.arrowRepresentableMap a).hom.hom.app (obj P.relations z)) = P.leftArrowCompositionLinearMap a z

At a vertex z, the representable map belonging to a is precisely left composition by the categorical image of a.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowRepresentableCoordinateBasis {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Module.Basis (P.LeftContinuationAt a z) k ↥(ModuleCat.Hom.hom ((P.arrowRepresentableMap a).hom.hom.app (obj P.relations z))).range

The pointwise range of the assembled representable map has the literal left-continuation path basis.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.finrank_arrowRepresentableMap_range_eq_natCard {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : Q) : Module.finrank k ↥(ModuleCat.Hom.hom ((P.arrowRepresentableMap a).hom.hom.app (obj P.relations z))).range = Nat.card (P.LeftContinuationAt a z)

The pointwise dimension of the assembled representable arrow image is the number of surviving left continuations at that vertex.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowAlgebraCoordinate {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : P.quotientCategoryAlgebra

The matrix coordinate of a displayed arrow in the finite category algebra.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowAlgebraCoordinate_mul_sourceProjector {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : P.arrowAlgebraCoordinate a * P.vertexProjector x = P.arrowAlgebraCoordinate a

The arrow coordinate is fixed on the right by its source projector.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.targetProjector_mul_arrowAlgebraCoordinate {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : P.vertexProjector y * P.arrowAlgebraCoordinate a = P.arrowAlgebraCoordinate a

The arrow coordinate is fixed on the left by its target projector.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowProjectiveLinearMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : ↥(RightModule.rightIdeal (P.vertexProjector x)) →ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↥(RightModule.rightIdeal (P.vertexProjector y))

Left multiplication by the arrow coordinate, restricted from the source vertex projective to the target vertex projective.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowProjectiveLinearMap_apply_val {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) (z : ↥(RightModule.rightIdeal (P.vertexProjector x))) : ↑((P.arrowProjectiveLinearMap a) z) = P.arrowAlgebraCoordinate a * ↑z

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.vertexRightIdealRepresentedLinearEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) : ↥(RightModule.rightIdeal (P.vertexProjector x)) ≃ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↑(P.representedVertexModule x)

A vertex-projector right ideal is the right module represented by the matching covariant representable.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowLinearMap {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : ↑((CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor ⋯).obj (P.quotientRepresentable (obj P.relations x))).obj →ₗ[(CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯)ᵐᵒᵖ] ↑((CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor ⋯).obj (P.quotientRepresentable (obj P.relations y))).obj

The represented linear map induced by the arrow transformation.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.vertexRightIdealRepresentedLinearEquiv_arrowProjective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : ↑(P.vertexRightIdealRepresentedLinearEquiv y) ∘ₗ P.arrowProjectiveLinearMap a = P.representedArrowLinearMap a ∘ₗ ↑(P.vertexRightIdealRepresentedLinearEquiv x)

The projective map defined by multiplying with the arrow matrix is the represented map of the arrow transformation, after the canonical vertex identifications.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowProjectiveRangeRepresentedRangeLinearEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : ↥(P.arrowProjectiveLinearMap a).range ≃ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↥(P.representedArrowLinearMap a).range

The range of the projective arrow map is the represented range of the assembled arrow transformation.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowProjectiveRangeRightIdealLinearEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : ↥(P.arrowProjectiveLinearMap a).range ≃ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↥(RightModule.rightIdeal (P.arrowAlgebraCoordinate a))

The range of the projective map induced by an arrow is the literal principal right ideal generated by its category-algebra coordinate.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowRightIdealRepresentedRangeLinearEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : ↥(RightModule.rightIdeal (P.arrowAlgebraCoordinate a)) ≃ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↥(P.representedArrowLinearMap a).range

The literal principal right ideal generated by a displayed arrow is linearly equivalent to the represented range of the assembled arrow transformation.