Main definitions and results

• FiniteGrp is the category of finite groups.

structure FiniteGrp : Type (u_1 + 1)

The category of finite groups.

• toGrp : Grp

  A group that is finite

• isFinite : 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

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

Equations

• FiniteGrp.instCoeSortType = { coe := fun (G : FiniteGrp.{?u.1}) => ↑G.toGrp }

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

Equations

• FiniteAddGrp.instCoeSortType = { coe := fun (G : FiniteAddGrp.{?u.1}) => ↑G.toAddGrp }

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

Equations

• FiniteGrp.instCategory = CategoryTheory.InducedCategory.category FiniteGrp.toGrp

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

Equations

• FiniteAddGrp.instCategory = CategoryTheory.InducedCategory.category FiniteAddGrp.toAddGrp

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

Equations

• FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp = CategoryTheory.InducedCategory.concreteCategory FiniteGrp.toGrp

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

Equations

• FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp = CategoryTheory.InducedCategory.concreteCategory FiniteAddGrp.toAddGrp

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

Equations

• G.instGroupCarrierToGrp = inferInstanceAs (Group ↑G.toGrp)

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

Equations

• G.instAddGroupCarrierToAddGrp = inferInstanceAs (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.

Equations

• FiniteGrp.of G = FiniteGrp.mk (Grp.of G)

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.

Equations

• FiniteAddGrp.of G = FiniteAddGrp.mk (AddGrp.of G)

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 Grp.

Equations

• FiniteGrp.ofHom f = Grp.ofHom f

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 AddGrp

Equations

• FiniteAddGrp.ofHom f = AddGrp.ofHom f

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