Documentation

TauCeti.Algebra.Category.CommGrpCat.FiniteGeneration

Finitely generated commutative groups #

This file packages finitely generated commutative groups as a full subcategory of CommGrpCat.

Main declarations #

source
instance TauCeti.instFGULift (G : Type v) [Group G] [Group.FG G] :
Group.FG (ULift.{u, v} G)

Universe lifts of finitely generated groups are finitely generated.

source
def TauCeti.CommGrpCat.isFG :
CategoryTheory.ObjectProperty CommGrpCat

The object property of being a finitely generated commutative group.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.CommGrpCat.isFG_iff (G : CommGrpCat) :
    isFG G ↔ Group.FG ↑G

    Membership in the finitely generated commutative-group object property.

    source
    @[reducible, inline]
    abbrev TauCeti.FGCommGrpCat :
    Type (u_1 + 1)

    The category of finitely generated commutative groups.

    Equations
    Instances For
      source
      @[reducible]
      def TauCeti.FGCommGrpCat.carrier (G : FGCommGrpCat) :
      Type v

      The underlying type of a finitely generated commutative group.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance TauCeti.FGCommGrpCat.instCoeSortType :
        CoeSort FGCommGrpCat (Type v)

        Objects of FGCommGrpCat coerce to their underlying type.

        Equations
        source
        @[instance_reducible]
        instance TauCeti.FGCommGrpCat.instCommGroupCarrier (G : FGCommGrpCat) :
        CommGroup ↑G

        An object of FGCommGrpCat inherits the commutative-group structure of its underlying group.

        Equations
        source
        instance TauCeti.FGCommGrpCat.instFGCarrier (G : FGCommGrpCat) :
        Group.FG ↑G

        The underlying group of an object of FGCommGrpCat is finitely generated.

        source
        @[reducible, inline]
        abbrev TauCeti.FGCommGrpCat.of (G : Type v) [CommGroup G] [Group.FG G] :
        FGCommGrpCat

        Construct an object of FGCommGrpCat from a finitely generated commutative group.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev TauCeti.FGCommGrpCat.ofHom {G H : Type v} [CommGroup G] [Group.FG G] [CommGroup H] [Group.FG H] (φ : G →* H) :
          of G ⟶ of H

          Lift a group homomorphism between finitely generated commutative groups to FGCommGrpCat.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev TauCeti.FGCommGrpCat.toMonoidHom {G H : FGCommGrpCat} (φ : G ⟶ H) :
            ↑G →* ↑H

            The group homomorphism underlying a morphism in FGCommGrpCat.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.FGCommGrpCat.ofHom_toMonoidHom {G H : FGCommGrpCat} (φ : G ⟶ H) :
              ofHom (toMonoidHom φ) = φ
              source
              @[simp]
              theorem TauCeti.FGCommGrpCat.toMonoidHom_ofHom {G H : Type v} [CommGroup G] [Group.FG G] [CommGroup H] [Group.FG H] (φ : G →* H) :
              toMonoidHom (ofHom φ) = φ
              source
              theorem TauCeti.FGCommGrpCat.hom_ext {G H : FGCommGrpCat} {φ ψ : G ⟶ H} (h : toMonoidHom φ = toMonoidHom ψ) :
              φ = ψ

              Two morphisms in FGCommGrpCat are equal when their underlying group homomorphisms are equal.

              source
              theorem TauCeti.FGCommGrpCat.hom_ext_iff {G H : FGCommGrpCat} {φ ψ : G ⟶ H} :
              φ = ψ ↔ toMonoidHom φ = toMonoidHom ψ
              source
              @[simp]
              theorem TauCeti.FGCommGrpCat.toMonoidHom_id {G : FGCommGrpCat} :
              toMonoidHom (CategoryTheory.CategoryStruct.id G) = MonoidHom.id ↑G
              source
              @[simp]
              theorem TauCeti.FGCommGrpCat.toMonoidHom_comp {G H K : FGCommGrpCat} (φ : G ⟶ H) (ψ : H ⟶ K) :
              toMonoidHom (CategoryTheory.CategoryStruct.comp φ ψ) = (toMonoidHom ψ).comp (toMonoidHom φ)