Multiplicative bases

MultiplicativeBasisDeformations.Foundations.ReductionMesh

Reduction of path categories and mesh relations along a ring map #

For a ring map red : š’Ŗ ā†’ k, reduction of coefficients on the linear path categories (redP): it preserves composition, paths and degrees, sends the mesh relations of coefficients Å© to those of c when red āˆ˜ Å© = c, maps the mesh ideal into the mesh ideal, and (for surjective red) every element of the mesh ideal over k lifts to one over š’Ŗ. This is the right exactness used in Lemma B.2 (characteristic-two-mesh-calculations.tex: "Right exactness of tensor product gives coker D_m(Eā‚„) āŠ— š”½ā‚‚ ā‰… coker D_m(Cā½Ā²ā¾)").

source
noncomputable def MultiplicativeBasisDeformations.LinearPaths.redP {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {x y : V} :
(obj x āŸ¶ obj y) ā†’+ (obj x āŸ¶ obj y)

Reduction of coefficients of a path combination.

Instances For
    source
    theorem MultiplicativeBasisDeformations.LinearPaths.redP_apply {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {x y : V} (f : obj x āŸ¶ obj y) :
    (redP red) f = ofFinsupp (Finsupp.mapRange ā‡‘red ā‹Æ (toFinsupp f))
    source
    theorem MultiplicativeBasisDeformations.LinearPaths.redP_smul {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {x y : V} (a : O) (f : obj x āŸ¶ obj y) :
    (redP red) (a ā€¢ f) = red a ā€¢ (redP red) f
    source
    theorem MultiplicativeBasisDeformations.LinearPaths.redP_path {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {x y : V} (p : Quiver.Path x y) :
    (redP red) (path p) = path p
    source
    theorem MultiplicativeBasisDeformations.LinearPaths.redP_smul_path {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {x y : V} (a : O) (p : Quiver.Path x y) :
    (redP red) (a ā€¢ path p) = red a ā€¢ path p
    source
    theorem MultiplicativeBasisDeformations.LinearPaths.redP_comp {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {x y z : V} (f : obj x āŸ¶ obj y) (g : obj y āŸ¶ obj z) :
    (redP red) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((redP red) f) ((redP red) g)
    source
    theorem MultiplicativeBasisDeformations.LinearPaths.redP_degreePart {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {x y : V} {n : ā„•} {f : obj x āŸ¶ obj y} (hf : f āˆˆ degreePart n x y) :
    (redP red) f āˆˆ degreePart n x y
    source
    theorem MultiplicativeBasisDeformations.LinearPaths.exists_lift {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] (hred : Function.Surjective ā‡‘red) {x y : V} {n : ā„•} {g : obj x āŸ¶ obj y} (hg : g āˆˆ degreePart n x y) :
    āˆƒ f āˆˆ degreePart n x y, (redP red) f = g

    Lifting path combinations, within a degree.

    source
    theorem MultiplicativeBasisDeformations.LinearPaths.exists_lift' {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] (hred : Function.Surjective ā‡‘red) {x y : V} (g : obj x āŸ¶ obj y) :
    āˆƒ (f : obj x āŸ¶ obj y), (redP red) f = g

    Every path combination lifts.

    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redP_meshRelation {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) (x : ā†‘Q.nonprojective) :
    (LinearPaths.redP red) (meshRelation u x) = meshRelation c x
    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redP_mem_ideal {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} {f : LinearPaths.obj X āŸ¶ LinearPaths.obj Y} (hf : f āˆˆ (RelSystem.mesh u).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) :
    (LinearPaths.redP red) f āˆˆ (RelSystem.mesh c).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

    The mesh ideal reduces into the mesh ideal.

    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_lift_ideal {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) (hs : Function.Surjective ā‡‘red) {X Y : V} {g : LinearPaths.obj X āŸ¶ LinearPaths.obj Y} (hg : g āˆˆ (RelSystem.mesh c).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) :
    āˆƒ f āˆˆ (RelSystem.mesh u).ideal (LinearPaths.obj X) (LinearPaths.obj Y), (LinearPaths.redP red) f = g

    The mesh ideal lifts.

    Reduction on the scalar mesh categories #

    source
    theorem MultiplicativeBasisDeformations.ScalarMeshCategory.functor_redP_eq {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} {Ī¦ Ī¦' : LinearPaths.obj X āŸ¶ LinearPaths.obj Y} (h : (RelationCategory.functor O (meshRelations u)).map Ī¦ = (RelationCategory.functor O (meshRelations u)).map Ī¦') :
    (RelationCategory.functor k (meshRelations c)).map ((LinearPaths.redP red) Ī¦) = (RelationCategory.functor k (meshRelations c)).map ((LinearPaths.redP red) Ī¦')
    source
    noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.redE {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] (u : MeshCoefficients O Q) (c : MeshCoefficients k Q) {X Y : V} (Ļ† : obj u X āŸ¶ obj u Y) :
    obj c X āŸ¶ obj c Y

    Reduction of morphisms of the scalar mesh category.

    Instances For
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_map {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} (Ī¦ : LinearPaths.obj X āŸ¶ LinearPaths.obj Y) :
      redE red u c ((RelationCategory.functor O (meshRelations u)).map Ī¦) = (RelationCategory.functor k (meshRelations c)).map ((LinearPaths.redP red) Ī¦)
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_add {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} (Ļ† Ļˆ : obj u X āŸ¶ obj u Y) :
      redE red u c (Ļ† + Ļˆ) = redE red u c Ļ† + redE red u c Ļˆ
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_zero {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} :
      redE red u c 0 = 0
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_sub {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} (Ļ† Ļˆ : obj u X āŸ¶ obj u Y) :
      redE red u c (Ļ† - Ļˆ) = redE red u c Ļ† - redE red u c Ļˆ
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_smul {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} (a : O) (Ļ† : obj u X āŸ¶ obj u Y) :
      redE red u c (a ā€¢ Ļ†) = red a ā€¢ redE red u c Ļ†
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_sum {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} {Ī¹ : Type u_1} (s : Finset Ī¹) (Ļ† : Ī¹ ā†’ (obj u X āŸ¶ obj u Y)) :
      redE red u c (āˆ‘ i āˆˆ s, Ļ† i) = āˆ‘ i āˆˆ s, redE red u c (Ļ† i)
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_comp {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y Z : V} (Ļ† : obj u X āŸ¶ obj u Y) (Ļˆ : obj u Y āŸ¶ obj u Z) :
      redE red u c (CategoryTheory.CategoryStruct.comp Ļ† Ļˆ) = CategoryTheory.CategoryStruct.comp (redE red u c Ļ†) (redE red u c Ļˆ)
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_pathMor {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} (p : Quiver.Path X Y) :
      redE red u c (pathMor u p) = pathMor c p
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_arrowMor {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} (a : X āŸ¶ Y) :
      redE red u c (arrowMor u a) = arrowMor c a
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redE_degreePart {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {X Y : V} {n : ā„•} {Ļ† : obj u X āŸ¶ obj u Y} (hĻ† : Ļ† āˆˆ degreePart u n X Y) :
      redE red u c Ļ† āˆˆ degreePart c n X Y
      source
      theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_lift_degreePart {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) (hs : Function.Surjective ā‡‘red) {X Y : V} {n : ā„•} {Ļˆ : obj c X āŸ¶ obj c Y} (hĻˆ : Ļˆ āˆˆ degreePart c n X Y) :
      āˆƒ Ļ† āˆˆ degreePart u n X Y, redE red u c Ļ† = Ļˆ

      Families #

      source
      noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.redA {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] (u : MeshCoefficients O Q) (c : MeshCoefficients k Q) (f : ArrowFamily u) :
      ArrowFamily c

      Reduction of arrow families.

      Instances For
        source
        noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.redF {O : Type u} {k : Type u'} [CommRing O] [CommRing k] (red : O ā†’+* k) {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] (u : MeshCoefficients O Q) (c : MeshCoefficients k Q) (g : MeshFamily u) :
        MeshFamily c

        Reduction of mesh families.

        Instances For
          source
          theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redF_meshDerivative {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) (f : ArrowFamily u) :
          redF red u c (meshDerivative u f) = meshDerivative c (redA red u c f)
          source
          theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redF_add {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (g g' : MeshFamily u) (hred' : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) :
          redF red u c (g + g') = redF red u c g + redF red u c g'
          source
          theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redF_smul {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) (a : O) (g : MeshFamily u) :
          redF red u c (a ā€¢ g) = red a ā€¢ redF red u c g
          source
          theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redF_sub {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) (g g' : MeshFamily u) :
          redF red u c (g - g') = redF red u c g - redF red u c g'
          source
          theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redF_sum {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) {Ī¹ : Type u_1} (s : Finset Ī¹) (g : Ī¹ ā†’ MeshFamily u) :
          redF red u c (āˆ‘ i āˆˆ s, g i) = āˆ‘ i āˆˆ s, redF red u c (g i)
          source
          theorem MultiplicativeBasisDeformations.ScalarMeshCategory.redF_row {O : Type u} {k : Type u'} [CommRing O] [CommRing k] {red : O ā†’+* k} {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) ā†’ Fintype ((y : V) Ɨ (y āŸ¶ x))] {u : MeshCoefficients O Q} {c : MeshCoefficients k Q} (hred : āˆ€ (x : ā†‘Q.nonprojective) (y : V) (a : y āŸ¶ ā†‘x), red ā†‘(u x y a) = ā†‘(c x y a)) [DecidableEq V] (x : ā†‘Q.nonprojective) (w : Quiver.Path ā†‘(Q.tau x) ā†‘x) :
          redF red u c (row u x w) = row c x w