Ambient Mukai charges and restriction to a heart

This module is the categorical transport layer for the Mukai exponential charge. An additive Mukai class map on K₀ C determines an additive complex charge on K₀ C; restriction along K₀Ab.toAmbient gives the corresponding heart datum. Triangle and shift formulas are then inherited from the Grothendieck group rather than reproved from the charge formula.

noncomputable def CategoryTheory.Triangulated.MukaiChargeData.ofAmbient {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (t : TStructure C) (m : K₀ C →+ Mukai.RealExtension V) : MukaiChargeData t.heart.FullSubcategory V

The heart datum of an ambient Mukai class map, by restriction along K₀Ab.toAmbient.

Equations

• CategoryTheory.Triangulated.MukaiChargeData.ofAmbient t m = { mukai := m.comp (CategoryTheory.K₀Ab.toAmbient t) }

@[simp]

theorem CategoryTheory.Triangulated.MukaiChargeData.ofAmbient_mukai {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (t : TStructure C) (m : K₀ C →+ Mukai.RealExtension V) (E : t.heart.FullSubcategory) : (ofAmbient t m).mukai (K₀Ab.of E) = m (K₀.of C E.obj)

noncomputable def CategoryTheory.Triangulated.MukaiChargeData.ambientChargeHom {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (m : K₀ C →+ Mukai.RealExtension V) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : K₀ C →+ ℂ

The exponential Mukai charge as an additive homomorphism on ambient Grothendieck classes.

Equations

• CategoryTheory.Triangulated.MukaiChargeData.ambientChargeHom m b β ω = (Mukai.expChargeHom b β ω).comp m

@[simp]

theorem CategoryTheory.Triangulated.MukaiChargeData.ambientChargeHom_apply {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (m : K₀ C →+ Mukai.RealExtension V) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (x : K₀ C) : (ambientChargeHom m b β ω) x = Mukai.expCharge b β ω (m x)

noncomputable def CategoryTheory.Triangulated.MukaiChargeData.ambientCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (m : K₀ C →+ Mukai.RealExtension V) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (X : C) : ℂ

The ambient charge, on any object of C.

Equations

• CategoryTheory.Triangulated.MukaiChargeData.ambientCharge m b β ω X = (CategoryTheory.Triangulated.MukaiChargeData.ambientChargeHom m b β ω) (CategoryTheory.Triangulated.K₀.of C X)

@[simp]

theorem CategoryTheory.Triangulated.MukaiChargeData.ambientCharge_obj {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (t : TStructure C) (m : K₀ C →+ Mukai.RealExtension V) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (E : t.heart.FullSubcategory) : ambientCharge m b β ω E.obj = charge b β ω (ofAmbient t m) E

On a heart object the ambient charge is the restricted heart charge — by construction.

theorem CategoryTheory.Triangulated.MukaiChargeData.ambientCharge_triangle {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (m : K₀ C →+ Mukai.RealExtension V) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {T : Pretriangulated.Triangle C} (hT : T ∈ Pretriangulated.distinguishedTriangles) : ambientCharge m b β ω T.obj₂ = ambientCharge m b β ω T.obj₁ + ambientCharge m b β ω T.obj₃

The ambient charge is additive on distinguished triangles.

theorem CategoryTheory.Triangulated.MukaiChargeData.ambientCharge_shift {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {V : Type u_2} [AddCommGroup V] [Module ℝ V] (m : K₀ C →+ Mukai.RealExtension V) (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (X : C) : ambientCharge m b β ω ((shiftFunctor C 1).obj X) = -ambientCharge m b β ω X

A shift negates the ambient charge.