The Grothendieck ring of a semiring

Mathlib's Algebra.GrothendieckAddGroup M is the group completion of an additive commutative monoid M, realized as the localization of M at its top submonoid. When M carries a semiring structure the completion carries a ring structure, uniquely determined by the requirement that the canonical map Algebra.GrothendieckAddGroup.of be multiplicative, and it is commutative when the semiring is. This file constructs that ring.

The multiplication is built from the universal property rather than from the underlying quotient: multiplication by a fixed element of the semiring extends to an additive endomorphism of the completion, and the assignment of that endomorphism is itself additive, so it extends once more. No well-definedness computation on the localization relation is needed, and no cancellativity hypothesis is used.

Main definitions

• Algebra.GrothendieckAddGroup.liftAddEquiv: Mathlib's lift as an additive isomorphism.
• Algebra.GrothendieckAddGroup.instRing and Algebra.GrothendieckAddGroup.instCommRing: the ring structure, commutative when the semiring is.
• Algebra.GrothendieckAddGroup.ofRingHom: the canonical semiring map into the completion.
• Algebra.GrothendieckAddGroup.liftRingHom: the universal property, as an equivalence between semiring homomorphisms out of S into a ring and ring homomorphisms out of the completion.

References

• Grothendieck group, Wikipedia

The universal property, in additive form

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

Restricting the extension of f along of recovers f.

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

The extension of f agrees with f on the image of the monoid.

theorem Algebra.GrothendieckAddGroup.addHom_ext {M : Type u_1} [AddCommMonoid M] {G : Type u_2} [AddCommGroup G] {F₁ F₂ : GrothendieckAddGroup M →+ G} (h : ∀ (a : M), F₁ (of a) = F₂ (of a)) : F₁ = F₂

Two additive maps out of the Grothendieck group agree as soon as they agree on the image of the monoid.

theorem Algebra.GrothendieckAddGroup.exists_eq_sub_of {M : Type u_1} [AddCommMonoid M] (x : GrothendieckAddGroup M) : ∃ (a : M) (b : M), x = of a - of b

Every element of the Grothendieck group is a difference of two elements of the monoid.

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

The universal property of the Grothendieck group, upgraded to an isomorphism of the additive groups of homomorphisms.

@[simp]

theorem Algebra.GrothendieckAddGroup.coe_liftAddEquiv {M : Type u_1} [AddCommMonoid M] {G : Type u_2} [AddCommGroup G] : ⇑liftAddEquiv = ⇑lift

The multiplication

@[instance_reducible]

noncomputable instance Algebra.GrothendieckAddGroup.instMul {S : Type u_3} [NonUnitalNonAssocSemiring S] : Mul (GrothendieckAddGroup S)

Multiplication on the Grothendieck ring of a semiring: the universal property extends fun a b => of (a * b) first in b, then in a.

theorem Algebra.GrothendieckAddGroup.of_mul_of {S : Type u_3} [NonUnitalNonAssocSemiring S] (a b : S) : of a * of b = of (a * b)

The canonical map into the Grothendieck ring is multiplicative.

@[instance_reducible]

noncomputable instance Algebra.GrothendieckAddGroup.instNonUnitalNonAssocRing {S : Type u_3} [NonUnitalNonAssocSemiring S] : NonUnitalNonAssocRing (GrothendieckAddGroup S)

The Grothendieck group of a non-unital non-associative semiring is a non-unital non-associative ring for the induced multiplication.

@[instance_reducible]

noncomputable instance Algebra.GrothendieckAddGroup.instNonUnitalRing {S : Type u_3} [NonUnitalSemiring S] : NonUnitalRing (GrothendieckAddGroup S)

The Grothendieck group of a non-unital semiring is a non-unital ring.

@[instance_reducible]

noncomputable instance Algebra.GrothendieckAddGroup.instOne {S : Type u_3} [NonAssocSemiring S] : One (GrothendieckAddGroup S)

The unit of the Grothendieck ring of a semiring.

theorem Algebra.GrothendieckAddGroup.one_def {S : Type u_3} [NonAssocSemiring S] : 1 = of 1

The unit of the Grothendieck ring is the image of the unit of the semiring.

@[instance_reducible]

noncomputable instance Algebra.GrothendieckAddGroup.instNonAssocRing {S : Type u_3} [NonAssocSemiring S] : NonAssocRing (GrothendieckAddGroup S)

The Grothendieck group of a possibly nonassociative semiring is a possibly nonassociative ring.

@[instance_reducible]

noncomputable instance Algebra.GrothendieckAddGroup.instRing {S : Type u_3} [Semiring S] : Ring (GrothendieckAddGroup S)

The Grothendieck ring: the group completion of the additive monoid underlying a semiring is a ring, with the multiplication induced by that of the semiring.

noncomputable def Algebra.GrothendieckAddGroup.ofRingHom {S : Type u_3} [NonAssocSemiring S] : S →+* GrothendieckAddGroup S

The canonical map from a semiring into its Grothendieck ring.

@[simp]

theorem Algebra.GrothendieckAddGroup.coe_ofRingHom {S : Type u_3} [NonAssocSemiring S] : ⇑ofRingHom = ⇑of

theorem Algebra.GrothendieckAddGroup.ofRingHom_apply {S : Type u_3} [NonAssocSemiring S] (a : S) : ofRingHom a = of a

The canonical ring map agrees with the canonical additive map on elements.

The universal property, in ring form

theorem Algebra.GrothendieckAddGroup.ringHom_ext {S : Type u_3} [NonAssocSemiring S] {R : Type u_4} [NonAssocRing R] {F₁ F₂ : GrothendieckAddGroup S →+* R} (h : ∀ (a : S), F₁ (of a) = F₂ (of a)) : F₁ = F₂

Two ring homomorphisms out of the Grothendieck ring agree as soon as they agree on the image of the semiring.

noncomputable def Algebra.GrothendieckAddGroup.liftRingHom {S : Type u_3} [NonAssocSemiring S] {R : Type u_4} [NonAssocRing R] : (S →+* R) ≃ (GrothendieckAddGroup S →+* R)

The universal property of the Grothendieck ring: a semiring homomorphism from S to a ring extends uniquely to the Grothendieck ring of S.

theorem Algebra.GrothendieckAddGroup.liftRingHom_apply_of {S : Type u_3} [NonAssocSemiring S] {R : Type u_4} [NonAssocRing R] (f : S →+* R) (a : S) : (liftRingHom f) (of a) = f a

The ring-homomorphism extension evaluates to the original semiring homomorphism on each generator.

@[simp]

theorem Algebra.GrothendieckAddGroup.liftRingHom_symm_apply {S : Type u_3} [NonAssocSemiring S] {R : Type u_4} [NonAssocRing R] (F : GrothendieckAddGroup S →+* R) : liftRingHom.symm F = F.comp ofRingHom

The inverse universal-property equivalence restricts a ring homomorphism along ofRingHom.

@[instance_reducible]

noncomputable instance Algebra.GrothendieckAddGroup.instCommRing {S : Type u_3} [CommSemiring S] : CommRing (GrothendieckAddGroup S)

The Grothendieck ring of a commutative semiring is commutative.