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
Instances For
    Equations
    Equations
    • X.instGroupWithZeroα = X.str

    Construct a bundled GrpWithZero from a GroupWithZero.

    Equations
    Instances For
      Equations
      • GrpWithZero.instFunLikeHomαGroupWithZero = { coe := fun (f : M N) => (↑f).toFun, coe_injective' := }
      theorem GrpWithZero.coe_comp {X : GrpWithZero} {Y : GrpWithZero} {Z : GrpWithZero} {f : X Y} {g : Y Z} :
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      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
      def GrpWithZero.Iso.mk {α : GrpWithZero} {β : GrpWithZero} (e : α ≃* β) :
      α β

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

      Equations
      Instances For