Socle reduction of representation-finite special-biserial algebras

For a special-biserial bound-quiver presentation, the kernel of the canonical map to its path-support-hull string algebra is exactly the simultaneous socle ideal of the nonuniserial indecomposable projective-injective modules. The final theorem transports this equality across the literal presentation and primitive-projective presentation chosen by the caller.

def MagnitudeConjecture.RightModule.idealRightIdealSubmodule {A : Type u} [Ring A] (I : TwoSidedIdeal A) (e : A) : Submodule Aᵐᵒᵖ ↥(rightIdeal e)

The part of a two-sided ideal lying in a principal right ideal.

@[simp]

theorem MagnitudeConjecture.RightModule.mem_idealRightIdealSubmodule {A : Type u} [Ring A] (I : TwoSidedIdeal A) (e : A) (x : ↥(rightIdeal e)) : x ∈ idealRightIdealSubmodule I e ↔ ↑x ∈ I

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.largeAlgebraFiniteDimensional {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensional k (algebra hC)

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.largeAlgebraOppositeIsNoetherian {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : IsNoetherianRing (algebra hC)ᵐᵒᵖ

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalProjector_complete {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CompleteOrthogonalIdempotents (smallCanonicalProjector hC)

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalProjector_primitive {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (i : SmallIndex) : RightModule.PrimitiveIdempotentData (smallCanonicalProjector hC i)

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalRightIdealLinearEquiv {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (i : SmallIndex) : ↑(RightModule.rightIdealFGObj (smallCanonicalProjector hC i)) ≃ₗ[(algebra hC)ᵐᵒᵖ] ↑((representedFGFunctor hC).obj (MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.largeRepresentable✝ hC ((Fintype.equivFin C).symm i)))

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalRightIdealIso {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (i : SmallIndex) : RightModule.rightIdealFGObj (smallCanonicalProjector hC i) ≅ (representedFGFunctor hC).obj (MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.largeRepresentable✝ hC ((Fintype.equivFin C).symm i))

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalSourceLabel {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hC)) (i : SmallIndex) : S.ProjectiveLabel

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalRepresentableSourceIso {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hC)) (i : SmallIndex) : (representedFGFunctor hC).obj (MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.largeRepresentable✝ hC ((Fintype.equivFin C).symm i)) ≅ S.fgObj (smallCanonicalSourceLabel hC hlocal S i).label

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalSourceLabel_injective {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hC)) (hskel : CategoryTheory.Skeletal C) : Function.Injective (smallCanonicalSourceLabel hC hlocal S)

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalSourceLabel_surjective {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hC)) : Function.Surjective (smallCanonicalSourceLabel hC hlocal S)

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalSourceEquiv {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hC)) (hskel : CategoryTheory.Skeletal C) : SmallIndex ≃ S.ProjectiveLabel

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallPrimitiveProjectivePresentation {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hC)) (hskel : CategoryTheory.Skeletal C) : S.PrimitiveProjectivePresentation

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraCategoryCoordinate_rightIdeal_eq_zero {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) {X Y Z : C} (q : ↥(RightModule.rightIdeal (smallCanonicalProjector hC ((Fintype.equivFin C) Z)))) (hYZ : Y ≠ Z) : algebraCategoryCoordinate hC (↑q) X Y = 0

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.exists_algebraCategoryCoordinate_ne_zero_of_rightIdeal {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) {Z : C} (q : ↥(RightModule.rightIdeal (smallCanonicalProjector hC ((Fintype.equivFin C) Z)))) (hq : q ≠ 0) : ∃ (X : C), algebraCategoryCoordinate hC (↑q) X Z ≠ 0

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraCategoryCoordinate_smul {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (c : k) (a : algebra hC) (X Y : C) : algebraCategoryCoordinate hC (c • a) X Y = c • algebraCategoryCoordinate hC a X Y

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.exists_surviving_hullKilledPath_of_relative_ne_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (f : obj P.relations z ⟶ obj P.relations x) (hf : f ∈ (relativeRelationHomIdeal ⋯).hom (obj P.relations z) (obj P.relations x)) (hfne : f ≠ 0) : ∃ (s : Quiver.Path x z), pathMap P.relations s ≠ 0 ∧ pathMap (pathSupportHull P.relations) s = 0

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.exists_relationSurvivingSupport_of_surviving_hullKilledPath {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) {x z : Q} (s : Quiver.Path x z) (hsSurvives : pathMap P.relations s ≠ 0) (hsHull : pathMap (pathSupportHull P.relations) s = 0) : ∃ r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x), Nonempty (P.RelationSurvivingSupport r)

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebraFiniteDimensional {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) : FiniteDimensional k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebraOppositeIsNoetherian {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) : IsNoetherianRing (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)ᵐᵒᵖ

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

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernelRow {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (z : Q) : Submodule (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)ᵐᵒᵖ ↥(RightModule.rightIdeal (CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalProjector ⋯ ((Fintype.equivFin (Category P.relations)) (obj P.relations z))))

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernelRow_coordinate_mem {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (z : Q) (q : ↥(P.relativeHullKernelRow z)) (X Y : Category P.relations) : CoveringHom.finiteCategoryProjectiveGenerator.algebraCategoryCoordinate ⋯ (↑↑q) X Y ∈ (relativeRelationHomIdeal ⋯).hom Y X

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.exists_relationSurvivingSupport_of_relativeHullKernelRow_ne_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (z : Q) (q : ↥(P.relativeHullKernelRow z)) (hq : q ≠ 0) : ∃ (x : Q) (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (_ : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)), Nonempty (P.RelationSurvivingSupport r)

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernelRow_eq_smul_of_ne_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (z : Q) (q₀ : ↥(P.relativeHullKernelRow z)) (hq₀ : q₀ ≠ 0) (q : ↥(P.relativeHullKernelRow z)) : ∃ (c : k), q = c • q₀

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernelRow_isSimple_of_ne_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (z : Q) (q₀ : ↥(P.relativeHullKernelRow z)) (hq₀ : q₀ ≠ 0) : IsSimpleModule (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)ᵐᵒᵖ ↥(P.relativeHullKernelRow z)

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernelRow_le_moduleSocle_of_ne_bot {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (z : Q) (hrow : P.relativeHullKernelRow z ≠ ⊥) : P.relativeHullKernelRow z ≤ moduleSocle (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)ᵐᵒᵖ ↥(RightModule.rightIdeal (CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalProjector ⋯ ((Fintype.equivFin (Category P.relations)) (obj P.relations z))))

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientVertexProjectiveLabel {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) (z : Q) : S.ProjectiveLabel

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryPrimitiveProjectivePresentation {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) : S.PrimitiveProjectivePresentation

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryPrimitiveProjectivePresentation_idempotent_vertex {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) (z : Q) : (P.quotientCategoryPrimitiveProjectivePresentation S).idempotent (P.quotientVertexProjectiveLabel S z) = CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalProjector ⋯ ((Fintype.equivFin (Category P.relations)) (obj P.relations z))

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientVertexProjectiveIso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) (z : Q) : (CoveringHom.finiteCategoryProjectiveGenerator.representedFGFunctor ⋯).obj ((CoveringHom.finiteDimensionalLinearCoyonedaFunctor ⋯).obj (Opposite.op (obj P.relations z))) ≅ S.fgObj (P.quotientVertexProjectiveLabel S z).label

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientVertexProjectiveLabel_mem_nonuniserialProjectiveInjectiveLabels {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] [IsAlgClosed k] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) {x z : Q} (r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x) (hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x)) (p : P.RelationSurvivingSupport r) : P.quotientVertexProjectiveLabel S z ∈ S.nonuniserialProjectiveInjectiveLabels

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernelRow_val_mem_socleFamily_of_ne_bot {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] [IsAlgClosed k] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) (z : Q) (hrow : P.relativeHullKernelRow z ≠ ⊥) (q : ↥(P.relativeHullKernelRow z)) : ↑↑q ∈ (P.quotientCategoryPrimitiveProjectivePresentation S).primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernel_le_socleFamily {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] [IsAlgClosed k] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) : TwoSidedIdeal.ker P.relativeHullAlgebraHom ≤ (P.quotientCategoryPrimitiveProjectivePresentation S).primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯

theorem MagnitudeConjecture.BoundQuiver.projectiveInjectiveIndecomposable_isUniserial_of_admitsStringPresentation {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (hString : AdmitsStringPresentation k B) (M : RightModule.FinitelyGeneratedCategory B) [CategoryTheory.Projective M] [CategoryTheory.Injective M] (hM : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Bᵐᵒᵖ ↑M) : IsUniserialModule Bᵐᵒᵖ ↑M

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.finalQuotientCategoryAlgebraFiniteDimensional {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) : FiniteDimensional k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.finalQuotientCategoryAlgebraOppositeIsNoetherian {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) : IsNoetherianRing (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)ᵐᵒᵖ

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientVertexProjectiveLabel_surjective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) : Function.Surjective (P.quotientVertexProjectiveLabel S)

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullQuotient_admitsStringPresentation {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q) : AdmitsStringPresentation k (RightModule.idealQuotientAlgebra (TwoSidedIdeal.ker P.relativeHullAlgebraHom))

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernelRow_ne_bot_of_vertexProjectiveLabel_mem {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] [IsAlgClosed k] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) (z : Q) (hz : P.quotientVertexProjectiveLabel S z ∈ S.nonuniserialProjectiveInjectiveLabels) : P.relativeHullKernelRow z ≠ ⊥

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.vertexSocleIdeal_le_relativeHullKernel {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] [IsAlgClosed k] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) (z : Q) (hz : P.quotientVertexProjectiveLabel S z ∈ S.nonuniserialProjectiveInjectiveLabels) : (P.quotientCategoryPrimitiveProjectivePresentation S).primitiveProjectiveSocleIdeal (P.quotientVertexProjectiveLabel S z) ⋯ ≤ TwoSidedIdeal.ker P.relativeHullAlgebraHom

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.socleFamily_le_relativeHullKernel {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] [IsAlgClosed k] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) : (P.quotientCategoryPrimitiveProjectivePresentation S).primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯ ≤ TwoSidedIdeal.ker P.relativeHullAlgebraHom

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relativeHullKernel_eq_socleFamily {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] [IsAlgClosed k] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) : TwoSidedIdeal.ker P.relativeHullAlgebraHom = (P.quotientCategoryPrimitiveProjectivePresentation S).primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯

theorem MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategorySocleFamily_admitsStringPresentation {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] [IsAlgClosed k] (P : SpecialBiserialPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k (MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.quotientCategoryAlgebra✝ P)) : AdmitsStringPresentation k (RightModule.idealQuotientAlgebra ((P.quotientCategoryPrimitiveProjectivePresentation S).primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯))

theorem MagnitudeConjecture.specialBiserial_socleFamilyQuotient_admitsStringPresentation {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : RightModule.FiniteIndecomposableSkeleton k A) (P : S.PrimitiveProjectivePresentation) (hSpecial : BoundQuiver.IsSpecialBiserial k A) : BoundQuiver.AdmitsStringPresentation k (RightModule.idealQuotientAlgebra (P.primitiveProjectiveSocleFamilyIdeal S.nonuniserialProjectiveInjectiveLabels ⋯))