algebra.category.Group.basic

source

def AddGroup :

Type (u+1)

The category of additive groups and group morphisms

Equations

AddGroup = category_theory.bundled add_group

source

def Group :

Type (u+1)

The category of groups and group morphisms.

Equations

Group = category_theory.bundled group

source

@[protected, instance]

def AddGroup.group.to_monoid.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection add_group.to_add_monoid

Equations

AddGroup.group.to_monoid.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def Group.group.to_monoid.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection group.to_monoid

Equations

Group.group.to_monoid.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def Group.large_category :

category_theory.large_category Group

source

@[protected, instance]

def Group.concrete_category :

category_theory.concrete_category Group

source

@[protected, instance]

def AddGroup.concrete_category :

category_theory.concrete_category AddGroup

source

@[protected, instance]

def AddGroup.large_category :

category_theory.large_category AddGroup

source

@[protected, instance]

def AddGroup.has_coe_to_sort :

has_coe_to_sort AddGroup (Type u_1)

Equations

AddGroup.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

def Group.has_coe_to_sort :

has_coe_to_sort Group (Type u_1)

Equations

Group.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

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

AddGroup

Construct a bundled AddGroup from the underlying type and typeclass.

Equations

AddGroup.of X = category_theory.bundled.of X

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

def AddGroup.of_hom {X Y : Type u} [add_group X] [add_group Y] (f : X →+ Y) :

AddGroup.of X ⟶ AddGroup.of Y

Typecheck a add_monoid_hom as a morphism in AddGroup.

Equations

AddGroup.of_hom f = f

source

def Group.of_hom {X Y : Type u} [group X] [group Y] (f : X →* Y) :

Group.of X ⟶ Group.of Y

Typecheck a monoid_hom as a morphism in Group.

Equations

Group.of_hom f = f

source

@[simp]

theorem AddGroup.of_hom_apply {X Y : Type u_1} [add_group X] [add_group Y] (f : X →+ Y) (x : X) :

⇑(AddGroup.of_hom f) x = ⇑f x

source

@[simp]

theorem Group.of_hom_apply {X Y : Type u_1} [group X] [group Y] (f : X →* Y) (x : X) :

⇑(Group.of_hom f) x = ⇑f x

source

@[protected, instance]

def Group.group (G : Group) :

group ↥G

Equations

G.group = G.str

source

@[protected, instance]

def AddGroup.add_group (G : AddGroup) :

add_group ↥G

Equations

G.add_group = G.str

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

@[protected, instance]

def Group.has_one :

has_one Group

Equations

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

source

@[protected, instance]

def AddGroup.has_zero :

has_zero AddGroup

Equations

AddGroup.has_zero = {zero := AddGroup.of punit (add_comm_group.to_add_group punit)}

source

@[protected, instance]

def AddGroup.inhabited :

inhabited AddGroup

Equations

AddGroup.inhabited = {default := 0}

source

@[protected, instance]

def Group.inhabited :

inhabited Group

Equations

Group.inhabited = {default := 1}

source

@[protected, instance]

def Group.one.unique :

unique ↥1

Equations

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

source

@[protected, instance]

def AddGroup.one.unique :

unique ↥0

Equations

AddGroup.one.unique = {to_inhabited := {default := 0}, uniq := AddGroup.one.unique._proof_1}

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

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

f₁ = f₂

source

@[protected, instance]

def Group.has_forget_to_Mon :

category_theory.has_forget₂ Group Mon

Equations

Group.has_forget_to_Mon = category_theory.bundled_hom.forget₂ Mon.assoc_monoid_hom group.to_monoid

source

@[protected, instance]

def AddGroup.has_forget_to_AddMon :

category_theory.has_forget₂ AddGroup AddMon

Equations

AddGroup.has_forget_to_AddMon = category_theory.bundled_hom.forget₂ AddMon.assoc_add_monoid_hom add_group.to_add_monoid

source

def AddCommGroup :

Type (u+1)

The category of additive commutative groups and group morphisms.

Equations

AddCommGroup = category_theory.bundled add_comm_group

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

@[protected, instance]

def AddCommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection add_comm_group.to_add_group

Equations

AddCommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def CommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection :

category_theory.bundled_hom.parent_projection comm_group.to_group

Equations

CommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk

source

@[protected, instance]

def CommGroup.large_category :

category_theory.large_category CommGroup

source

@[protected, instance]

def CommGroup.concrete_category :

category_theory.concrete_category CommGroup

source

@[protected, instance]

def AddCommGroup.large_category :

category_theory.large_category AddCommGroup

source

@[protected, instance]

def AddCommGroup.concrete_category :

category_theory.concrete_category AddCommGroup

source

@[protected, instance]

def AddCommGroup.has_coe_to_sort :

has_coe_to_sort AddCommGroup (Type u_1)

Equations

AddCommGroup.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

def CommGroup.has_coe_to_sort :

has_coe_to_sort CommGroup (Type u_1)

Equations

CommGroup.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

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

AddCommGroup

Construct a bundled AddCommGroup from the underlying type and typeclass.

Equations

AddCommGroup.of G = category_theory.bundled.of G

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

def CommGroup.of_hom {X Y : Type u} [comm_group X] [comm_group Y] (f : X →* Y) :

CommGroup.of X ⟶ CommGroup.of Y

Typecheck a monoid_hom as a morphism in CommGroup.

Equations

CommGroup.of_hom f = f

source

def AddCommGroup.of_hom {X Y : Type u} [add_comm_group X] [add_comm_group Y] (f : X →+ Y) :

AddCommGroup.of X ⟶ AddCommGroup.of Y

Typecheck a add_monoid_hom as a morphism in AddCommGroup.

Equations

AddCommGroup.of_hom f = f

source

@[simp]

theorem AddCommGroup.of_hom_apply {X Y : Type u_1} [add_comm_group X] [add_comm_group Y] (f : X →+ Y) (x : X) :

⇑(AddCommGroup.of_hom f) x = ⇑f x

source

@[simp]

theorem CommGroup.of_hom_apply {X Y : Type u_1} [comm_group X] [comm_group Y] (f : X →* Y) (x : X) :

⇑(CommGroup.of_hom f) x = ⇑f x

source

@[protected, instance]

def CommGroup.comm_group_instance (G : CommGroup) :

comm_group ↥G

Equations

G.comm_group_instance = G.str

source

@[protected, instance]

def AddCommGroup.add_comm_group_instance (G : AddCommGroup) :

add_comm_group ↥G

Equations

G.add_comm_group_instance = G.str

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

@[protected, instance]

def AddCommGroup.has_zero :

has_zero AddCommGroup

Equations

AddCommGroup.has_zero = {zero := AddCommGroup.of punit punit.add_comm_group}

source

@[protected, instance]

def CommGroup.has_one :

has_one CommGroup

Equations

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

source

@[protected, instance]

def AddCommGroup.inhabited :

inhabited AddCommGroup

Equations

AddCommGroup.inhabited = {default := 0}

source

@[protected, instance]

def CommGroup.inhabited :

inhabited CommGroup

Equations

CommGroup.inhabited = {default := 1}

source

@[protected, instance]

def CommGroup.one.unique :

unique ↥1

Equations

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

source

@[protected, instance]

def AddCommGroup.one.unique :

unique ↥0

Equations

AddCommGroup.one.unique = {to_inhabited := {default := 0}, uniq := AddCommGroup.one.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

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

@[protected, instance]

def AddCommGroup.has_forget_to_AddGroup :

category_theory.has_forget₂ AddCommGroup AddGroup

Equations

AddCommGroup.has_forget_to_AddGroup = category_theory.bundled_hom.forget₂ (category_theory.bundled_hom.map_hom AddMon.assoc_add_monoid_hom add_group.to_add_monoid) add_comm_group.to_add_group

source

@[protected, 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 Mon.assoc_monoid_hom group.to_monoid) comm_group.to_group

source

@[protected, 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

@[protected, instance]

def AddCommGroup.has_forget_to_AddCommMon :

category_theory.has_forget₂ AddCommGroup AddCommMon

Equations

AddCommGroup.has_forget_to_AddCommMon = category_theory.induced_category.has_forget₂ (λ (G : AddCommGroup), AddCommMon.of ↥G)

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 = ⇑(zmultiples_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 : Group} (e : ↥X ≃* ↥Y) :

X ≅ 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 : AddGroup} (e : ↥X ≃+ ↥Y) :

X ≅ Y

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

Equations

e.to_AddGroup_iso = {hom := e.to_add_monoid_hom, inv := e.symm.to_add_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem add_equiv.to_AddGroup_iso_hom {X Y : AddGroup} (e : ↥X ≃+ ↥Y) :

e.to_AddGroup_iso.hom = e.to_add_monoid_hom

source

@[simp]

theorem add_equiv.to_AddGroup_iso_neg {X Y : AddGroup} (e : ↥X ≃+ ↥Y) :

e.to_AddGroup_iso.inv = e.symm.to_add_monoid_hom

source

@[simp]

theorem mul_equiv.to_Group_iso_hom {X Y : Group} (e : ↥X ≃* ↥Y) :

e.to_Group_iso.hom = e.to_monoid_hom

source

@[simp]

theorem mul_equiv.to_Group_iso_inv {X Y : Group} (e : ↥X ≃* ↥Y) :

e.to_Group_iso.inv = e.symm.to_monoid_hom

source

@[simp]

theorem add_equiv.to_AddCommGroup_iso_neg {X Y : AddCommGroup} (e : ↥X ≃+ ↥Y) :

e.to_AddCommGroup_iso.inv = e.symm.to_add_monoid_hom

source

@[simp]

theorem mul_equiv.to_CommGroup_iso_hom {X Y : CommGroup} (e : ↥X ≃* ↥Y) :

e.to_CommGroup_iso.hom = e.to_monoid_hom

source

def mul_equiv.to_CommGroup_iso {X Y : CommGroup} (e : ↥X ≃* ↥Y) :

X ≅ 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 : AddCommGroup} (e : ↥X ≃+ ↥Y) :

X ≅ Y

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

Equations

e.to_AddCommGroup_iso = {hom := e.to_add_monoid_hom, inv := e.symm.to_add_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem mul_equiv.to_CommGroup_iso_inv {X Y : CommGroup} (e : ↥X ≃* ↥Y) :

e.to_CommGroup_iso.inv = e.symm.to_monoid_hom

source

@[simp]

theorem add_equiv.to_AddCommGroup_iso_hom {X Y : AddCommGroup} (e : ↥X ≃+ ↥Y) :

e.to_AddCommGroup_iso.hom = e.to_add_monoid_hom

source

@[simp]

theorem category_theory.iso.AddGroup_iso_to_add_equiv_symm_apply {X Y : AddGroup} (i : X ≅ Y) (ᾰ : ↥Y) :

⇑(i.AddGroup_iso_to_add_equiv.symm) ᾰ = ⇑(i.inv) ᾰ

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 = monoid_hom.to_mul_equiv i.hom i.inv _ _

source

@[simp]

theorem category_theory.iso.Group_iso_to_mul_equiv_apply {X Y : Group} (i : X ≅ Y) (ᾰ : ↥X) :

⇑(i.Group_iso_to_mul_equiv) ᾰ = ⇑(i.hom) ᾰ

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.

Equations

i.AddGroup_iso_to_add_equiv = add_monoid_hom.to_add_equiv i.hom i.inv _ _

source

@[simp]

theorem category_theory.iso.AddGroup_iso_to_add_equiv_apply {X Y : AddGroup} (i : X ≅ Y) (ᾰ : ↥X) :

⇑(i.AddGroup_iso_to_add_equiv) ᾰ = ⇑(i.hom) ᾰ

source

@[simp]

theorem category_theory.iso.Group_iso_to_mul_equiv_symm_apply {X Y : Group} (i : X ≅ Y) (ᾰ : ↥Y) :

⇑(i.Group_iso_to_mul_equiv.symm) ᾰ = ⇑(i.inv) ᾰ

source

@[simp]

theorem category_theory.iso.AddCommGroup_iso_to_add_equiv_apply {X Y : AddCommGroup} (i : X ≅ Y) (ᾰ : ↥X) :

⇑(i.AddCommGroup_iso_to_add_equiv) ᾰ = ⇑(i.hom) ᾰ

source

@[simp]

theorem category_theory.iso.CommGroup_iso_to_mul_equiv_symm_apply {X Y : CommGroup} (i : X ≅ Y) (ᾰ : ↥Y) :

⇑(i.CommGroup_iso_to_mul_equiv.symm) ᾰ = ⇑(i.inv) ᾰ

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.

Equations

i.AddCommGroup_iso_to_add_equiv = add_monoid_hom.to_add_equiv i.hom i.inv _ _

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 = monoid_hom.to_mul_equiv i.hom i.inv _ _

source

@[simp]

theorem category_theory.iso.AddCommGroup_iso_to_add_equiv_symm_apply {X Y : AddCommGroup} (i : X ≅ Y) (ᾰ : ↥Y) :

⇑(i.AddCommGroup_iso_to_add_equiv.symm) ᾰ = ⇑(i.inv) ᾰ

source

@[simp]

theorem category_theory.iso.CommGroup_iso_to_mul_equiv_apply {X Y : CommGroup} (i : X ≅ Y) (ᾰ : ↥X) :

⇑(i.CommGroup_iso_to_mul_equiv) ᾰ = ⇑(i.hom) ᾰ

source

def mul_equiv_iso_Group_iso {X Y : Group} :

↥X ≃* ↥Y ≅ X ≅ 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 : X ≅ Y), i.Group_iso_to_mul_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

def add_equiv_iso_AddGroup_iso {X Y : AddGroup} :

↥X ≃+ ↥Y ≅ X ≅ Y

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

Equations

add_equiv_iso_AddGroup_iso = {hom := λ (e : ↥X ≃+ ↥Y), e.to_AddGroup_iso, inv := λ (i : X ≅ Y), i.AddGroup_iso_to_add_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

def add_equiv_iso_AddCommGroup_iso {X Y : AddCommGroup} :

↥X ≃+ ↥Y ≅ X ≅ Y

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

Equations

add_equiv_iso_AddCommGroup_iso = {hom := λ (e : ↥X ≃+ ↥Y), e.to_AddCommGroup_iso, inv := λ (i : X ≅ Y), i.AddCommGroup_iso_to_add_equiv, hom_inv_id' := _, inv_hom_id' := _}

source

def mul_equiv_iso_CommGroup_iso {X Y : CommGroup} :

↥X ≃* ↥Y ≅ X ≅ 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 : X ≅ 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

@[protected, instance]

def Group.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget Group)

source

@[protected, instance]

def AddGroup.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddGroup)

source

@[protected, instance]

def AddCommGroup.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget AddCommGroup)

source

@[protected, instance]

def CommGroup.forget_reflects_isos :

category_theory.reflects_isomorphisms (category_theory.forget CommGroup)

mathlib documentation

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