The category of groups with zero #
This file defines GrpWithZero
, the category of groups with zero.
The category of groups with zero.
Equations
Instances For
Equations
- GrpWithZero.instCoeSortType = CategoryTheory.Bundled.coeSort
Equations
- X.instGroupWithZeroα = X.str
Equations
- GrpWithZero.instInhabited = { default := GrpWithZero.of (WithZero PUnit.{?u.3 + 1} ) }
theorem
GrpWithZero.coe_comp
{X : GrpWithZero}
{Y : GrpWithZero}
{Z : GrpWithZero}
{f : X ⟶ Y}
{g : Y ⟶ Z}
:
⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f
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
Equations
- One or more equations did not get rendered due to their size.
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
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 := ⋯ }