Grothendieck group

The Grothendieck group of a commutative monoid M is the "smallest" commutative group G containing M, in the sense that monoid homs M → H are in bijection with monoid homs G → H for any commutative group H.

Note that "Grothendieck group" also refers to the analogous construction in an abelian category obtained by formally making the last term of each short exact sequence invertible.

References

• Grothendieck group, Wikipedia

@[reducible, inline]

abbrev Algebra.GrothendieckGroup (M : Type u_1) [CommMonoid M] : Type u_1

The Grothendieck group of a monoid M is the localization at its top submonoid.

@[reducible, inline]

abbrev Algebra.GrothendieckAddGroup (M : Type u_1) [AddCommMonoid M] : Type u_1

The Grothendieck group of an additive monoid M is the localization at its top submonoid.

@[reducible, inline]

abbrev Algebra.GrothendieckGroup.of {M : Type u_1} [CommMonoid M] : M →* GrothendieckGroup M

The inclusion from a commutative monoid M to its Grothendieck group.

Note that this is only injective if M is cancellative.

@[reducible, inline]

abbrev Algebra.GrothendieckAddGroup.of {M : Type u_1} [AddCommMonoid M] : M →+ GrothendieckAddGroup M

The inclusion from an additive commutative monoid M to its Grothendieck group.

Note that this is only injective if M is cancellative.

theorem Algebra.GrothendieckGroup.of_injective {M : Type u_1} [CommMonoid M] [IsCancelMul M] : Function.Injective ⇑of

theorem Algebra.GrothendieckAddGroup.of_injective {M : Type u_1} [AddCommMonoid M] [IsCancelAdd M] : Function.Injective ⇑of

instance Algebra.GrothendieckGroup.instInv {M : Type u_1} [CommMonoid M] : Inv (GrothendieckGroup M)

instance Algebra.GrothendieckAddGroup.instNeg {M : Type u_1} [AddCommMonoid M] : Neg (GrothendieckAddGroup M)

@[simp]

theorem Algebra.GrothendieckGroup.inv_mk {M : Type u_1} [CommMonoid M] (m : M) (s : ↥⊤) : (Localization.mk m s)⁻¹ = Localization.mk ↑s ⟨m, ⋯⟩

@[simp]

theorem Algebra.GrothendieckAddGroup.neg_mk {M : Type u_1} [AddCommMonoid M] (m : M) (s : ↥⊤) : -AddLocalization.mk m s = AddLocalization.mk ↑s ⟨m, ⋯⟩

instance Algebra.GrothendieckGroup.instCommGroup {M : Type u_1} [CommMonoid M] : CommGroup (GrothendieckGroup M)

The Grothendieck group is a group.

instance Algebra.GrothendieckAddGroup.instAddCommGroup {M : Type u_1} [AddCommMonoid M] : AddCommGroup (GrothendieckAddGroup M)

The Grothendieck group is a group.

@[simp]

theorem Algebra.GrothendieckGroup.mk_div_mk {M : Type u_1} [CommMonoid M] (m₁ m₂ : M) (s₁ s₂ : ↥⊤) : Localization.mk m₁ s₁ / Localization.mk m₂ s₂ = Localization.mk (m₁ * ↑s₂) ⟨↑s₁ * m₂, ⋯⟩

@[simp]

theorem Algebra.GrothendieckAddGroup.mk_sub_mk {M : Type u_1} [AddCommMonoid M] (m₁ m₂ : M) (s₁ s₂ : ↥⊤) : AddLocalization.mk m₁ s₁ - AddLocalization.mk m₂ s₂ = AddLocalization.mk (m₁ + ↑s₂) ⟨↑s₁ + m₂, ⋯⟩

noncomputable def Algebra.GrothendieckGroup.lift {M : Type u_1} {G : Type u_2} [CommMonoid M] [CommGroup G] : (M →* G) ≃ (GrothendieckGroup M →* G)

A monoid homomorphism from a monoid M to a group G lifts to a group homomorphism from the Grothendieck group of M to G.

noncomputable def Algebra.GrothendieckAddGroup.lift {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] : (M →+ G) ≃ (GrothendieckAddGroup M →+ G)

A monoid homomorphism from a monoid M to a group G lifts to a group homomorphism from the Grothendieck group of M to G.

@[simp]

theorem Algebra.GrothendieckGroup.lift_symm_apply {M : Type u_1} {G : Type u_2} [CommMonoid M] [CommGroup G] (f : GrothendieckGroup M →* G) : lift.symm f = f.comp of

@[simp]

theorem Algebra.GrothendieckAddGroup.lift_symm_apply {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (f : GrothendieckAddGroup M →+ G) : lift.symm f = f.comp of

theorem Algebra.GrothendieckGroup.lift_apply {M : Type u_1} {G : Type u_2} [CommMonoid M] [CommGroup G] (f : M →* G) (x : GrothendieckGroup M) : (lift f) x = f ((Localization.monoidOf ⊤).sec x).1 / f ↑((Localization.monoidOf ⊤).sec x).2

theorem Algebra.GrothendieckAddGroup.lift_apply {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (f : M →+ G) (x : GrothendieckAddGroup M) : (lift f) x = f ((AddLocalization.addMonoidOf ⊤).sec x).1 - f ↑((AddLocalization.addMonoidOf ⊤).sec x).2