Multiplicative bases

MultiplicativeBasisDeformations.Foundations.ProjectiveEvaluation

Evaluation at the projective labels: full faithfulness (Lemma 2.9) #

Construction 2.8 (con:projective-algebra): A₀ = ⊕_{x,y} D(P_y, P_x), the category algebra of the projective labels, and evaluation sends X to the module with components C(P_x, X). Lemma 2.9 (first part, graded-category.tex): under the vanishings for modules killed by e, "P ↦ Pe is fully faithful on proj Λ". The manuscript proves this with the multiplication map (Me) ⊗_{Λ_e} eΛ → M, whose kernel and cokernel are killed by e, and the vanishings. We use the same two steps without the tensor product: a map g on the e-parts is defined on the submodule generated by the e-part by ∑ λ_i m_i ↦ ∑ λ_i g(m_i), well defined because the discrepancy generates a submodule killed by e (Hom-vanishing), and it extends to the whole module because the quotient is killed by e (Ext¹-vanishing).

add C is represented by finite families of labels; maps between families are matrices of morphisms.

source
@[reducible, inline]
abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.PV {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) :
Type

The projective labels.

Instances For
    source
    @[reducible, inline]
    abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.F0 {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) :
    D.PV → 𝒞

    The projective labels as a family of objects.

    Instances For
      source
      def MultiplicativeBasisDeformations.CatAlg.MeshData.extZ {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (X : 𝒞) :
      Rep D.F0 X →ₗ[k] Rep F X

      Extension by zero from the projective labels.

      Instances For
        source
        def MultiplicativeBasisDeformations.CatAlg.MeshData.restr {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (X : 𝒞) :
        Rep F X →ₗ[k] Rep D.F0 X

        Restriction to the projective labels.

        Instances For
          source
          @[simp]
          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extZ_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {X : 𝒞} (m : Rep D.F0 X) (y : ι) :
          (D.extZ X) m y = if h : D.proj y then m ⟨y, h⟩ else 0
          source
          @[simp]
          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.restr_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {X : 𝒞} (m : Rep F X) (p : D.PV) :
          (D.restr X) m p = m ↑p
          source
          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.sum_proj {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {T : Type u_1} [AddCommMonoid T] (G : ι → T) (hG : ∀ (z : ι), ¬D.proj z → G z = 0) :
          ∑ z : ι, G z = ∑ q : D.PV, G ↑q
          source
          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.restr_extZ {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (X : 𝒞) (m : Rep D.F0 X) :
          (D.restr X) ((D.extZ X) m) = m
          source
          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extZ_injective {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (X : 𝒞) :
          Function.Injective ⇑(D.extZ X)
          source
          def MultiplicativeBasisDeformations.CatAlg.MeshData.resAlg {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (μ : Alg F) :
          Alg D.F0

          The P × P block of an element of Λ.

          Instances For
            source
            theorem MultiplicativeBasisDeformations.CatAlg.MeshData.resAlg_add {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (μ ν : Alg F) :
            D.resAlg (μ + ν) = D.resAlg μ + D.resAlg ν
            source
            theorem MultiplicativeBasisDeformations.CatAlg.MeshData.resAlg_mul_of_rows {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (μ ν : Alg F) (hμ : ∀ (y z : ι), ¬D.proj z → μ y z = 0) :
            D.resAlg (μ * ν) = D.resAlg μ * D.resAlg ν
            source
            theorem MultiplicativeBasisDeformations.CatAlg.MeshData.smul_extZ {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {X : 𝒞} (μ : Alg F) (hμ : ∀ (y z : ι), ¬D.proj y → μ y z = 0) (m : Rep D.F0 X) :
            μ • (D.extZ X) m = (D.extZ X) (D.resAlg μ • m)

            Elements with rows in P act on the e-part through their P × P block.

            source
            theorem MultiplicativeBasisDeformations.CatAlg.MeshData.idem_mul_rows {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) (p : D.PV) (a : Alg F) (y z : ι) :
            ¬D.proj y → (idem ↑p * a) y z = 0
            source
            theorem MultiplicativeBasisDeformations.CatAlg.MeshData.idem_smul_eq_extZ {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {X : 𝒞} (p : D.PV) (m : Rep F X) :
            idem ↑p • m = (D.extZ X) ((D.restr X) (idem ↑p • m))

            e_p m lies in the image of extension by zero.

            Finite families #

            source
            @[reducible, inline]
            abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.RZ {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] {ι : Type} (F : ι → 𝒞) {κ : Type} (Z : κ → ι) :
            Type w

            R_Z = ⊕_j R_{Z j} for a family of labels.

            Instances For
              source
              @[reducible, inline]
              abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.EZ {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ : Type} (Z : κ → ι) :
              Type w

              The evaluation ⊕_j C(P_-, Z j) of a family.

              Instances For
                source
                @[reducible, inline]
                abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.Mat {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] {ι : Type} (F : ι → 𝒞) {κ κ' : Type} (Z : κ → ι) (Z' : κ' → ι) :
                Type w

                Matrices of morphisms between families.

                Instances For
                  source
                  def MultiplicativeBasisDeformations.CatAlg.MeshData.bigMap {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {κ κ' : Type} [Fintype κ] {Z : κ → ι} {Z' : κ' → ι} (f : Mat F Z Z') :
                  RZ F Z →ₗ[Alg F] RZ F Z'

                  The Λ-linear map of a matrix.

                  Instances For
                    source
                    def MultiplicativeBasisDeformations.CatAlg.MeshData.evMap {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ κ' : Type} [Fintype κ] {Z : κ → ι} {Z' : κ' → ι} (f : Mat F Z Z') :
                    D.EZ Z →ₗ[Alg D.F0] D.EZ Z'

                    The A₀-linear map of a matrix: evaluation.

                    Instances For
                      source
                      theorem MultiplicativeBasisDeformations.CatAlg.MeshData.bigMap_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] {Z : κ → ι} {Z' : κ' → ι} (f : Mat F Z Z') (m : RZ F Z) (j' : κ') :
                      (bigMap f) m j' = ∑ j : κ, (repMap (f j j')) (m j)
                      source
                      theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evMap_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] {Z : κ → ι} {Z' : κ' → ι} (f : Mat F Z Z') (m : D.EZ Z) (j' : κ') :
                      (D.evMap f) m j' = ∑ j : κ, (repMap (f j j')) (m j)
                      source
                      def MultiplicativeBasisDeformations.CatAlg.MeshData.extZs {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ : Type} (Z : κ → ι) :
                      D.EZ Z →ₗ[k] RZ F Z

                      Extension by zero, componentwise.

                      Instances For
                        source
                        theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extZs_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ : Type} [Fintype κ] [DecidableEq κ] (Z : κ → ι) (m : D.EZ Z) (j : κ) :
                        (D.extZs Z) m j = (D.extZ (F (Z j))) (m j)
                        source
                        theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extZs_injective {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ : Type} [Fintype κ] [DecidableEq κ] (Z : κ → ι) :
                        Function.Injective ⇑(D.extZs Z)
                        source
                        theorem MultiplicativeBasisDeformations.CatAlg.MeshData.repMap_extZ {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {X Y : 𝒞} (f : X ⟶ Y) (m : Rep D.F0 X) :
                        (repMap f) ((D.extZ X) m) = (D.extZ Y) ((repMap f) m)
                        source
                        theorem MultiplicativeBasisDeformations.CatAlg.MeshData.bigMap_extZs {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] {Z : κ → ι} {Z' : κ' → ι} (f : Mat F Z Z') (m : D.EZ Z) :
                        (bigMap f) ((D.extZs Z) m) = (D.extZs Z') ((D.evMap f) m)
                        source
                        def MultiplicativeBasisDeformations.CatAlg.MeshData.yonMat {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {κ κ' : Type} [DecidableEq κ] {Z : κ → ι} {Z' : κ' → ι} (Φ : RZ F Z →ₗ[Alg F] RZ F Z') :
                        Mat F Z Z'

                        The matrix of a Λ-linear map between families (Yoneda).

                        Instances For
                          source
                          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.eq_bigMap {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] {Z : κ → ι} {Z' : κ' → ι} (Φ : RZ F Z →ₗ[Alg F] RZ F Z') :
                          Φ = bigMap (yonMat Φ)
                          source
                          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.bigMap_injective {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] {Z : κ → ι} {Z' : κ' → ι} {f g : Mat F Z Z'} (h : bigMap f = bigMap g) :
                          f = g
                          source
                          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.bigMap_zero {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] {Z : κ → ι} {Z' : κ' → ι} :
                          bigMap 0 = 0
                          source
                          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.killedSub_span {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ : Type} [Fintype κ] [DecidableEq κ] (Z : κ → ι) :
                          D.KilledSub (Submodule.span (Alg F) (Set.range ⇑(D.extZs Z)))

                          The e-part of a family generates a submodule whose quotient is killed by e.

                          source
                          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.smul_extZs {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ : Type} [Fintype κ] [DecidableEq κ] {Z : κ → ι} (μ : Alg F) (hμ : ∀ (y z : ι), ¬D.proj y → μ y z = 0) (m : D.EZ Z) :
                          μ • (D.extZs Z) m = (D.extZs Z) (D.resAlg μ • m)
                          source
                          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evMap_injective {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Z : κ → ι} {Z' : κ' → ι} {f : Mat F Z Z'} (h : D.evMap f = 0) :
                          f = 0

                          Evaluation is faithful on add C (Lemma 2.9).

                          source
                          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evMap_surjective {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {L : LocalFamily F} (D : MeshData F L) {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Z : κ → ι} {Z' : κ' → ι} (g : D.EZ Z →ₗ[Alg D.F0] D.EZ Z') :
                          ∃ (f : Mat F Z Z'), D.evMap f = g

                          Evaluation is full on add C (Lemma 2.9).