Category cocycles and the map Ψ (toward Proposition 12.5)

A Hochschild two-cocycle φ of the category C of internal degree q gives the first-order deformation of C; restricted to the projective corner it is a cocycle μ of A₀, and its other restrictions are lifts of the actions on the evaluated modules (ν(m, a) = φ(a, m)) and of the arrow maps (g_a(m) = φ(m, a)). The mesh error of these lifts is Σ_a c_{x,a} φ(σa, a) (Ψc_catLift): this is how Ψ reads off the class of the deformation (deformation-refinements.tex: "Evaluation of every object at those projectives gives a free lift of its normalized module").

def MultiplicativeBasisDeformations.GExt.ActLift.ofBilin {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} (MM : GMod GΛ M) (ν₂ : M →ₗ[R] Λ →ₗ[R] M) (hdeg : ∀ (p d : ℤ) (m : M) (a : Λ), MM.gr.IsHom p m → GΛ.gr.IsHom d a → MM.gr.IsHom (p + d + q) ((ν₂ m) a)) (heq : ∀ (m : M) (a b : Λ), (ν₂ ((MM.act m) a)) b - (ν₂ m) (a * b) + (MM.act ((ν₂ m) a)) b = (MM.act m) ((μ a) b)) : ActLift μ q MM

A lifted action from a bilinear correction m * a = ma + εν(m, a).

theorem MultiplicativeBasisDeformations.GExt.ActLift.ofBilin_act {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] {μ : Λ →ₗ[R] Λ →ₗ[R] Λ} {q : ℤ} (MM : GMod GΛ M) (ν₂ : M →ₗ[R] Λ →ₗ[R] M) (hdeg : ∀ (p d : ℤ) (m : M) (a : Λ), MM.gr.IsHom p m → GΛ.gr.IsHom d a → MM.gr.IsHom (p + d + q) ((ν₂ m) a)) (heq : ∀ (m : M) (a b : Λ), (ν₂ ((MM.act m) a)) b - (ν₂ m) (a * b) + (MM.act ((ν₂ m) a)) b = (MM.act m) ((μ a) b)) (m : M) (a : Λ) : (ofBilin MM ν₂ hdeg heq).act m a = (ν₂ m) a

structure MultiplicativeBasisDeformations.MeshWalk.CatCocycle {k : Type u} [Field k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (q : ℕ) : Type u

A Hochschild two-cocycle of the category C of internal degree q.

• φ {X Y Z : V} : (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) → (ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) → (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Z)
• add_left {X Y Z : V} (f f' : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : self.φ (f + f') g = self.φ f g + self.φ f' g
• add_right {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g g' : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : self.φ f (g + g') = self.φ f g + self.φ f g'
• smul_left {X Y Z : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : self.φ (t • f) g = t • self.φ f g
• smul_right {X Y Z : V} (t : k) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : self.φ f (t • g) = t • self.φ f g
• cocycle {W X Y Z : V} (f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X) (g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : CategoryTheory.CategoryStruct.comp f (self.φ g h) - self.φ (CategoryTheory.CategoryStruct.comp f g) h + self.φ f (CategoryTheory.CategoryStruct.comp g h) - CategoryTheory.CategoryStruct.comp (self.φ f g) h = 0
• deg {X Y Z : V} {d e : ℕ} {f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} {g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z} : f ∈ ScalarMeshCategory.degreePart c d X Y → g ∈ ScalarMeshCategory.degreePart c e Y Z → self.φ f g ∈ ScalarMeshCategory.degreePart c (d + e + q) X Z

theorem MultiplicativeBasisDeformations.MeshWalk.CatCocycle.zero_left {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {q : ℕ} (Φ : CatCocycle c q) {X Y Z : V} (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.φ 0 g = 0

theorem MultiplicativeBasisDeformations.MeshWalk.CatCocycle.zero_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {q : ℕ} (Φ : CatCocycle c q) {X Y Z : V} (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : Φ.φ f 0 = 0

theorem MultiplicativeBasisDeformations.MeshWalk.CatCocycle.sum_left {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {q : ℕ} (Φ : CatCocycle c q) {X Y Z : V} {ι : Type u_1} (s : Finset ι) (f : ι → (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)) (g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.φ (∑ i ∈ s, f i) g = ∑ i ∈ s, Φ.φ (f i) g

theorem MultiplicativeBasisDeformations.MeshWalk.CatCocycle.sum_right {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {q : ℕ} (Φ : CatCocycle c q) {X Y Z : V} {ι : Type u_1} (s : Finset ι) (f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (g : ι → (ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z)) : Φ.φ f (∑ i ∈ s, g i) = ∑ i ∈ s, Φ.φ f (g i)

theorem MultiplicativeBasisDeformations.MeshWalk.CatCocycle.cocycle' {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {q : ℕ} (Φ : CatCocycle c q) {W X Y Z : V} (f : ScalarMeshCategory.obj c W ⟶ ScalarMeshCategory.obj c X) (g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) (h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z) : Φ.φ f (CategoryTheory.CategoryStruct.comp g h) = Φ.φ (CategoryTheory.CategoryStruct.comp f g) h + CategoryTheory.CategoryStruct.comp (Φ.φ f g) h - CategoryTheory.CategoryStruct.comp f (Φ.φ g h)

The cocycle identity, solved for φ(f, gh).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.CatCocycle.meshVal {k : Type u} [Field k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {q : ℕ} (Φ : CatCocycle c q) : ScalarMeshCategory.MeshFamily c

The mesh value Σ_a c_{x,a} φ(σa, a) of a category cocycle.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.catMu {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {q : ℕ} (Φ : CatCocycle c q) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

The cocycle of A₀: μ(a, b) = Σ_w φ(b_{yw}, a_{wz}).

theorem MultiplicativeBasisDeformations.MeshWalk.catMu_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ) (y z : D.PV) : MulOpposite.unop (((catMu D Φ) a) b) y z = ∑ w : D.PV, Φ.φ (MulOpposite.unop b y w) (MulOpposite.unop a w z)

theorem MultiplicativeBasisDeformations.MeshWalk.catMu_isHCocycle {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) : GExt.IsHCocycle (catMu D Φ)

theorem MultiplicativeBasisDeformations.MeshWalk.catMu_hDeg {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) : GExt.HDeg (galgA0 D hfin) (catMu D Φ) ↑q

noncomputable def MultiplicativeBasisDeformations.MeshWalk.catNu {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {q : ℕ} (Φ : CatCocycle c q) (X : V) : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)

The correction ν(m, a)_y = Σ_w φ(a_{yw}, m_w) of the action on M_X.

theorem MultiplicativeBasisDeformations.MeshWalk.catNu_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) (X : V) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (y : D.PV) : ((catNu D Φ X) m) a y = ∑ w : D.PV, Φ.φ (MulOpposite.unop a y w) (m w)

theorem MultiplicativeBasisDeformations.MeshWalk.evAct_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (X : V) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (y : D.PV) : ((evAct D X) m) a y = ∑ w : D.PV, CategoryTheory.CategoryStruct.comp (MulOpposite.unop a y w) (m w)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.catL {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) (X : V) : GExt.ActLift (catMu D Φ) (↑q) (gmodEv D hfin X)

The lifted action on M_X.

theorem MultiplicativeBasisDeformations.MeshWalk.catL_act {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) (X : V) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (catL D hfin Φ X).act m a = ((catNu D Φ X) m) a

noncomputable def MultiplicativeBasisDeformations.MeshWalk.catG {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) {q : ℕ} (Φ : CatCocycle c q) {y x : V} (α : y ⟶ x) : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)

The lifted arrow map g_a(m)_y = φ(m_y, a).

theorem MultiplicativeBasisDeformations.MeshWalk.catG_lift {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) {y x : V} (α : y ⟶ x) : GExt.IsLiftHom (catL D hfin Φ y) (catL D hfin Φ x) (fA D α) (catG D Φ α)

theorem MultiplicativeBasisDeformations.MeshWalk.catG_deg {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) {y x : V} (α : y ⟶ x) (p : ℤ) (m : CatAlg.Rep D.F0 (meshFam Q c y)) (hm : (zgrEv D hfin y).IsHom p m) : (zgrEv D hfin x).IsHom (p + (1 + ↑q)) ((catG D Φ α) m)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.catLift {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) : LiftData D hfin q (catMu D Φ)

The lift data of a category cocycle.

theorem MultiplicativeBasisDeformations.MeshWalk.Ψc_catLift {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {q : ℕ} (Φ : CatCocycle c q) : Ψc (catLift D hfin Φ) = Submodule.Quotient.mk Φ.meshVal

Ψ of the restricted cocycle is the mesh value [Σ_a c_{x,a} φ(σa, a)].