Documentation

Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

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 #

source
🔸 coverage
@[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.

Instances For
    source
    🔸 coverage
    @[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.

    Instances For
      source
      🔸 coverage
      @[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.

      Instances For
        source
        🔸 coverage
        @[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.

        Instances For
          source
          📐 coverage
          theorem Algebra.GrothendieckGroup.of_injective {M : Type u_1} [CommMonoid M] [IsCancelMul M] :
          Function.Injective ⇑of
          source
          📐 coverage
          theorem Algebra.GrothendieckAddGroup.of_injective {M : Type u_1} [AddCommMonoid M] [IsCancelAdd M] :
          Function.Injective ⇑of
          source
          🔸 coverage
          @[implicit_reducible]
          instance Algebra.GrothendieckGroup.instInv {M : Type u_1} [CommMonoid M] :
          Inv (GrothendieckGroup M)
          source
          🔸 coverage
          @[implicit_reducible]
          instance Algebra.GrothendieckAddGroup.instNeg {M : Type u_1} [AddCommMonoid M] :
          Neg (GrothendieckAddGroup M)
          source
          📐 coverage
          @[simp]
          theorem Algebra.GrothendieckGroup.inv_mk {M : Type u_1} [CommMonoid M] (m : M) (s : ↥⊤) :
          (Localization.mk m s)⁻¹ = Localization.mk ↑s ⟨m, ⋯⟩
          source
          📐 coverage
          @[simp]
          theorem Algebra.GrothendieckAddGroup.neg_mk {M : Type u_1} [AddCommMonoid M] (m : M) (s : ↥⊤) :
          -AddLocalization.mk m s = AddLocalization.mk ↑s ⟨m, ⋯⟩
          source
          🔸 coverage
          @[implicit_reducible]
          instance Algebra.GrothendieckGroup.instCommGroup {M : Type u_1} [CommMonoid M] :
          CommGroup (GrothendieckGroup M)

          The Grothendieck group is a group.

          source
          🔸 coverage
          @[implicit_reducible]
          instance Algebra.GrothendieckAddGroup.instAddCommGroup {M : Type u_1} [AddCommMonoid M] :
          AddCommGroup (GrothendieckAddGroup M)

          The Grothendieck group is a group.

          source
          📐 coverage
          @[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₂, ⋯⟩
          source
          📐 coverage
          @[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₂, ⋯⟩
          source
          🔸 coverage
          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.

          Instances For
            source
            🔸 coverage
            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.

            Instances For
              source
              📐 coverage
              @[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
              source
              📐 coverage
              @[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
              source
              📐 coverage
              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
              source
              📐 coverage
              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