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.

Equations

• Algebra.GrothendieckGroup M = Localization ⊤

@[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.

Equations

• Algebra.GrothendieckAddGroup M = AddLocalization ⊤

@[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.

Equations

• Algebra.GrothendieckGroup.of = (Localization.monoidOf ⊤).toMonoidHom

@[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.

Equations

• Algebra.GrothendieckAddGroup.of = (AddLocalization.addMonoidOf ⊤).toAddMonoidHom

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)

Equations

• Algebra.GrothendieckGroup.instInv = { inv := fun (x : Localization ⊤) => Localization.rec (fun (m : M) (s : ↥⊤) => Localization.mk ↑s ⟨m, ⋯⟩) ⋯ x }

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

Equations

• Algebra.GrothendieckAddGroup.instNeg = { neg := fun (x : AddLocalization ⊤) => AddLocalization.rec (fun (m : M) (s : ↥⊤) => AddLocalization.mk ↑s ⟨m, ⋯⟩) ⋯ x }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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

The Grothendieck group is a group.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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