The category of groups with zero

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

def GroupWithZeroCat : Type (u_1 + 1)

The category of groups with zero.

Equations

• GroupWithZeroCat = CategoryTheory.Bundled GroupWithZero

instance GroupWithZeroCat.instCoeSortGroupWithZeroCatType : CoeSort GroupWithZeroCat (Type u_1)

Equations

• GroupWithZeroCat.instCoeSortGroupWithZeroCatType = CategoryTheory.Bundled.coeSort

instance GroupWithZeroCat.instGroupWithZeroα (X : GroupWithZeroCat) : GroupWithZero ↑X

Equations

• GroupWithZeroCat.instGroupWithZeroα X = X.str

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

Construct a bundled GroupWithZeroCat from a GroupWithZero.

Equations

• GroupWithZeroCat.of α = CategoryTheory.Bundled.of α

instance GroupWithZeroCat.instInhabitedGroupWithZeroCat : Inhabited GroupWithZeroCat

Equations

• GroupWithZeroCat.instInhabitedGroupWithZeroCat = { default := GroupWithZeroCat.of (WithZero PUnit.{u_1 + 1} ) }

instance GroupWithZeroCat.instLargeCategoryGroupWithZeroCat : CategoryTheory.LargeCategory GroupWithZeroCat

Equations

• One or more equations did not get rendered due to their size.

instance GroupWithZeroCat.instFunLikeHomGroupWithZeroCatToQuiverToCategoryStructInstLargeCategoryGroupWithZeroCatαGroupWithZero {M : GroupWithZeroCat} {N : GroupWithZeroCat} : FunLike (M ⟶ N) ↑M ↑N

Equations

• GroupWithZeroCat.instFunLikeHomGroupWithZeroCatToQuiverToCategoryStructInstLargeCategoryGroupWithZeroCatαGroupWithZero = { coe := fun (f : M ⟶ N) => f.toFun, coe_injective' := ⋯ }

theorem GroupWithZeroCat.coe_id {X : GroupWithZeroCat} : ⇑(CategoryTheory.CategoryStruct.id X) = id

theorem GroupWithZeroCat.coe_comp {X : GroupWithZeroCat} {Y : GroupWithZeroCat} {Z : GroupWithZeroCat} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

instance GroupWithZeroCat.groupWithZeroConcreteCategory : CategoryTheory.ConcreteCategory GroupWithZeroCat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GroupWithZeroCat.forget_map {X : GroupWithZeroCat} {Y : GroupWithZeroCat} (f : X ⟶ Y) : (CategoryTheory.forget GroupWithZeroCat).map f = ⇑f

instance GroupWithZeroCat.hasForgetToBipointed : CategoryTheory.HasForget₂ GroupWithZeroCat Bipointed

Equations

• One or more equations did not get rendered due to their size.

instance GroupWithZeroCat.hasForgetToMon : CategoryTheory.HasForget₂ GroupWithZeroCat MonCat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GroupWithZeroCat.Iso.mk_hom {α : GroupWithZeroCat} {β : GroupWithZeroCat} (e : ↑α ≃* ↑β) : (GroupWithZeroCat.Iso.mk e).hom = ↑e

@[simp]

theorem GroupWithZeroCat.Iso.mk_inv {α : GroupWithZeroCat} {β : GroupWithZeroCat} (e : ↑α ≃* ↑β) : (GroupWithZeroCat.Iso.mk e).inv = ↑(MulEquiv.symm e)

def GroupWithZeroCat.Iso.mk {α : GroupWithZeroCat} {β : GroupWithZeroCat} (e : ↑α ≃* ↑β) : α ≅ β

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

Equations

• GroupWithZeroCat.Iso.mk e = { hom := ↑e, inv := ↑(MulEquiv.symm e), hom_inv_id := ⋯, inv_hom_id := ⋯ }