The category of groups with zero

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

structure GrpWithZero : Type (u_1 + 1)

The category of groups with zero.

• of :: (
• carrier : Type u_1

  The underlying group with zero.

• str : GroupWithZero self.carrier
• )

instance GrpWithZero.instCoeSortType : CoeSort GrpWithZero (Type u_1)

Equations

• GrpWithZero.instCoeSortType = { coe := GrpWithZero.carrier }

instance GrpWithZero.instInhabited : Inhabited GrpWithZero

Equations

• GrpWithZero.instInhabited = { default := { carrier := WithZero PUnit.{?u.2 + 1}, str := WithZero.instGroupWithZero } }

instance GrpWithZero.instLargeCategory : CategoryTheory.LargeCategory GrpWithZero

Equations

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

instance GrpWithZero.groupWithZeroConcreteCategory : CategoryTheory.ConcreteCategory GrpWithZero fun (x1 x2 : GrpWithZero) => x1.carrier →*₀ x2.carrier

Equations

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

@[reducible, inline]

abbrev GrpWithZero.ofHom {X Y : Type u} [GroupWithZero X] [GroupWithZero Y] (f : X →*₀ Y) : { carrier := X, str := inst✝ } ⟶ { carrier := Y, str := inst✝¹ }

Typecheck a MonoidWithZeroHom as a morphism in GrpWithZero.

Equations

• GrpWithZero.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[simp]

theorem GrpWithZero.hom_id {X : GrpWithZero} : CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X) = MonoidWithZeroHom.id X.carrier

@[simp]

theorem GrpWithZero.hom_comp {X Y Z : GrpWithZero} {f : X ⟶ Y} {g : Y ⟶ Z} : CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g) = MonoidWithZeroHom.comp g f

theorem GrpWithZero.coe_id {X : GrpWithZero} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

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

@[simp]

theorem GrpWithZero.forget_map {X Y : GrpWithZero} (f : X ⟶ Y) : (CategoryTheory.forget GrpWithZero).map f = ⇑(CategoryTheory.ConcreteCategory.hom 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.

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

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

Equations

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

@[simp]

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

@[simp]

theorem GrpWithZero.Iso.mk_inv {α β : GrpWithZero} (e : α.carrier ≃* β.carrier) : (mk e).inv = ofHom ↑e.symm