def DegreeAdditivity.K0SESRelSet (R : Type u) [Ring R] : Set (FreeAbelianGroup (ModuleCat R))

The set of relations in K^0 arising from short exact sequences 0 → A → B → C → 0: each yields the relation [B] - [A] - [C] = 0.

def DegreeAdditivity.K0SESRelSubgroup (R : Type u) [Ring R] : AddSubgroup (FreeAbelianGroup (ModuleCat R))

Subgroup generated by all SES-relations; quotienting by it yields the Grothendieck group.

@[reducible, inline]

abbrev DegreeAdditivity.GrothendieckGroupK0 (R : Type u) [Ring R] : Type (u + 1)

Grothendieck group K^0(A) = K^0(R-Mod) (Def 42, Lec 22): free abelian on iso classes of modules modulo [B] = [A] + [C] for every SES 0 → A → B → C → 0.

def DegreeAdditivity.GrothendieckGroupK0.classOf (R : Type u) [Ring R] (M : ModuleCat R) : GrothendieckGroupK0 R

The class [M] of a module M in K^0(R).

theorem DegreeAdditivity.GrothendieckGroupK0.ses_relation (R : Type u) [Ring R] {A B C : ModuleCat R} (f : ↑A →ₗ[R] ↑B) (g : ↑B →ₗ[R] ↑C) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (hex : Function.Exact ⇑f ⇑g) : classOf R B = classOf R A + classOf R C

Defining relation in K^0: for any SES 0 → A → B → C → 0, [B] = [A] + [C].

theorem DegreeAdditivity.GrothendieckGroupK0.classOf_zero (R : Type u) [Ring R] : classOf R (ModuleCat.of R PUnit.{u + 1}) = 0

The class of the zero module vanishes in K^0.

theorem DegreeAdditivity.GrothendieckGroupK0.classOf_prod (R : Type u) [Ring R] (M N : ModuleCat R) : classOf R (ModuleCat.of R (↑M × ↑N)) = classOf R M + classOf R N

Additivity on direct sums: [M × N] = [M] + [N] in K^0.

theorem DegreeAdditivity.GrothendieckGroupK0.classOf_iso (R : Type u) [Ring R] (M N : ModuleCat R) (e : ↑M ≃ₗ[R] ↑N) : classOf R M = classOf R N

Isomorphic modules have the same class in K^0.

def DegreeAdditivity.IsSESAdditive (R : Type u) [Ring R] {G : Type u_1} [AddCommGroup G] (φ : ModuleCat R → G) : Prop

A function φ to an abelian group is SES-additive when φ(B) = φ(A) + φ(C) holds for every short exact sequence. This is the universal property tested by K^0.

theorem DegreeAdditivity.K0SESRelSubgroup_le_ker (R : Type u) [Ring R] {G : Type u_1} [AddCommGroup G] (φ : ModuleCat R → G) (hφ : IsSESAdditive R φ) : K0SESRelSubgroup R ≤ (FreeAbelianGroup.lift φ).ker

If φ is SES-additive, then the lifted homomorphism vanishes on every SES-relation.

def DegreeAdditivity.GrothendieckGroupK0.lift (R : Type u) [Ring R] {G : Type u_1} [AddCommGroup G] (φ : ModuleCat R → G) (hφ : IsSESAdditive R φ) : GrothendieckGroupK0 R →+ G

Universal property: lift an SES-additive φ : Mod → G to a homomorphism K^0(R) → G.

theorem DegreeAdditivity.GrothendieckGroupK0.lift_classOf (R : Type u) [Ring R] {G : Type u_1} [AddCommGroup G] (φ : ModuleCat R → G) (hφ : IsSESAdditive R φ) (M : ModuleCat R) : (lift R φ hφ) (classOf R M) = φ M

Computation: the universal lift sends [M] to φ M.

theorem DegreeAdditivity.GrothendieckGroupK0.lift_unique (R : Type u) [Ring R] {G : Type u_1} [AddCommGroup G] (ψ₁ ψ₂ : GrothendieckGroupK0 R →+ G) (h : ∀ (M : ModuleCat R), ψ₁ (classOf R M) = ψ₂ (classOf R M)) : ψ₁ = ψ₂

Uniqueness in the universal property: two homomorphisms agreeing on all classes [M] are equal.