Multiplicative bases

MultiplicativeBasisDeformations.Independent.MeshComparison

The independent mesh category and the scalar mesh categories of Γ_A #

The path category of the independent quiver Γ_A is definitionally the linear path category of the proof library. Granted that the independent translate, defined by almost split sequences, is the translation of Γ_A in the proof library (TranslateCompatible), the independent mesh relations are the all-one mesh relations, so the independent k(Γ_A) is the scalar mesh category with all coefficients one. A gauge transformation (Lemma 4.4) then identifies it with the scalar mesh category whose coefficients come from the almost split sequences.

source
def MultiplicativeBasisDeformations.Statement.oneCoeff {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) :
MeshCoefficients k (toSkeleton S).arTranslationQuiver

The all-one coefficient system on Γ_A.

Instances For
    source
    def MultiplicativeBasisDeformations.Statement.TranslateCompatible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) :
    Prop

    The independent translate agrees with the translation of Γ_A in the proof library.

    Instances For
      source
      theorem MultiplicativeBasisDeformations.Statement.meshRelation_internal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) (t i : (toSkeleton S).ARVertex) :
      meshRelation S t i = ∑ j : (toSkeleton S).ARVertex, ∑ b : t ⟶ j, ∑ a : j ⟶ i, LinearPaths.path (b.toPath.comp a.toPath)

      The independent mesh relation in the vocabulary of the proof library (a definitional unfolding).

      source
      theorem MultiplicativeBasisDeformations.Statement.meshRelation_one {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) (x : ↑(toSkeleton S).arTranslationQuiver.nonprojective) :
      ∑ j : (toSkeleton S).ARVertex, ∑ b : ↑((toSkeleton S).arTranslationQuiver.tau x) ⟶ j, ∑ a : j ⟶ ↑x, LinearPaths.path (b.toPath.comp a.toPath) = MultiplicativeBasisDeformations.meshRelation (oneCoeff S) x

      The all-one mesh relation as a sum over all paths of length two.

      source
      theorem MultiplicativeBasisDeformations.Statement.meshRelation_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndecomposableFamily k A) (x : ↑(toSkeleton S).arTranslationQuiver.nonprojective) :
      meshRelation S ↑((toSkeleton S).arTranslationQuiver.tau x) ↑x = MultiplicativeBasisDeformations.meshRelation (oneCoeff S) x

      The independent mesh relation at a nonprojective vertex is the all-one mesh relation.

      source
      theorem MultiplicativeBasisDeformations.Statement.meshRelations_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : IndecomposableFamily k A} (hτ : TranslateCompatible S) (X Y : (toSkeleton S).ARVertex) :
      meshRelations S X Y = MultiplicativeBasisDeformations.meshRelations (oneCoeff S) (LinearPaths.obj X) (LinearPaths.obj Y)

      Under translate compatibility, the independent mesh relations are the all-one mesh relations.

      source
      theorem MultiplicativeBasisDeformations.Statement.meshIdeal_eq {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : IndecomposableFamily k A} (hτ : TranslateCompatible S) (X Y : (toSkeleton S).ARVertex) :
      meshIdeal S X Y = CategoricalIdeal.HomIdeal.generatedHomSubmodule k (MultiplicativeBasisDeformations.meshRelations (oneCoeff S)) (LinearPaths.obj X) (LinearPaths.obj Y)
      source
      theorem MultiplicativeBasisDeformations.Statement.meshRel_iff {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : IndecomposableFamily k A} (hτ : TranslateCompatible S) {X Y : PathCategory S} (f g : X ⟶ Y) :
      meshRel S f g ↔ (CategoricalIdeal.HomIdeal.linearSpan k (MultiplicativeBasisDeformations.meshRelations (oneCoeff S))).rel f g