mathlib docs: algebra.category.Group.basic

source

def AddGroup :

Type (u+1)

The category of additive groups and group morphisms

source

def Group :

Type (u+1)

The category of groups and group morphisms.

Equations

Group = category_theory.bundled group

source

@[instance]

def AddGroup.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection add_group.to_add_monoid

source

@[instance]

def Group.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection group.to_monoid

Equations

Group.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

def AddGroup.of (X : Type u) [add_group X] :

AddGroup

Construct a bundled AddGroup from the underlying type and typeclass.

source

def Group.of (X : Type u) [group X] :

Group

Construct a bundled Group from the underlying type and typeclass.

Equations

Group.of X = category_theory.bundled.of X

source

@[instance]

def Group.group (G : Group) :

group ↥G

Equations

G.group = G.str

source

@[instance]

def AddGroup.add_group (G : AddGroup) :

add_group ↥G

source

@[simp]

theorem AddGroup.coe_of (R : Type u) [add_group R] :

↥(AddGroup.of R) = R

source

@[simp]

theorem Group.coe_of (R : Type u) [group R] :

↥(Group.of R) = R

source

@[instance]

def Group.has_one :

has_one Group

Equations

Group.has_one = {one := Group.of punit (comm_group.to_group punit)}

source

@[instance]

def AddGroup.has_zero :

has_zero AddGroup

source

@[instance]

def AddGroup.inhabited :

inhabited AddGroup

source

@[instance]

def Group.inhabited :

inhabited Group

Equations

Group.inhabited = {default := 1}

source

@[instance]

def Group.unique :

unique ↥1

Equations

Group.unique = {to_inhabited := {default := 1}, uniq := Group.unique._proof_1}

source

@[instance]

def AddGroup.unique :

unique ↥0

source

@[simp]

theorem AddGroup.zero_apply (G H : AddGroup) (g : ↥G) :

⇑0 g = 0

source

@[simp]

theorem Group.one_apply (G H : Group) (g : ↥G) :

⇑1 g = 1

source

@[ext]

theorem Group.ext (G H : Group) (f₁ f₂ : G ⟶ H) (w : ∀ (x : ↥G), ⇑f₁ x = ⇑f₂ x) :

f₁ = f₂

source

@[ext]

theorem AddGroup.ext (G H : AddGroup) (f₁ f₂ : G ⟶ H) (w : ∀ (x : ↥G), ⇑f₁ x = ⇑f₂ x) :

f₁ = f₂

source

@[instance]

def Group.has_forget_to_Mon :

category_theory.has_forget₂ Group Mon

Equations

Group.has_forget_to_Mon = category_theory.bundled_hom.forget₂ monoid_hom group.to_monoid

source

@[instance]

def AddGroup.has_forget_to_AddMon :

category_theory.has_forget₂ AddGroup AddMon

source

def AddCommGroup :

Type (u+1)

The category of additive commutative groups and group morphisms.

source

def CommGroup :

Type (u+1)

The category of commutative groups and group morphisms.

Equations

CommGroup = category_theory.bundled comm_group

source

def Ab :

Type (u_1+1)

Ab is an abbreviation for AddCommGroup, for the sake of mathematicians' sanity.

source

@[instance]

def AddCommGroup.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection add_comm_group.to_add_group

source

@[instance]

def CommGroup.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection comm_group.to_group

Equations

CommGroup.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

def AddCommGroup.of (G : Type u) [add_comm_group G] :

AddCommGroup

Construct a bundled AddCommGroup from the underlying type and typeclass.

source

def CommGroup.of (G : Type u) [comm_group G] :

CommGroup

Construct a bundled CommGroup from the underlying type and typeclass.

Equations

CommGroup.of G = category_theory.bundled.of G

source

@[instance]

def CommGroup.comm_group_instance (G : CommGroup) :

comm_group ↥G

Equations

G.comm_group_instance = G.str

source

@[instance]

def AddCommGroup.add_comm_group_instance (G : AddCommGroup) :

add_comm_group ↥G

source

@[simp]

theorem AddCommGroup.coe_of (R : Type u) [add_comm_group R] :

↥(AddCommGroup.of R) = R

source

@[simp]

theorem CommGroup.coe_of (R : Type u) [comm_group R] :

↥(CommGroup.of R) = R

source

@[instance]

def AddCommGroup.has_zero :

has_zero AddCommGroup

source

@[instance]

def CommGroup.has_one :

has_one CommGroup

Equations

CommGroup.has_one = {one := CommGroup.of punit punit.comm_group}

source

@[instance]

def AddCommGroup.inhabited :

inhabited AddCommGroup

source

@[instance]

def CommGroup.inhabited :

inhabited CommGroup

Equations

CommGroup.inhabited = {default := 1}

source

@[instance]

def AddCommGroup.unique :

unique ↥0

source

@[instance]

def CommGroup.unique :

unique ↥1

Equations

CommGroup.unique = {to_inhabited := {default := 1}, uniq := CommGroup.unique._proof_1}

source

@[simp]

theorem CommGroup.one_apply (G H : CommGroup) (g : ↥G) :

⇑1 g = 1

source

@[simp]

theorem AddCommGroup.zero_apply (G H : AddCommGroup) (g : ↥G) :

⇑0 g = 0

source

@[ext]

theorem AddCommGroup.ext (G H : AddCommGroup) (f₁ f₂ : G ⟶ H) (w : ∀ (x : ↥G), ⇑f₁ x = ⇑f₂ x) :

f₁ = f₂

source

@[ext]

theorem CommGroup.ext (G H : CommGroup) (f₁ f₂ : G ⟶ H) (w : ∀ (x : ↥G), ⇑f₁ x = ⇑f₂ x) :

f₁ = f₂

source

@[instance]

def AddCommGroup.has_forget_to_AddGroup :

category_theory.has_forget₂ AddCommGroup AddGroup

source

@[instance]

def CommGroup.has_forget_to_Group :

category_theory.has_forget₂ CommGroup Group

Equations

CommGroup.has_forget_to_Group = category_theory.bundled_hom.forget₂ (category_theory.bundled_hom.map_hom monoid_hom group.to_monoid) comm_group.to_group

source

@[instance]

def CommGroup.has_forget_to_CommMon :

category_theory.has_forget₂ CommGroup CommMon

Equations

CommGroup.has_forget_to_CommMon = category_theory.induced_category.has_forget₂ (λ (G : CommGroup), CommMon.of ↥G)

source

@[instance]

def AddCommGroup.has_forget_to_AddCommMon :

category_theory.has_forget₂ AddCommGroup AddCommMon

source

def AddCommGroup.as_hom {G : AddCommGroup} (g : ↥G) :

AddCommGroup.of ℤ ⟶ G

Any element of an abelian group gives a unique morphism from ℤ sending 1 to that element.

Equations

AddCommGroup.as_hom g = ⇑(gmultiples_hom ↥G) g

source

@[simp]

theorem AddCommGroup.as_hom_apply {G : AddCommGroup} (g : ↥G) (i : ℤ) :

⇑(AddCommGroup.as_hom g) i = i • g

source

theorem AddCommGroup.as_hom_injective {G : AddCommGroup} :

function.injective AddCommGroup.as_hom

source

@[ext]

theorem AddCommGroup.int_hom_ext {G : AddCommGroup} (f g : AddCommGroup.of ℤ ⟶ G) (w : ⇑f 1 = ⇑g 1) :

f = g

source

theorem AddCommGroup.injective_of_mono {G H : AddCommGroup} (f : G ⟶ H) [category_theory.mono f] :

function.injective ⇑f

source

def mul_equiv.to_Group_iso {X Y : Type u} [group X] [group Y] (e : X ≃* Y) :

Group.of X ≅ Group.of Y

Build an isomorphism in the category Group from a mul_equiv between groups.

Equations

e.to_Group_iso = {hom := e.to_monoid_hom, inv := e.symm.to_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}

source

def add_equiv.to_AddGroup_iso {X Y : Type u} [add_group X] [add_group Y] (e : X ≃+ Y) :

AddGroup.of X ≅ AddGroup.of Y

Build an isomorphism in the category AddGroup from an add_equiv between add_groups.

source

def mul_equiv.to_CommGroup_iso {X Y : Type u} [comm_group X] [comm_group Y] (e : X ≃* Y) :

CommGroup.of X ≅ CommGroup.of Y

Build an isomorphism in the category CommGroup from a mul_equiv between comm_groups.

Equations

e.to_CommGroup_iso = {hom := e.to_monoid_hom, inv := e.symm.to_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}

source

def add_equiv.to_AddCommGroup_iso {X Y : Type u} [add_comm_group X] [add_comm_group Y] (e : X ≃+ Y) :

AddCommGroup.of X ≅ AddCommGroup.of Y

Build an isomorphism in the category AddCommGroup from a add_equiv between add_comm_groups.

source

def category_theory.iso.Group_iso_to_mul_equiv {X Y : Group} (i : X ≅ Y) :

↥X ≃* ↥Y

Build a mul_equiv from an isomorphism in the category Group.

Equations

i.Group_iso_to_mul_equiv = {to_fun := ⇑(i.hom), inv_fun := ⇑(i.inv), left_inv := _, right_inv := _, map_mul' := _}

source

def category_theory.iso.AddGroup_iso_to_add_equiv {X Y : AddGroup} (i : X ≅ Y) :

↥X ≃+ ↥Y

Build an add_equiv from an isomorphism in the category AddGroup.

source

def category_theory.iso.AddCommGroup_iso_to_add_equiv {X Y : AddCommGroup} (i : X ≅ Y) :

↥X ≃+ ↥Y

Build an add_equiv from an isomorphism in the category AddCommGroup.

source

def category_theory.iso.CommGroup_iso_to_mul_equiv {X Y : CommGroup} (i : X ≅ Y) :

↥X ≃* ↥Y

Build a mul_equiv from an isomorphism in the category CommGroup.

Equations

i.CommGroup_iso_to_mul_equiv = {to_fun := ⇑(i.hom), inv_fun := ⇑(i.inv), left_inv := _, right_inv := _, map_mul' := _}

source

def mul_equiv_iso_Group_iso {X Y : Type u} [group X] [group Y] :

X ≃* Y ≅ Group.of X ≅ Group.of Y

multiplicative equivalences between groups are the same as (isomorphic to) isomorphisms in Group

Equations

mul_equiv_iso_Group_iso = {hom := λ (e : X ≃* Y), e.to_Group_iso, inv := λ (i : Group.of X ≅ Group.of Y), i.Group_iso_to_mul_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

def add_equiv_iso_AddGroup_iso {X Y : Type u} [add_group X] [add_group Y] :

X ≃+ Y ≅ AddGroup.of X ≅ AddGroup.of Y

additive equivalences between add_groups are the same as (isomorphic to) isomorphisms in AddGroup

source

def add_equiv_iso_AddCommGroup_iso {X Y : Type u} [add_comm_group X] [add_comm_group Y] :

X ≃+ Y ≅ AddCommGroup.of X ≅ AddCommGroup.of Y

additive equivalences between add_comm_groups are the same as (isomorphic to) isomorphisms in AddCommGroup

source

def mul_equiv_iso_CommGroup_iso {X Y : Type u} [comm_group X] [comm_group Y] :

X ≃* Y ≅ CommGroup.of X ≅ CommGroup.of Y

multiplicative equivalences between comm_groups are the same as (isomorphic to) isomorphisms in CommGroup

Equations

mul_equiv_iso_CommGroup_iso = {hom := λ (e : X ≃* Y), e.to_CommGroup_iso, inv := λ (i : CommGroup.of X ≅ CommGroup.of Y), i.CommGroup_iso_to_mul_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

def category_theory.Aut.iso_perm {α : Type u} :

Group.of (category_theory.Aut α) ≅ Group.of (equiv.perm α)

The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group of permutations.

Equations

category_theory.Aut.iso_perm = {hom := {to_fun := λ (g : ↥(Group.of (category_theory.Aut α))), category_theory.iso.to_equiv g, map_one' := _, map_mul' := _}, inv := {to_fun := λ (g : ↥(Group.of (equiv.perm α))), equiv.to_iso g, map_one' := _, map_mul' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

def category_theory.Aut.mul_equiv_perm {α : Type u} :

category_theory.Aut α ≃* equiv.perm α

The (unbundled) group of automorphisms of a type is mul_equiv to the (unbundled) group of permutations.

Equations

category_theory.Aut.mul_equiv_perm = category_theory.Aut.iso_perm.Group_iso_to_mul_equiv

source

@[instance]

def Group.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget Group)

Equations

Group.forget_reflects_isos = {reflects := λ (X Y : Group) (f : X ⟶ Y) (_x : category_theory.is_iso ((category_theory.forget Group).map f)), let i : (category_theory.forget Group).obj X ≅ (category_theory.forget Group).obj Y := category_theory.as_iso ((category_theory.forget Group).map f), e : ↥X ≃* ↥Y := {to_fun := f.to_fun, inv_fun := i.to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _} in {inv := e.to_Group_iso.inv, hom_inv_id' := _, inv_hom_id' := _}}

source

@[instance]

def AddGroup.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddGroup)

source

@[instance]

def AddCommGroup.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddCommGroup)

source

@[instance]

def CommGroup.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget CommGroup)

Equations

CommGroup.forget_reflects_isos = {reflects := λ (X Y : CommGroup) (f : X ⟶ Y) (_x : category_theory.is_iso ((category_theory.forget CommGroup).map f)), let i : (category_theory.forget CommGroup).obj X ≅ (category_theory.forget CommGroup).obj Y := category_theory.as_iso ((category_theory.forget CommGroup).map f), e : ↥X ≃* ↥Y := {to_fun := f.to_fun, inv_fun := i.to_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _} in {inv := e.to_CommGroup_iso.inv, hom_inv_id' := _, inv_hom_id' := _}}

mathlib documentation

Category instances for group, add_group, comm_group, and add_comm_group.