Documentation

Mathlib.Algebra.Category.GrpWithZero

The category of groups with zero #

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

def GrpWithZero :

Type (u_1 + 1)

The category of groups with zero.

Equations

GrpWithZero = CategoryTheory.Bundled GroupWithZero

Instances For

instance GrpWithZero.instCoeSortType :

CoeSort GrpWithZero (Type u_1)

Equations

GrpWithZero.instCoeSortType = CategoryTheory.Bundled.coeSort

instance GrpWithZero.instGroupWithZeroα (X : GrpWithZero) :

GroupWithZero ↑X

Equations

X.instGroupWithZeroα = X.str

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

Construct a bundled GrpWithZero from a GroupWithZero.

Equations

GrpWithZero.of α = CategoryTheory.Bundled.of α

instance GrpWithZero.instInhabited :

Inhabited GrpWithZero

Equations

GrpWithZero.instInhabited = { default := GrpWithZero.of (WithZero PUnit.{?u.3 + 1} ) }

instance GrpWithZero.instLargeCategory :

CategoryTheory.LargeCategory GrpWithZero

Equations

GrpWithZero.instLargeCategory = CategoryTheory.Category.mk @GrpWithZero.instLargeCategory.proof_1 @GrpWithZero.instLargeCategory.proof_2 @GrpWithZero.instLargeCategory.proof_3

instance GrpWithZero.instFunLikeHomαGroupWithZero {M : GrpWithZero} {N : GrpWithZero} :

FunLike (M ⟶ N) ↑M ↑N

Equations

GrpWithZero.instFunLikeHomαGroupWithZero = { coe := fun (f : M ⟶ N) => (↑f).toFun, coe_injective' := ⋯ }

theorem GrpWithZero.coe_id {X : GrpWithZero} :

⇑(CategoryTheory.CategoryStruct.id X) = id

theorem GrpWithZero.coe_comp {X : GrpWithZero} {Y : GrpWithZero} {Z : GrpWithZero} {f : X ⟶ Y} {g : Y ⟶ Z} :

⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

instance GrpWithZero.groupWithZeroConcreteCategory :

CategoryTheory.ConcreteCategory GrpWithZero

Equations

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

@[simp]

theorem GrpWithZero.forget_map {X : GrpWithZero} {Y : GrpWithZero} (f : X ⟶ Y) :

(CategoryTheory.forget GrpWithZero).map f = ⇑f

instance GrpWithZero.hasForgetToBipointed :

CategoryTheory.HasForget₂ GrpWithZero Bipointed

Equations

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

instance GrpWithZero.hasForgetToMon :

CategoryTheory.HasForget₂ GrpWithZero MonCat

Equations

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

@[simp]

theorem GrpWithZero.Iso.mk_inv {α : GrpWithZero} {β : GrpWithZero} (e : ↑α ≃* ↑β) :

(GrpWithZero.Iso.mk e).inv = ↑e.symm

@[simp]

theorem GrpWithZero.Iso.mk_hom {α : GrpWithZero} {β : GrpWithZero} (e : ↑α ≃* ↑β) :

(GrpWithZero.Iso.mk e).hom = ↑e

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

α ≅ β

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

Equations

GrpWithZero.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }