mathlib3 documentation

algebra.category.GroupWithZero

The category of groups with zero #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines GroupWithZero, the category of groups with zero.

def GroupWithZero :

Type (u_1+1)

The category of groups with zero.

Equations

GroupWithZero = category_theory.bundled group_with_zero

Instances for GroupWithZero

@[protected, instance]

def GroupWithZero.has_coe_to_sort :

has_coe_to_sort GroupWithZero (Type u_1)

Equations

GroupWithZero.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

@[protected, instance]

def GroupWithZero.group_with_zero (X : GroupWithZero) :

group_with_zero ↥X

Equations

X.group_with_zero = X.str

def GroupWithZero.of (α : Type u_1) [group_with_zero α] :

Construct a bundled GroupWithZero from a group_with_zero.

Equations

GroupWithZero.of α = category_theory.bundled.of α

@[protected, instance]

def GroupWithZero.inhabited :

inhabited GroupWithZero

Equations

GroupWithZero.inhabited = {default := GroupWithZero.of (with_zero punit) with_zero.group_with_zero}

@[protected, instance]

def GroupWithZero.category_theory.large_category :

category_theory.large_category GroupWithZero

Equations

GroupWithZero.category_theory.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : GroupWithZero), ↥X →*₀ ↥Y}, id := λ (X : GroupWithZero), monoid_with_zero_hom.id ↥X, comp := λ (X Y Z : GroupWithZero) (f : X ⟶ Y) (g : Y ⟶ Z), monoid_with_zero_hom.comp g f}, id_comp' := GroupWithZero.category_theory.large_category._proof_1, comp_id' := GroupWithZero.category_theory.large_category._proof_2, assoc' := GroupWithZero.category_theory.large_category._proof_3}

@[protected, instance]

def GroupWithZero.category_theory.concrete_category :

category_theory.concrete_category GroupWithZero

Equations

GroupWithZero.category_theory.concrete_category = category_theory.concrete_category.mk {obj := coe_sort GroupWithZero.has_coe_to_sort, map := λ (X Y : GroupWithZero), coe_fn, map_id' := GroupWithZero.category_theory.concrete_category._proof_1, map_comp' := GroupWithZero.category_theory.concrete_category._proof_2}

@[protected, instance]

def GroupWithZero.has_forget_to_Bipointed :

category_theory.has_forget₂ GroupWithZero Bipointed

Equations

GroupWithZero.has_forget_to_Bipointed = {forget₂ := {obj := λ (X : GroupWithZero), {X := ↥X, to_prod := (0, 1)}, map := λ (X Y : GroupWithZero) (f : X ⟶ Y), {to_fun := ⇑f, map_fst := _, map_snd := _}, map_id' := GroupWithZero.has_forget_to_Bipointed._proof_3, map_comp' := GroupWithZero.has_forget_to_Bipointed._proof_4}, forget_comp := GroupWithZero.has_forget_to_Bipointed._proof_5}

@[protected, instance]

def GroupWithZero.has_forget_to_Mon :

category_theory.has_forget₂ GroupWithZero Mon

Equations

GroupWithZero.has_forget_to_Mon = {forget₂ := {obj := λ (X : GroupWithZero), {α := ↥X, str := monoid_with_zero.to_monoid ↥X (group_with_zero.to_monoid_with_zero ↥X)}, map := λ (X Y : GroupWithZero), monoid_with_zero_hom.to_monoid_hom, map_id' := GroupWithZero.has_forget_to_Mon._proof_1, map_comp' := GroupWithZero.has_forget_to_Mon._proof_2}, forget_comp := GroupWithZero.has_forget_to_Mon._proof_3}

def GroupWithZero.iso.mk {α β : GroupWithZero} (e : ↥α ≃* ↥β) :

α ≅ β

Constructs an isomorphism of groups with zero from a group isomorphism between them.

Equations

GroupWithZero.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem GroupWithZero.iso.mk_inv {α β : GroupWithZero} (e : ↥α ≃* ↥β) :

(GroupWithZero.iso.mk e).inv = ↑(e.symm)

@[simp]

theorem GroupWithZero.iso.mk_hom {α β : GroupWithZero} (e : ↥α ≃* ↥β) :

(GroupWithZero.iso.mk e).hom = ↑e