Mathlib.Algebra.Category.Grp.FiniteGrp

Main definitions and results #

FiniteGrp is the category of finite groups.

source

structure FiniteGrp :

Type (u_1 + 1)

The category of finite groups.

toGrp : Grp
A group that is finite
isFinite : Finite ↑self.toGrp

Instances For

source

structure FiniteAddGrp :

Type (u_1 + 1)

The category of finite additive groups.

toAddGrp : AddGrp
An additive group that is finite
isFinite : Finite ↑self.toAddGrp

Instances For

source

instance FiniteGrp.instCoeSortType :

CoeSort FiniteGrp.{u} (Type u)

Equations

source

instance FiniteAddGrp.instCoeSortType :

CoeSort FiniteAddGrp.{u} (Type u)

Equations

source

instance FiniteGrp.instCategory :

CategoryTheory.Category.{u_1, u_1 + 1} FiniteGrp.{u_1}

Equations

source

instance FiniteAddGrp.instCategory :

CategoryTheory.Category.{u_1, u_1 + 1} FiniteAddGrp.{u_1}

Equations

source

instance FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp :

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

Equations

source

instance FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp :

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

Equations

source

instance FiniteGrp.instGroupCarrierToGrp (G : FiniteGrp.{u_1}) :

Group ↑G.toGrp

Equations

source

instance FiniteAddGrp.instAddGroupCarrierToAddGrp (G : FiniteAddGrp.{u_1}) :

AddGroup ↑G.toAddGrp

Equations

source

instance FiniteGrp.instFiniteCarrierToGrp (G : FiniteGrp.{u_1}) :

Finite ↑G.toGrp

source

instance FiniteAddGrp.instFiniteCarrierToAddGrp (G : FiniteAddGrp.{u_1}) :

Finite ↑G.toAddGrp

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

source

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