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.

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

    Construct a bundled GroupWithZeroCat from a GroupWithZero.

    Equations
    Instances For
      source
      instance GroupWithZeroCat.instInhabitedGroupWithZeroCat :
      Inhabited GroupWithZeroCat
      Equations
      source
      instance GroupWithZeroCat.instLargeCategoryGroupWithZeroCat :
      CategoryTheory.LargeCategory GroupWithZeroCat
      Equations
      source
      instance GroupWithZeroCat.instFunLikeHomGroupWithZeroCatToQuiverToCategoryStructInstLargeCategoryGroupWithZeroCatαGroupWithZero {M : GroupWithZeroCat} {N : GroupWithZeroCat} :
      FunLike (M ⟶ N) ↑M ↑N
      Equations
      • One or more equations did not get rendered due to their size.
      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
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem GroupWithZeroCat.forget_map {X : GroupWithZeroCat} {Y : GroupWithZeroCat} (f : X ⟶ Y) :
      (CategoryTheory.forget GroupWithZeroCat).toPrefunctor.map f = ⇑f
      source
      instance GroupWithZeroCat.hasForgetToBipointed :
      CategoryTheory.HasForget₂ GroupWithZeroCat Bipointed
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance GroupWithZeroCat.hasForgetToMon :
      CategoryTheory.HasForget₂ GroupWithZeroCat MonCat
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance GroupWithZeroCat.instCoeFunHomGroupWithZeroCatToQuiverToCategoryStructInstLargeCategoryGroupWithZeroCatForAllαGroupWithZero {X : GroupWithZeroCat} {Y : GroupWithZeroCat} :
      CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ↑X → ↑Y
      Equations
      • GroupWithZeroCat.instCoeFunHomGroupWithZeroCatToQuiverToCategoryStructInstLargeCategoryGroupWithZeroCatForAllαGroupWithZero = { coe := fun (f : ↑X →*₀ ↑Y) => ⇑f }
      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.

      Equations
      Instances For