Category instances for group, add_group, comm_group, and add_comm_group. #
We introduce the bundled categories:
Group
AddGroup
CommGroup
AddCommGroup
along with the relevant forgetful functors between them, and to the bundled monoid categories.
The category of additive groups and group morphisms
Equations
Instances for AddGroup
The category of groups and group morphisms.
Equations
Equations
- AddGroup.group.to_monoid.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk
Equations
- Group.group.to_monoid.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk
Construct a bundled AddGroup
from the underlying type and typeclass.
Equations
Instances for ↥AddGroup.of
Typecheck a add_monoid_hom
as a morphism in AddGroup
.
Equations
- AddGroup.of_hom f = f
Typecheck a monoid_hom
as a morphism in Group
.
Equations
- Group.of_hom f = f
Equations
Equations
Equations
- AddGroup.of_unique G = i
Equations
- Group.of_unique G = i
Equations
Equations
The category of additive commutative groups and group morphisms.
Equations
Instances for AddCommGroup
- AddCommGroup.large_category
- AddCommGroup.concrete_category
- AddCommGroup.has_coe_to_sort
- AddCommGroup.inhabited
- AddCommGroup.has_forget_to_AddGroup
- AddCommGroup.Group.has_coe
- AddCommGroup.has_forget_to_AddCommMon
- AddCommGroup.CommMon.has_coe
- Ring.has_forget_to_AddCommGroup
- AddCommGroup.category_theory.preadditive
- Module.has_forget_to_AddCommGroup
- AddCommGroup.has_limits_of_size
- AddCommGroup.has_limits
- AddCommGroup.colimits.has_colimits_AddCommGroup
- AddCommGroup.category_theory.abelian
- AddCommGroup.category_theory.limits.has_binary_biproducts
- AddCommGroup.category_theory.limits.has_finite_biproducts
- AddCommGroup.has_zero_object
- AddCommGroup.well_powered_AddCommGroup
The category of commutative groups and group morphisms.
Equations
Instances for CommGroup
- CommGroup.large_category
- CommGroup.concrete_category
- CommGroup.has_coe_to_sort
- CommGroup.inhabited
- CommGroup.has_forget_to_Group
- CommGroup.Group.has_coe
- CommGroup.has_forget_to_CommMon
- CommGroup.CommMon.has_coe
- CommGroup.has_limits_of_size
- CommGroup.has_limits
- CommGroup.category_theory.limits.has_zero_object
Ab
is an abbreviation for AddCommGroup
, for the sake of mathematicians' sanity.
Equations
- AddCommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk
Equations
- CommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk
Construct a bundled AddCommGroup
from the underlying type and typeclass.
Equations
Instances for ↥AddCommGroup.of
Construct a bundled CommGroup
from the underlying type and typeclass.
Equations
Instances for ↥CommGroup.of
Typecheck a monoid_hom
as a morphism in CommGroup
.
Equations
- CommGroup.of_hom f = f
Typecheck a add_monoid_hom
as a morphism in AddCommGroup
.
Equations
- AddCommGroup.of_hom f = f
Equations
- G.comm_group_instance = G.str
Equations
Equations
Equations
Equations
- CommGroup.of_unique G = i
Equations
Equations
Equations
Equations
Equations
Equations
Equations
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
Build an isomorphism in the category Group
from a mul_equiv
between group
s.
Equations
- e.to_Group_iso = {hom := e.to_monoid_hom, inv := e.symm.to_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}
Build an isomorphism in the category AddGroup
from an add_equiv
between add_group
s.
Equations
- e.to_AddGroup_iso = {hom := e.to_add_monoid_hom, inv := e.symm.to_add_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}
Build an isomorphism in the category CommGroup
from a mul_equiv
between comm_group
s.
Equations
- e.to_CommGroup_iso = {hom := e.to_monoid_hom, inv := e.symm.to_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}
Build an isomorphism in the category AddCommGroup
from a add_equiv
between
add_comm_group
s.
Equations
- e.to_AddCommGroup_iso = {hom := e.to_add_monoid_hom, inv := e.symm.to_add_monoid_hom, hom_inv_id' := _, inv_hom_id' := _}
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 _ _
Build an add_equiv
from an isomorphism
in the category AddCommGroup
.
Equations
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 _ _
multiplicative equivalences between group
s 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' := _}
additive equivalences between add_group
s 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' := _}
additive equivalences between add_comm_group
s 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' := _}
multiplicative equivalences between comm_group
s 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' := _}
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' := _}
The (unbundled) group of automorphisms of a type is mul_equiv
to the (unbundled) group
of permutations.