Quotients between bound-quiver category algebras

An inclusion between two generated relation ideals gives a full linear functor between the corresponding quotient path categories. Since this functor is bijective on objects, it induces a surjective homomorphism between their finite category algebras. This is the algebraic quotient map used by the path-support-hull construction.

noncomputable def MagnitudeConjecture.BoundQuiver.quotientKerAlgEquivOfSurjective {k : Type u} [Field k] {A B : Type u} [Ring A] [Ring B] [Algebra k A] [Algebra k B] (f : A →ₐ[k] B) (hf : Function.Surjective ⇑f) : (TwoSidedIdeal.ker f).ringCon.Quotient ≃ₐ[k] B

The first isomorphism theorem, stated for Mathlib's noncommutative two-sided kernel ideal rather than directly for RingCon.ker.

noncomputable def MagnitudeConjecture.BoundQuiver.relationQuotientFunctor {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) : CategoryTheory.Functor (Category R) (Category S)

The linear functor between relation quotients induced by inclusion of their generated two-sided Hom ideals.

instance MagnitudeConjecture.BoundQuiver.relationQuotientFunctor_additive {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) : (relationQuotientFunctor hRS).Additive

The relation-quotient functor is additive.

instance MagnitudeConjecture.BoundQuiver.relationQuotientFunctor_linear {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) : CategoryTheory.Functor.Linear k (relationQuotientFunctor hRS)

The relation-quotient functor is linear.

instance MagnitudeConjecture.BoundQuiver.relationQuotientFunctor_full {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) : (relationQuotientFunctor hRS).Full

The relation-quotient functor is full.

noncomputable def MagnitudeConjecture.BoundQuiver.relativeRelationHomIdeal {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal (Category R)

The relative relation Hom ideal: morphisms in the first quotient which become zero after enlarging the relation ideal.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.mem_relativeRelationHomIdeal_iff {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) {X Y : Category R} (f : X ⟶ Y) : f ∈ (relativeRelationHomIdeal hRS).hom X Y ↔ (relationQuotientFunctor hRS).map f = 0

theorem MagnitudeConjecture.BoundQuiver.mem_relativeRelationHomIdeal_iff_exists_lift {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) {X Y : Category R} (f : X ⟶ Y) : f ∈ (relativeRelationHomIdeal hRS).hom X Y ↔ ∃ (g : X.as ⟶ Y.as), (LinearPathCategory.HomogeneousQuotient.quotientFunctor R).map g = f ∧ g ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X.as Y.as

A morphism belongs to the relative relation Hom ideal exactly when one (equivalently every) free-path-category lift belongs to the larger generated relation ideal.

theorem MagnitudeConjecture.BoundQuiver.relativeRelationHomIdeal_eq_span_killedPathMap {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) (hS : IsMonomial S) (x y : Q) : (relativeRelationHomIdeal hRS).homSubmodule (obj R y) (obj R x) = Submodule.span k (Set.range fun (p : { p : Quiver.Path x y // pathMap S p = 0 }) => pathMap R ↑p)

If the larger relation ideal is monomial, the relative kernel between the two relation quotients is spanned by the old-quotient images of the paths killed by the larger quotient.

theorem MagnitudeConjecture.BoundQuiver.relationQuotientFunctor_obj_bijective {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) : Function.Bijective (relationQuotientFunctor hRS).obj

Passing from one relation ideal to a larger one does not change the object set.

noncomputable def MagnitudeConjecture.BoundQuiver.relationQuotientAlgebraHom {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hR : IsAdmissible R) (hS : IsAdmissible S) (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) : CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯ →ₐ[k] CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯

The surjective finite-category-algebra map induced by inclusion of admissible bound-quiver relation ideals.

theorem MagnitudeConjecture.BoundQuiver.relationQuotientAlgebraHom_surjective {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hR : IsAdmissible R) (hS : IsAdmissible S) (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) : Function.Surjective ⇑(relationQuotientAlgebraHom hR hS hRS)

The algebra map attached to an inclusion of admissible relation ideals is surjective.

theorem MagnitudeConjecture.BoundQuiver.relationQuotientAlgebraHom_eq_zero_iff_coordinate {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hR : IsAdmissible R) (hS : IsAdmissible S) (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) (a : CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯) : (relationQuotientAlgebraHom hR hS hRS) a = 0 ↔ ∀ (i j : CoveringHom.finiteCategoryProjectiveGenerator.SmallIndex), (relationQuotientFunctor hRS).map (CoveringHom.finiteCategoryProjectiveGenerator.smallAlgebraCategoryCoordinate ⋯ a i j) = 0

Membership in the kernel of a relation-quotient category-algebra map is coordinatewise: every category-morphism matrix entry is killed by the underlying quotient functor.

theorem MagnitudeConjecture.BoundQuiver.relationQuotientAlgebraHom_eq_zero_iff_objectCoordinate {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R S : RelationFamily k Q} (hR : IsAdmissible R) (hS : IsAdmissible S) (hRS : ∀ (X Y : LinearPathCategory.Category k Q), QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k S X Y) (a : CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯) : (relationQuotientAlgebraHom hR hS hRS) a = 0 ↔ ∀ (X Y : Category R), (relationQuotientFunctor hRS).map (CoveringHom.finiteCategoryProjectiveGenerator.algebraCategoryCoordinate ⋯ a X Y) = 0

Object-indexed form of the coordinatewise kernel criterion for a relation-quotient category-algebra map.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullAlgebraHom {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {A : Type u} [Ring A] [Algebra k A] (P : SpecialBiserialPresentation k A Q) : have hR := ⋯; A →ₐ[k] CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯

The canonical quotient homomorphism from a special-biserial category algebra to its path-support-hull string category algebra.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullAlgebraHom_surjective {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {A : Type u} [Ring A] [Algebra k A] (P : SpecialBiserialPresentation k A Q) : Function.Surjective ⇑P.pathSupportHullAlgebraHom

The path-support-hull algebra homomorphism is surjective.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullAlgebraHom_eq_zero_iff_coordinate {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {A : Type u} [Ring A] [Algebra k A] (P : SpecialBiserialPresentation k A Q) (a : A) : P.pathSupportHullAlgebraHom a = 0 ↔ ∀ (i j : CoveringHom.finiteCategoryProjectiveGenerator.SmallIndex), (relationQuotientFunctor ⋯).map (CoveringHom.finiteCategoryProjectiveGenerator.smallAlgebraCategoryCoordinate ⋯ (P.algebraEquiv a) i j) = 0

The path-support-hull map kills an ambient algebra element exactly when the hull quotient kills every category-morphism coordinate of that element in the supplied bound-quiver presentation.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullAlgebraHom_eq_zero_iff_objectCoordinate {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {A : Type u} [Ring A] [Algebra k A] (P : SpecialBiserialPresentation k A Q) (a : A) : P.pathSupportHullAlgebraHom a = 0 ↔ ∀ (X Y : Category P.relations), (relationQuotientFunctor ⋯).map (CoveringHom.finiteCategoryProjectiveGenerator.algebraCategoryCoordinate ⋯ (P.algebraEquiv a) X Y) = 0

Object-indexed form of the coordinatewise kernel criterion for the path-support-hull map.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullQuotientAlgEquiv {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {A : Type u} [Ring A] [Algebra k A] (P : SpecialBiserialPresentation k A Q) : (TwoSidedIdeal.ker P.pathSupportHullAlgebraHom).ringCon.Quotient ≃ₐ[k] CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯

The quotient by the kernel of the path-support-hull map is canonically the resulting string category algebra.

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotient_admitsStringPresentation_of_ker_eq {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {A : Type u} [Ring A] [Algebra k A] (P : SpecialBiserialPresentation k A Q) (J : TwoSidedIdeal A) (hker : TwoSidedIdeal.ker P.pathSupportHullAlgebraHom = J) : AdmitsStringPresentation k J.ringCon.Quotient

Once a specified two-sided ideal has been identified as the kernel of the path-support-hull map, its literal quotient admits a string presentation. Thus the remaining structural content of socle reduction is exactly the kernel identification.