Multiplicative bases

MultiplicativeBasisDeformations.Foundations.EvaluationEquivalence

Proposition 2.10(1): evaluation is an equivalence add C ≃ mod A₀ #

prop:projective-evaluation(1) (graded-category.tex): "Evaluation induces an equivalence add C ≃ mod A₀."

add C is the category of finite families of labels with matrices of morphisms (AddC), and mod A₀ the full subcategory of finitely generated modules over the category algebra of the projective labels (ModFG). Evaluation is a functor (evFunctor); it is faithful (evMap_injective), full (evMap_surjective) and essentially surjective (InjData.essSurj), hence an equivalence (evFunctor_isEquivalence).

source
structure MultiplicativeBasisDeformations.CatAlg.AddC {𝒞 : Type v} {ι : Type} (F : ι → 𝒞) :
Type

add C: finite families of labels, with matrices of morphisms.

  • n : ℕ
  • Z : Fin self.n → ι
Instances For
    source
    def MultiplicativeBasisDeformations.CatAlg.AddC.idMat {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} {F : ι → 𝒞} (X : AddC F) (j j' : Fin X.n) :
    F (X.Z j) ⟶ F (X.Z j')

    The identity matrix.

    Instances For
      source
      @[instance_reducible]
      instance MultiplicativeBasisDeformations.CatAlg.AddC.instCategory {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} {F : ι → 𝒞} :
      CategoryTheory.Category.{w, 0} (AddC F)
      source
      theorem MultiplicativeBasisDeformations.CatAlg.AddC.comp_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {X Y Z : AddC F} (f : X ⟶ Y) (g : Y ⟶ Z) (j : Fin X.n) (j'' : Fin Z.n) :
      CategoryTheory.CategoryStruct.comp f g j j'' = ∑ j' : Fin Y.n, CategoryTheory.CategoryStruct.comp (f j j') (g j' j'')
      source
      theorem MultiplicativeBasisDeformations.CatAlg.AddC.id_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (X : AddC F) (j j' : Fin X.n) :
      CategoryTheory.CategoryStruct.id X j j' = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
      source
      @[reducible, inline]
      abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.ModFG {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 (w + 1)

      mod A₀: finitely generated modules over the category algebra of the projective labels.

      Instances For
        source
        theorem MultiplicativeBasisDeformations.CatAlg.MeshData.repMap_id' {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) :
        (repMap (CategoryTheory.CategoryStruct.id X)) m = m
        source
        theorem MultiplicativeBasisDeformations.CatAlg.MeshData.repMap_neg' {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 : 𝒞} (g : X ⟶ Y) :
        repMap (-g) = -repMap g
        source
        theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evMap_sub {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 g : Mat F Z Z') :
        D.evMap (f - g) = D.evMap f - D.evMap g
        source
        def MultiplicativeBasisDeformations.CatAlg.MeshData.evFunctor0 {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) :
        CategoryTheory.Functor (AddC F) (ModuleCat (Alg D.F0))

        Evaluation add C → Mod A₀.

        Instances For
          source
          instance MultiplicativeBasisDeformations.CatAlg.MeshData.instFaithfulAddCModuleCatAlgPVF0EvFunctor0 {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] :
          D.evFunctor0.Faithful
          source
          instance MultiplicativeBasisDeformations.CatAlg.MeshData.instFullAddCModuleCatAlgPVF0EvFunctor0 {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] :
          D.evFunctor0.Full
          source
          theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evZ_finite {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (X : AddC F) :
          Module.Finite (Alg D.F0) (D.EZ X.Z)
          source
          @[reducible, inline]
          abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.evFunctor {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] :
          CategoryTheory.Functor (AddC F) D.ModFG

          Evaluation add C → mod A₀.

          Instances For
            source
            instance MultiplicativeBasisDeformations.CatAlg.MeshData.instFaithfulAddCModFGEvFunctor {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] :
            D.evFunctor.Faithful
            source
            instance MultiplicativeBasisDeformations.CatAlg.MeshData.instFullAddCModFGEvFunctor {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] :
            D.evFunctor.Full
            source
            theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evFunctor_essSurj {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (J : D.InjData) :
            D.evFunctor.EssSurj
            source
            theorem MultiplicativeBasisDeformations.CatAlg.MeshData.evFunctor_isEquivalence {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (J : D.InjData) :
            D.evFunctor.IsEquivalence

            Proposition 2.10(1) (prop:projective-evaluation(1)): evaluation is an equivalence add C ≃ mod A₀.

            Transport along a ring isomorphism #

            source
            @[reducible, inline]
            abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.FGProp (R' : Type w) [Ring R'] :
            CategoryTheory.ObjectProperty (ModuleCat R')

            Finitely generated modules over a ring.

            Instances For
              source
              instance MultiplicativeBasisDeformations.CatAlg.MeshData.instIsClosedUnderIsomorphismsModuleCatFGProp {R' : Type w} [Ring R'] :
              (FGProp R').IsClosedUnderIsomorphisms
              source
              theorem MultiplicativeBasisDeformations.CatAlg.MeshData.finite_compHom_iff {R' : Type w} [Ring R'] {A : Type u_1} [Ring A] (r : R' ≃+* A) (X : Type u_2) [AddCommGroup X] [Module A X] :
              Module.Finite R' X ↔ Module.Finite A X
              source
              theorem MultiplicativeBasisDeformations.CatAlg.MeshData.fg_restrictScalars_iff {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {R' : Type w} [Ring R'] (r : R' ≃+* Alg D.F0) (X : ModuleCat (Alg D.F0)) :
              Module.Finite R' ↑((ModuleCat.restrictScalars r.toRingHom).obj X) ↔ Module.Finite (Alg D.F0) ↑X
              source
              noncomputable def MultiplicativeBasisDeformations.CatAlg.MeshData.evEquivOfRingEquiv {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) [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {R' : Type w} [Ring R'] (J : D.InjData) (r : R' ≃+* Alg D.F0) :
              AddC F ≌ (FGProp R').FullSubcategory

              add C ≃ mod R' for any ring R' isomorphic to the category algebra of the projective labels (for instance kP on the other side of A₀ ≅ kP).

              Instances For