Documentation

Mathlib.Algebra.Category.GrpWithZero

The category of groups with zero #

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

source
🔶 coverage
structure GrpWithZero :
Type (u_1 + 1)

The category of groups with zero.

Instances For
    source
    🔸 coverage
    instance GrpWithZero.instCoeSortType :
    CoeSort GrpWithZero (Type u_1)
    Equations
      source
      🔸 coverage
      instance GrpWithZero.instInhabited :
      Inhabited GrpWithZero
      Equations
        source
        🔸 coverage
        instance GrpWithZero.instLargeCategory :
        CategoryTheory.LargeCategory GrpWithZero
        Equations
          source
          🔸 coverage
          instance GrpWithZero.groupWithZeroConcreteCategory :
          CategoryTheory.ConcreteCategory GrpWithZero fun (x1 x2 : GrpWithZero) => x1.carrier →*₀ x2.carrier
          Equations
            source
            🔸 coverage
            @[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
              Instances For
                source
                📐 coverage
                @[simp]
                theorem GrpWithZero.hom_id {X : GrpWithZero} :
                CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X) = MonoidWithZeroHom.id X.carrier
                source
                📐 coverage
                @[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
                source
                📐 coverage
                theorem GrpWithZero.coe_id {X : GrpWithZero} :
                ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
                source
                📐 coverage
                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)
                source
                📐 coverage
                @[simp]
                theorem GrpWithZero.forget_map {X Y : GrpWithZero} (f : X ⟶ Y) :
                (CategoryTheory.forget GrpWithZero).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)
                source
                🔸 coverage
                instance GrpWithZero.hasForgetToBipointed :
                CategoryTheory.HasForget₂ GrpWithZero Bipointed
                Equations
                  source
                  🔸 coverage
                  instance GrpWithZero.hasForgetToMon :
                  CategoryTheory.HasForget₂ GrpWithZero MonCat
                  Equations
                    source
                    🔸 coverage
                    def GrpWithZero.Iso.mk {α β : GrpWithZero} (e : α.carrier ≃* β.carrier) :
                    α ≅ β

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

                    Equations
                      Instances For
                        source
                        📐 coverage
                        @[simp]
                        theorem GrpWithZero.Iso.mk_inv {α β : GrpWithZero} (e : α.carrier ≃* β.carrier) :
                        (mk e).inv = ofHom ↑e.symm
                        source
                        📐 coverage
                        @[simp]
                        theorem GrpWithZero.Iso.mk_hom {α β : GrpWithZero} (e : α.carrier ≃* β.carrier) :
                        (mk e).hom = ofHom ↑e