3. GrothendieckGroup.Defs
Module BridgelandStability.GrothendieckGroup.Defs — 6 declarations (Structure, Definition)
3.1. K0Presentation
Structure | BridgelandStability.GrothendieckGroup.Defs | Source | Open Issue
/-- A presentation of a Grothendieck-style group: objects, relations, and
the three-term decomposition `obj₂(r) = obj₁(r) + obj₃(r)`. -/
@[nolint checkUnivs]
structure K0Presentation (Obj : Type u) (Rel : Type v) where
/-- The first term of the relation (e.g., `T.obj₁` or `S.X₁`). -/
obj₁ : Rel → Obj
/-- The middle term (the one that equals the sum of the other two). -/
obj₂ : Rel → Obj
/-- The third term. -/
obj₃ : Rel → Obj
3.2. K0Presentation.subgroup
Definition | BridgelandStability.GrothendieckGroup.Defs | Source | Open Issue
/-- The subgroup of relations: `{obj₂(r) - obj₁(r) - obj₃(r) | r : Rel}`. -/
def subgroup : AddSubgroup (FreeAbelianGroup Obj) :=
AddSubgroup.closure
{x | ∃ r : Rel,
x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) -
FreeAbelianGroup.of (P.obj₃ r)}
3.3. K0Presentation.IsAdditive
Structure | BridgelandStability.GrothendieckGroup.Defs | Source | Open Issue
/-- A function on objects is *additive* for a presentation if it respects the relations. -/
class IsAdditive {A : Type*} [AddCommGroup A] (f : Obj → A) : Prop where
additive : ∀ r : Rel, f (P.obj₂ r) = f (P.obj₁ r) + f (P.obj₃ r)
3.4. K0Presentation.K0
Definition | BridgelandStability.GrothendieckGroup.Defs | Source | Open Issue
/-- The Grothendieck group: free abelian group on objects modulo the relations. -/
abbrev K0 : Type _ := FreeAbelianGroup Obj ⧸ P.subgroup
3.5. K0Presentation.instAddCommGroupK0
Definition | BridgelandStability.GrothendieckGroup.Defs | Source | Open Issue
instance : AddCommGroup P.K0 :=
inferInstanceAs (AddCommGroup (FreeAbelianGroup Obj ⧸ P.subgroup))
3.6. K0Presentation.lift
Definition | BridgelandStability.GrothendieckGroup.Defs | Source | Open Issue
/-- The universal property: an additive function lifts uniquely to a group homomorphism. -/
def lift {A : Type*} [AddCommGroup A] (f : Obj → A) [P.IsAdditive f] : P.K0 →+ A :=
QuotientAddGroup.lift P.subgroup (FreeAbelianGroup.lift f)
((AddSubgroup.closure_le _).mpr fun x ⟨r, hx⟩ ↦ Obj:Type uRel:Type vP:K0Presentation Obj RelA:Type u_1inst✝¹:AddCommGroup Af:Obj → Ainst✝:P.IsAdditive fx:FreeAbelianGroup Objx✝:x ∈ {x | ∃ r, x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) - FreeAbelianGroup.of (P.obj₃ r)}r:Relhx:x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) - FreeAbelianGroup.of (P.obj₃ r)⊢ x ∈ ↑(FreeAbelianGroup.lift f).ker
Obj:Type uRel:Type vP:K0Presentation Obj RelA:Type u_1inst✝¹:AddCommGroup Af:Obj → Ainst✝:P.IsAdditive fx:FreeAbelianGroup Objx✝:x ∈ {x | ∃ r, x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) - FreeAbelianGroup.of (P.obj₃ r)}r:Relhx:x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) - FreeAbelianGroup.of (P.obj₃ r)⊢ f (P.obj₂ r) - f (P.obj₁ r) - f (P.obj₃ r) = 0
Obj:Type uRel:Type vP:K0Presentation Obj RelA:Type u_1inst✝¹:AddCommGroup Af:Obj → Ainst✝:P.IsAdditive fx:FreeAbelianGroup Objx✝:x ∈ {x | ∃ r, x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) - FreeAbelianGroup.of (P.obj₃ r)}r:Relhx:x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) - FreeAbelianGroup.of (P.obj₃ r)h:f (P.obj₂ r) = f (P.obj₁ r) + f (P.obj₃ r)⊢ f (P.obj₂ r) - f (P.obj₁ r) - f (P.obj₃ r) = 0
Obj:Type uRel:Type vP:K0Presentation Obj RelA:Type u_1inst✝¹:AddCommGroup Af:Obj → Ainst✝:P.IsAdditive fx:FreeAbelianGroup Objx✝:x ∈ {x | ∃ r, x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) - FreeAbelianGroup.of (P.obj₃ r)}r:Relhx:x = FreeAbelianGroup.of (P.obj₂ r) - FreeAbelianGroup.of (P.obj₁ r) - FreeAbelianGroup.of (P.obj₃ r)h:f (P.obj₂ r) = f (P.obj₁ r) + f (P.obj₃ r)⊢ f (P.obj₁ r) + f (P.obj₃ r) - f (P.obj₁ r) - f (P.obj₃ r) = 0; All goals completed! 🐙)