Multiplicative bases

MultiplicativeBasisDeformations.Refinements.MeshNormalForm

Proposition 12.2: normal forms for filtered mesh categories #

deformation-refinements.tex (prop:characteristic-two-normal-form). Let C = kQ/(r_v) be a finite-dimensional graded category with homogeneous quadratic relations, and choose, in each degree q โ‰ฅ 3, homogeneous tuples p_i of degree d_i = q whose classes represent the cokernel of D_{q-1}. Every finite filtered E with gr E = C has a presentation E โ‰… kQ/(๐”ช^{N+1}, r_v โˆ’ ฮฃ_i ฮป_i (p_i)_v) inducing the identification on gr.

As for Proposition 5.4 (FilteredNormalForm.lean), we prove the proposition for E = ind(mod A) filtered by the radical powers, C = k(ฮ“_A) and the identification of Proposition 2.6(3). The hypothesis is in spanning form: the image of D_{q-1} and the classes of the retained tuples of degree q span all degree-q mesh families. The proof is the source's: correct the arrow lifts degree by degree, retaining a combination of the p_i in each degree (Lifts.exists_retained_correction); the filtration is finite. The resulting lifts realize kQ โ†’ ind(mod A) surjectively, with kernel exactly (๐”ช^{N+1}, r_v โˆ’ ฮฃ_i ฮป_i (p_i)_v) (normalForm), and agree with the identification on every radical layer.

Deviation in the injectivity step: the source compares associated gradings; we show directly, degree by degree, that a morphism realized to zero lies in the perturbed ideal, using the injectivity of Proposition 2.6(3) and the homogeneous parts of the mesh ideal.

The mesh relations as a presentation #

source
@[reducible, inline]
noncomputable abbrev MultiplicativeBasisDeformations.FlatPert.meshPres {k : Type u_1} [CommRing k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) โ†’ Fintype ((y : V) ร— (y โŸถ x))] (c : MeshCoefficients k Q) :
Pres k V

The mesh presentation: one quadratic relation r_x : ฯ„ x โ†’ x at each nonprojective vertex.

Instances For
    source
    theorem MultiplicativeBasisDeformations.FlatPert.ctxSpan_meshPres {k : Type u_1} [CommRing k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) โ†’ Fintype ((y : V) ร— (y โŸถ x))] [DecidableEq V] [(x y : V) โ†’ DecidableEq (x โŸถ y)] (c : MeshCoefficients k Q) (x y : V) :
    ctxSpan (meshPres c) (meshPres c).r x y = CategoricalIdeal.HomIdeal.generatedHomSubmodule k (meshRelations c) (LinearPaths.obj x) (LinearPaths.obj y)

    The mesh ideal is the span of the contextual mesh relations.

    source
    theorem MultiplicativeBasisDeformations.FlatPert.sub_proj_mem_geSpan {k : Type u_1} [CommRing k] {V : Type} [Quiver V] {n : โ„•} {x y : V} {h : Hm k x y} (hh : h โˆˆ geSpan k n x y) :
    h - (LinearPaths.proj n x y) h โˆˆ geSpan k (n + 1) x y

    The part of degree n of an element of ๐”ช^n agrees with it modulo ๐”ช^{n+1}.

    Retained tuples #

    source
    structure MultiplicativeBasisDeformations.IndSkeleton.Retained {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] (S : IndSkeleton k A) :
    Type (max 1 w)

    Retained tuples p_i = ((p_i)_v)_v, homogeneous of degree d_i โ‰ฅ 3.

    Instances For
      source
      def MultiplicativeBasisDeformations.IndSkeleton.Retained.Spans {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} (b : S.ArrowBases) (R : S.Retained) :
      Prop

      The cokernel hypothesis (spanning form): in each degree q = m + 1 โ‰ฅ 3, the image of D_m and the classes of the retained tuples of degree q span all mesh families of degree q.

      Instances For
        source
        noncomputable def MultiplicativeBasisDeformations.IndSkeleton.Lifts.errRet {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} {b : S.ArrowBases} (L : S.Lifts b) (R : S.Retained) (lam : R.I โ†’ k) (x : โ†‘S.arTranslationQuiver.nonprojective) :
        S.label โ†‘(S.arTranslationQuiver.tau x) โŸถ S.label โ†‘x

        The relation errors relative to the retained terms: r_v โˆ’ ฮฃ_i ฮป_i (p_i)_v, realized.

        Instances For
          source
          theorem MultiplicativeBasisDeformations.IndSkeleton.Lifts.pathMap_sub_pathMap {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} {b : S.ArrowBases} {m : โ„•} (hm : 1 โ‰ค m) (L L' : S.Lifts b) (hLL : โˆ€ {x y : S.ARVertex} (a : x โŸถ y), L'.L a - L.L a โˆˆ S.radPow m (S.label x) (S.label y)) {x y : S.ARVertex} (p : Quiver.Path x y) :
          L'.pathMap p - L.pathMap p โˆˆ S.radPow (p.length + m - 1) (S.label x) (S.label y)

          Two lift families differing in J^m on the arrows realize a path of length โ„“ up to J^{โ„“+m-1}.

          source
          theorem MultiplicativeBasisDeformations.IndSkeleton.Lifts.realize_sub_realize {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} {b : S.ArrowBases} {m d : โ„•} (hm : 1 โ‰ค m) (L L' : S.Lifts b) (hLL : โˆ€ {x y : S.ARVertex} (a : x โŸถ y), L'.L a - L.L a โˆˆ S.radPow m (S.label x) (S.label y)) {x y : S.ARVertex} {F : LinearPaths.obj x โŸถ LinearPaths.obj y} (hF : F โˆˆ LinearPaths.degreePart d x y) :
          (L'.realize x y) F - (L.realize x y) F โˆˆ S.radPow (d + m - 1) (S.label x) (S.label y)
          source
          theorem MultiplicativeBasisDeformations.IndSkeleton.Lifts.exists_retained_correction {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} (b : S.ArrowBases) (R : S.Retained) (hR : Retained.Spans b R) {m : โ„•} (hm : 2 โ‰ค m) (L : S.Lifts b) (lam : R.I โ†’ k) (hL : โˆ€ (x : โ†‘S.arTranslationQuiver.nonprojective), L.errRet R lam x โˆˆ S.radPow (m + 1) (S.label โ†‘(S.arTranslationQuiver.tau x)) (S.label โ†‘x)) :
          โˆƒ (L' : S.Lifts b) (lam' : R.I โ†’ k), โˆ€ (x : โ†‘S.arTranslationQuiver.nonprojective), L'.errRet R lam' x โˆˆ S.radPow (m + 2) (S.label โ†‘(S.arTranslationQuiver.tau x)) (S.label โ†‘x)

          The correction step of Proposition 12.2: if the relation errors relative to the retained terms lie in J^{m+1} (m โ‰ฅ 2), a change of the lifts in degree m and of the coefficients of the retained tuples of degree m + 1 moves them into J^{m+2}.

          source
          theorem MultiplicativeBasisDeformations.IndSkeleton.exists_lifts_errRet_mem {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} (b : S.ArrowBases) (R : S.Retained) (hR : Retained.Spans b R) (n : โ„•) :
          โˆƒ (L : S.Lifts b) (lam : R.I โ†’ k), โˆ€ (x : โ†‘S.arTranslationQuiver.nonprojective), L.errRet R lam x โˆˆ S.radPow (n + 3) (S.label โ†‘(S.arTranslationQuiver.tau x)) (S.label โ†‘x)

          Successive correction: lifts and retained coefficients with errors in J^{n+3}.

          source
          theorem MultiplicativeBasisDeformations.IndSkeleton.exists_lifts_errRet_eq_zero {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} (b : S.ArrowBases) (R : S.Retained) (hR : Retained.Spans b R) :
          โˆƒ (L : S.Lifts b) (lam : R.I โ†’ k), โˆ€ (x : โ†‘S.arTranslationQuiver.nonprojective), L.errRet R lam x = 0

          The process terminates: lifts satisfying r_v = ฮฃ_i ฮป_i (p_i)_v exactly.

          The presentation #

          source
          noncomputable def MultiplicativeBasisDeformations.IndSkeleton.Retained.pert {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} (b : S.ArrowBases) (R : S.Retained) (lam : R.I โ†’ k) (x : S.ARVertex) (t : (FlatPert.meshPres (S.arCoefficients b)).T x) :
          FlatPert.Hm k ((FlatPert.meshPres (S.arCoefficients b)).src x t) x

          The retained perturbation f_v = ฮฃ_i ฮป_i (p_i)_v of the mesh relations.

          Instances For
            source
            theorem MultiplicativeBasisDeformations.IndSkeleton.Retained.pert_mem {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} (b : S.ArrowBases) (R : S.Retained) (lam : R.I โ†’ k) (x : S.ARVertex) (t : (FlatPert.meshPres (S.arCoefficients b)).T x) :
            pert b R lam x t โˆˆ FlatPert.geSpan k ((FlatPert.meshPres (S.arCoefficients b)).deg x t + 1) ((FlatPert.meshPres (S.arCoefficients b)).src x t) x
            source
            theorem MultiplicativeBasisDeformations.IndSkeleton.Lifts.realize_geSpan {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} {b : S.ArrowBases} (L : S.Lifts b) {d : โ„•} {x y : S.ARVertex} {g : FlatPert.Hm k x y} (hg : g โˆˆ FlatPert.geSpan k d x y) :
            (L.realize x y) g โˆˆ S.radPow d (S.label x) (S.label y)
            source
            @[reducible, inline]
            noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.idealRet {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} {b : S.ArrowBases} (R : S.Retained) (lam : R.I โ†’ k) (N : โ„•) :
            FlatPert.IdealFam k S.ARVertex

            The ideal (๐”ช^{N+1}, r_v โˆ’ ฮฃ_i ฮป_i (p_i)_v).

            Instances For
              source
              theorem MultiplicativeBasisDeformations.IndSkeleton.Lifts.realize_eq_zero_of_memRet {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} {b : S.ArrowBases} (R : S.Retained) (lam : R.I โ†’ k) (N : โ„•) (L : S.Lifts b) (hL : โˆ€ (x : โ†‘S.arTranslationQuiver.nonprojective), L.errRet R lam x = 0) (hN : โˆ€ (X Y : S.Ind), S.radPow N X Y = โŠฅ) {x y : S.ARVertex} {G : FlatPert.Hm k x y} (hG : G โˆˆ (idealRet R lam N).I x y) :
              (L.realize x y) G = 0
              source
              theorem MultiplicativeBasisDeformations.IndSkeleton.hctx_le_ret {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} {b : S.ArrowBases} (R : S.Retained) (lam : R.I โ†’ k) (N n : โ„•) (x y : S.ARVertex) :
              FlatPert.hctx (FlatPert.meshPres (S.arCoefficients b)) n x y โ‰ค (idealRet R lam N).I x y โŠ” FlatPert.geSpan k (n + 1) x y

              Homogeneous contextual mesh relations lie in the perturbed ideal modulo ๐”ช^{n+1}.

              source
              theorem MultiplicativeBasisDeformations.IndSkeleton.Lifts.mem_of_realize_eq_zero {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} {b : S.ArrowBases} (R : S.Retained) (lam : R.I โ†’ k) (N : โ„•) (L : S.Lifts b) (hL : โˆ€ (x : โ†‘S.arTranslationQuiver.nonprojective), L.errRet R lam x = 0) (hN : โˆ€ (X Y : S.Ind), S.radPow N X Y = โŠฅ) {x y : S.ARVertex} {G : FlatPert.Hm k x y} (hG : (L.realize x y) G = 0) :
              G โˆˆ (idealRet R lam N).I x y

              Injectivity: a morphism of kQ realized to zero lies in the perturbed ideal.

              source
              theorem MultiplicativeBasisDeformations.IndSkeleton.normalForm {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aแตแต’แต–] {S : IndSkeleton k A} (b : S.ArrowBases) (R : S.Retained) (N : โ„•) (hR : Retained.Spans b R) (hN : โˆ€ (X Y : S.Ind), S.radPow N X Y = โŠฅ) :
              โˆƒ (lam : R.I โ†’ k) (L : S.Lifts b), (โˆ€ (x : โ†‘S.nonprojectiveVertices), L.error x = โˆ‘ i : R.I, lam i โ€ข (L.realize โ†‘(S.arTranslationQuiver.tau x) โ†‘x) (R.p i x)) โˆง (โˆ€ (x y : S.ARVertex) (G : FlatPert.Hm k x y), (L.realize x y) G = 0 โ†” G โˆˆ (idealRet R lam N).I x y) โˆง (โˆ€ (x y : S.ARVertex) (f : S.label x โŸถ S.label y), โˆƒ (G : LinearPaths.obj x โŸถ LinearPaths.obj y), (L.realize x y) G = f) โˆง โˆ€ (d : โ„•) (x y : S.ARVertex) {F : FlatPert.Hm k x y}, F โˆˆ LinearPaths.degreePart d x y โ†’ (L.realize x y) F - (S.realize b x y) F โˆˆ S.radPow (d + 1) (S.label x) (S.label y)

              Proposition 12.2 for E = ind(mod A) filtered by the radical powers, C = k(ฮ“_A) and the identification of Proposition 2.6(3): given retained tuples whose classes span the cokernels of the derivatives, there are coefficients ฮป and arrow lifts realizing kQ/(๐”ช^{N+1}, r_v โˆ’ ฮฃ_i ฮป_i (p_i)_v) โ‰… ind(mod A) โ€” the realization is surjective with exactly this kernel โ€” and inducing the prescribed identification on every radical layer.