Main definitions and results

• FiniteGrp is the category of finite groups.

structure FiniteGrp : Type (u_1 + 1)

The category of finite groups.

• toGrp : GrpCat

  A group that is finite

• isFinite : Finite ↑self.toGrp

structure FiniteAddGrp : Type (u_1 + 1)

The category of finite additive groups.

• toAddGrp : AddGrpCat

  An additive group that is finite

• isFinite : Finite ↑self.toAddGrp

instance FiniteGrp.instCoeSortType : CoeSort FiniteGrp.{u} (Type u)

instance FiniteAddGrp.instCoeSortType : CoeSort FiniteAddGrp.{u} (Type u)

instance FiniteGrp.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} FiniteGrp.{u_1}

instance FiniteAddGrp.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} FiniteAddGrp.{u_1}

instance FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp : CategoryTheory.ConcreteCategory FiniteGrp.{u_1} fun (x1 x2 : FiniteGrp.{u_1}) => ↑x1.toGrp →* ↑x2.toGrp

instance FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp : CategoryTheory.ConcreteCategory FiniteAddGrp.{u_1} fun (x1 x2 : FiniteAddGrp.{u_1}) => ↑x1.toAddGrp →+ ↑x2.toAddGrp

instance FiniteGrp.instGroupCarrierToGrp (G : FiniteGrp.{u_1}) : Group ↑G.toGrp

instance FiniteAddGrp.instAddGroupCarrierToAddGrp (G : FiniteAddGrp.{u_1}) : AddGroup ↑G.toAddGrp

instance FiniteGrp.instFiniteCarrierToGrp (G : FiniteGrp.{u_1}) : Finite ↑G.toGrp

instance FiniteAddGrp.instFiniteCarrierToAddGrp (G : FiniteAddGrp.{u_1}) : Finite ↑G.toAddGrp

def FiniteGrp.of (G : Type u) [Group G] [Finite G] : FiniteGrp.{u}

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

def FiniteAddGrp.of (G : Type u) [AddGroup G] [Finite G] : FiniteAddGrp.{u}

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

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

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

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

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

theorem FiniteGrp.ofHom_apply {X Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem FiniteAddGrp.ofHom_apply {X Y : Type u} [AddGroup X] [Finite X] [AddGroup Y] [Finite Y] (f : X →+ Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x