Documentation

Mathlib.Algebra.Category.GroupWithZeroCat

The category of groups with zero #

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

source
def GroupWithZeroCat :
Type (u_1 + 1)

The category of groups with zero.

Instances For
    source
    instance GroupWithZeroCat.instCoeSortGroupWithZeroCatType :
    CoeSort GroupWithZeroCat (Type u_1)
    source
    instance GroupWithZeroCat.instGroupWithZeroα (X : GroupWithZeroCat) :
    GroupWithZero ↑X
    source
    def GroupWithZeroCat.of (α : Type u_1) [GroupWithZero α] :
    GroupWithZeroCat

    Construct a bundled GroupWithZeroCat from a GroupWithZero.

    Instances For
      source
      instance GroupWithZeroCat.instInhabitedGroupWithZeroCat :
      Inhabited GroupWithZeroCat
      source
      instance GroupWithZeroCat.instLargeCategoryGroupWithZeroCat :
      CategoryTheory.LargeCategory GroupWithZeroCat
      source
      instance GroupWithZeroCat.instFunLikeHomGroupWithZeroCatToQuiverToCategoryStructInstLargeCategoryGroupWithZeroCatαGroupWithZero {M : GroupWithZeroCat} {N : GroupWithZeroCat} :
      FunLike (M ⟶ N) ↑M fun x => ↑N
      source
      theorem GroupWithZeroCat.coe_id {X : GroupWithZeroCat} :
      ↑(CategoryTheory.CategoryStruct.id X) = id
      source
      theorem GroupWithZeroCat.coe_comp {X : GroupWithZeroCat} {Y : GroupWithZeroCat} {Z : GroupWithZeroCat} {f : X ⟶ Y} {g : Y ⟶ Z} :
      ↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f
      source
      instance GroupWithZeroCat.groupWithZeroConcreteCategory :
      CategoryTheory.ConcreteCategory GroupWithZeroCat
      source
      @[simp]
      theorem GroupWithZeroCat.forget_map {X : GroupWithZeroCat} {Y : GroupWithZeroCat} (f : X ⟶ Y) :
      (CategoryTheory.forget GroupWithZeroCat).map f = ↑f
      source
      instance GroupWithZeroCat.hasForgetToBipointed :
      CategoryTheory.HasForget₂ GroupWithZeroCat Bipointed
      source
      instance GroupWithZeroCat.hasForgetToMon :
      CategoryTheory.HasForget₂ GroupWithZeroCat MonCat
      source
      instance GroupWithZeroCat.instCoeFunHomGroupWithZeroCatToQuiverToCategoryStructInstLargeCategoryGroupWithZeroCatForAllαGroupWithZero {X : GroupWithZeroCat} {Y : GroupWithZeroCat} :
      CoeFun (X ⟶ Y) fun x => ↑X → ↑Y
      source
      @[simp]
      theorem GroupWithZeroCat.Iso.mk_hom {α : GroupWithZeroCat} {β : GroupWithZeroCat} (e : ↑α ≃* ↑β) :
      (GroupWithZeroCat.Iso.mk e).hom = ↑e
      source
      @[simp]
      theorem GroupWithZeroCat.Iso.mk_inv {α : GroupWithZeroCat} {β : GroupWithZeroCat} (e : ↑α ≃* ↑β) :
      (GroupWithZeroCat.Iso.mk e).inv = ↑(MulEquiv.symm e)
      source
      def GroupWithZeroCat.Iso.mk {α : GroupWithZeroCat} {β : GroupWithZeroCat} (e : ↑α ≃* ↑β) :
      α ≅ β

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

      Instances For