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

theorem FiniteGrp.isFinite (self : FiniteGrp.{u_1}) :

Finite ↑self.toGrp

source

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

source

theorem FiniteAddGrp.isFinite (self : FiniteAddGrp.{u_1}) :

Finite ↑self.toAddGrp

source

instance FiniteGrp.instCoeSortType :

CoeSort FiniteGrp.{u} (Type u)

Equations

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

source

instance FiniteAddGrp.instCoeSortType :

CoeSort FiniteAddGrp.{u} (Type u)

Equations

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

source

instance FiniteGrp.instCategory :

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

Equations

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

source

instance FiniteAddGrp.instCategory :

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

Equations

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

source

instance FiniteGrp.instConcreteCategory :

CategoryTheory.ConcreteCategory FiniteGrp.{u_1}

Equations

FiniteGrp.instConcreteCategory = CategoryTheory.InducedCategory.concreteCategory FiniteGrp.toGrp

source

instance FiniteAddGrp.instConcreteCategory :

CategoryTheory.ConcreteCategory FiniteAddGrp.{u_1}

Equations

FiniteAddGrp.instConcreteCategory = CategoryTheory.InducedCategory.concreteCategory FiniteAddGrp.toAddGrp

source

instance FiniteGrp.instGroupαToGrp (G : FiniteGrp.{u_1}) :

Group ↑G.toGrp

Equations

G.instGroupαToGrp = inferInstanceAs (Group ↑G.toGrp)

source

instance FiniteAddGrp.instGroupαToAddGrp (G : FiniteAddGrp.{u_1}) :

AddGroup ↑G.toAddGrp

Equations

G.instGroupαToAddGrp = inferInstanceAs (AddGroup ↑G.toAddGrp)

source

instance FiniteGrp.instFiniteαGroupToGrp (G : FiniteGrp.{u_1}) :

Finite ↑G.toGrp

Equations

⋯ = ⋯

source

instance FiniteAddGrp.instFiniteαAddGroupToAddGrp (G : FiniteAddGrp.{u_1}) :

Finite ↑G.toAddGrp

Equations

⋯ = ⋯

source

instance FiniteGrp.instFunLikeHomαGroupToGrp (G : FiniteGrp.{u_1}) (H : FiniteGrp.{u_1}) :

FunLike (G ⟶ H) ↑G.toGrp ↑H.toGrp

Equations

G.instFunLikeHomαGroupToGrp H = inferInstanceAs (FunLike (↑G.toGrp →* ↑H.toGrp) ↑G.toGrp ↑H.toGrp)

source

instance FiniteAddGrp.instFunLikeHomαAddGroupToAddGrp (G : FiniteAddGrp.{u_1}) (H : FiniteAddGrp.{u_1}) :

FunLike (G ⟶ H) ↑G.toAddGrp ↑H.toAddGrp

Equations

G.instFunLikeHomαAddGroupToAddGrp H = inferInstanceAs (FunLike (↑G.toAddGrp →+ ↑H.toAddGrp) ↑G.toAddGrp ↑H.toAddGrp)

source

instance FiniteGrp.instMonoidHomClassHomαGroupToGrp (G : FiniteGrp.{u_1}) (H : FiniteGrp.{u_1}) :

MonoidHomClass (G ⟶ H) ↑G.toGrp ↑H.toGrp

Equations

⋯ = ⋯

source

instance FiniteAddGrp.instAddMonoidHomClassHomαAddGroupToAddGrp (G : FiniteAddGrp.{u_1}) (H : FiniteAddGrp.{u_1}) :

AddMonoidHomClass (G ⟶ H) ↑G.toAddGrp ↑H.toAddGrp

Equations

⋯ = ⋯

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

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

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

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

Instances For

source

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

FiniteGrp.of X ⟶ FiniteGrp.of Y

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

Equations

FiniteGrp.ofHom f = Grp.ofHom f

Instances For

source

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

FiniteAddGrp.of X ⟶ FiniteAddGrp.of Y

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

Equations

FiniteAddGrp.ofHom f = AddGrp.ofHom f

Instances For

source

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

source

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

(FiniteAddGrp.ofHom f) x = f x