Documentation

Mathlib.Algebra.Category.Grp.FiniteGrp

Main definitions and results #

source
🔶 coverage
structure FiniteGrp :
Type (u + 1)

The category of finite groups.

Instances For
    source
    🔶 coverage
    structure FiniteAddGrp :
    Type (u + 1)

    The category of finite additive groups.

    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance FiniteGrp.instCoeSortType :
      CoeSort FiniteGrp.{u} (Type u)
      source
      🔸 coverage
      @[implicit_reducible]
      instance FiniteAddGrp.instCoeSortType :
      CoeSort FiniteAddGrp.{u} (Type u)
      source
      🔸 coverage
      @[implicit_reducible]
      instance FiniteGrp.instCategory :
      CategoryTheory.Category.{u_1, u_1 + 1} FiniteGrp.{u_1}
      source
      🔸 coverage
      @[implicit_reducible]
      instance FiniteAddGrp.instCategory :
      CategoryTheory.Category.{u_1, u_1 + 1} FiniteAddGrp.{u_1}
      source
      🔸 coverage
      @[implicit_reducible]
      instance FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp :
      CategoryTheory.ConcreteCategory FiniteGrp.{u_1} fun (x1 x2 : FiniteGrp.{u_1}) => ↑x1.toGrp →* ↑x2.toGrp
      source
      🔸 coverage
      @[implicit_reducible]
      instance FiniteAddGrp.instConcreteCategoryAddMonoidHomCarrierToAddGrp :
      CategoryTheory.ConcreteCategory FiniteAddGrp.{u_1} fun (x1 x2 : FiniteAddGrp.{u_1}) => ↑x1.toAddGrp →+ ↑x2.toAddGrp
      source
      🔸 coverage
      @[implicit_reducible]
      instance FiniteGrp.instGroupCarrierToGrp (G : FiniteGrp.{u_1}) :
      Group ↑G.toGrp
      source
      🔸 coverage
      @[implicit_reducible]
      instance FiniteAddGrp.instAddGroupCarrierToAddGrp (G : FiniteAddGrp.{u_1}) :
      AddGroup ↑G.toAddGrp
      source
      📐 coverage
      instance FiniteGrp.instFiniteCarrierToGrp (G : FiniteGrp.{u_1}) :
      Finite ↑G.toGrp
      source
      📐 coverage
      instance FiniteAddGrp.instFiniteCarrierToAddGrp (G : FiniteAddGrp.{u_1}) :
      Finite ↑G.toAddGrp
      source
      🔸 coverage
      def FiniteGrp.of (G : Type u) [Group G] [Finite G] :
      FiniteGrp.{u}

      Construct a term of FiniteGrp from a type endowed with the structure of a finite group.

      Instances For
        source
        🔸 coverage
        def FiniteAddGrp.of (G : Type u) [AddGroup G] [Finite G] :
        FiniteAddGrp.{u}

        Construct a term of FiniteAddGrp from a type endowed with the structure of a finite additive group.

        Instances For
          source
          🔸 coverage
          def FiniteGrp.ofHom {X Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) :
          of X ⟶ of Y

          The morphism in FiniteGrp, induced from a morphism of the category GrpCat.

          Instances For
            source
            🔸 coverage
            def FiniteAddGrp.ofHom {X Y : Type u} [AddGroup X] [Finite X] [AddGroup Y] [Finite Y] (f : X →+ Y) :
            of X ⟶ of Y

            The morphism in FiniteAddGrp, induced from a morphism of the category AddGrpCat

            Instances For
              source
              📐 coverage
              theorem FiniteGrp.ofHom_apply {X Y : Type u} [Group X] [Finite X] [Group Y] [Finite Y] (f : X →* Y) (x : X) :
              (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x
              source
              📐 coverage
              theorem FiniteAddGrp.ofHom_apply {X Y : Type u} [AddGroup X] [Finite X] [AddGroup Y] [Finite Y] (f : X →+ Y) (x : X) :
              (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x