2. GrothendieckGroup.Basic
Module BridgelandStability.GrothendieckGroup.Basic — 8 declarations (Structure, Definition, Theorem)
2.1. CategoryTheory.Triangulated.IsTriangleAdditive
Structure | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue
/-- A function `f : C → A` to an additive group is triangle-additive if
`f(B) = f(A) + f(C)` for every distinguished triangle `A → B → C → A⟦1⟧`. -/
class IsTriangleAdditive {A : Type*} [AddCommGroup A] (f : C → A) : Prop where
additive : ∀ (T : Pretriangulated.Triangle C),
T ∈ (distTriang C) → f T.obj₂ = f T.obj₁ + f T.obj₃
2.2. CategoryTheory.Triangulated.trianglePresentation
Definition | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue
/-- The `K0Presentation` for distinguished triangles in a pretriangulated category:
generators are objects of `C`, relations are distinguished triangles. -/
abbrev trianglePresentation :
K0Presentation C {T : Pretriangulated.Triangle C // T ∈ distTriang C} where
obj₁ := fun r => r.1.obj₁
obj₂ := fun r => r.1.obj₂
obj₃ := fun r => r.1.obj₃
2.3. CategoryTheory.Triangulated.instIsAdditiveSubtypeTriangleMemSetDistinguishedTrianglesTrianglePresentationOfIsTriangleAdditive
Theorem | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue
instance {A : Type*} [AddCommGroup A] (f : C → A) [IsTriangleAdditive f] :
(trianglePresentation C).IsAdditive fShow proof
where
additive := fun ⟨T, hT⟩ => IsTriangleAdditive.additive T hT
2.4. CategoryTheory.Triangulated.K₀
Definition | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue
/-- The Grothendieck group of a pretriangulated category `C`, defined as the quotient of
`FreeAbelianGroup C` by the distinguished triangle relations. -/
def K₀ : Type _ := (trianglePresentation C).K0
2.5. CategoryTheory.Triangulated.K₀.instAddCommGroup
Definition | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue
instance K₀.instAddCommGroup : AddCommGroup (K₀ C) :=
inferInstanceAs (AddCommGroup (trianglePresentation C).K0)
2.6. CategoryTheory.Triangulated.K₀.of
Definition | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue
/-- The class map sending an object `X` of `C` to its class `[X]` in `K₀ C`. -/
def K₀.of (X : C) : K₀ C :=
QuotientAddGroup.mk (FreeAbelianGroup.of X)
2.7. CategoryTheory.Triangulated.K₀.lift
Definition | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue
/-- The universal property of K₀: any triangle-additive function lifts
to an additive group homomorphism from K₀. -/
def K₀.lift {A : Type*} [AddCommGroup A] (f : C → A) [IsTriangleAdditive f] : K₀ C →+ A :=
(trianglePresentation C).lift f
2.8. CategoryTheory.Triangulated.cl
Definition | BridgelandStability.GrothendieckGroup.Basic | Source | Open Issue
/-- The class of an object `E` in the target lattice `Λ`, via the class map
`v : K₀(C) → Λ`. This is `v([E])` in the notation of Bridgeland, BMS16, etc.
At `v = id`: `cl v E = K₀.of C E` definitionally. -/
abbrev cl (E : C) : Λ := v (K₀.of C E)