Documentation

Mathlib.Algebra.Category.Grp.FiniteGrp

Main definitions and results #

structure FiniteGrp :
Type (u_1 + 1)

The category of finite groups.

  • toGrp : Grp

    A group that is finite

  • isFinite : Finite self.toGrp
Instances For
    theorem FiniteGrp.isFinite (self : FiniteGrp.{u_1}) :
    Finite self.toGrp
    structure FiniteAddGrp :
    Type (u_1 + 1)

    The category of finite additive groups.

    • toAddGrp : AddGrp

      An add group that is finite

    • isFinite : Finite self.toAddGrp
    Instances For
      theorem FiniteAddGrp.isFinite (self : FiniteAddGrp.{u_1}) :
      Finite self.toAddGrp
      Equations
      Equations
      Equations
      • =
      Equations
      • =
      Equations
      instance FiniteGrp.instFunLikeHomαGroupToGrp (G : FiniteGrp.{u_1}) (H : FiniteGrp.{u_1}) :
      FunLike (G H) G.toGrp H.toGrp
      Equations
      Equations
      • =

      Construct a term of FiniteAddGrp from a type endowed with the structure of a finite additive group.

      Equations
      Instances For

        Construct a term of FiniteGrp from a type endowed with the structure of a finite group.

        Equations
        Instances For
          def FiniteAddGrp.ofHom {X : Type u} {Y : Type u} [AddGroup X] [Finite X] [AddGroup Y] [Finite Y] (f : X →+ Y) :

          The morphism in FiniteAddGrp, induced from a morphism of the category AddGrp

          Equations
          Instances For
            def FiniteGrp.ofHom {X : Type u} {Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) :

            The morphism in FiniteGrp, induced from a morphism of the category Grp.

            Equations
            Instances For
              theorem FiniteAddGrp.ofHom_apply {X : Type u} {Y : Type u} [AddGroup X] [Finite X] [AddGroup Y] [Finite Y] (f : X →+ Y) (x : X) :
              theorem FiniteGrp.ofHom_apply {X : Type u} {Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) (x : X) :
              (FiniteGrp.ofHom f) x = f x