Documentation

Mathlib.Algebra.Category.Grp.ForgetCorepresentable

The forget functor is corepresentable #

It is shown that the forget functor AddCommGrpCat.{u} ⥤ Type u is corepresentable by ULift ℤ. Similar results are obtained for the variants CommGrpCat, AddGrpCat and GrpCat.

(ULift ℤ →+ G) ≃ G #

These universe-monomorphic variants of zmultiplesHom/zpowersHom are put here since they shouldn't be useful outside of category theory.

source
def uliftZMultiplesHom (G : Type u) [AddGroup G] :
G ≃ (ULift.{u, 0} ℤ →+ G)

The equivalence (ULift ℤ →+ G) ≃ G for any additive group G.

Equations
Instances For
    source
    @[simp]
    theorem uliftZMultiplesHom_apply_apply (G : Type u) [AddGroup G] (a✝ : G) (x : ULift.{u, 0} ℤ) :
    ((uliftZMultiplesHom G) a✝) x = AddEquiv.ulift x • a✝
    source
    @[simp]
    theorem uliftZMultiplesHom_symm_apply (G : Type u) [AddGroup G] (a✝ : ULift.{u, 0} ℤ →+ G) :
    (uliftZMultiplesHom G).symm a✝ = a✝ (AddEquiv.ulift.symm 1)
    source
    def uliftZPowersHom (G : Type u) [Group G] :
    G ≃ (ULift.{u, 0} (Multiplicative ℤ) →* G)

    The equivalence (ULift (Multiplicative ℤ) →* G) ≃ G for any group G.

    Equations
    Instances For
      source
      @[simp]
      theorem uliftZPowersHom_apply_apply (G : Type u) [Group G] (a✝ : G) (x : ULift.{u, 0} (Multiplicative ℤ)) :
      ((uliftZPowersHom G) a✝) x = a✝ ^ Multiplicative.toAdd (MulEquiv.ulift x)
      source
      @[simp]
      theorem uliftZPowersHom_symm_apply (G : Type u) [Group G] (a✝ : ULift.{u, 0} (Multiplicative ℤ) →* G) :
      (uliftZPowersHom G).symm a✝ = a✝ (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))
      source
      def GrpCat.coyonedaObjIsoForget :
      CategoryTheory.coyoneda.obj (Opposite.op ↧(ULift.{u, 0} (Multiplicative ℤ))) ≅ CategoryTheory.forget GrpCat

      The forget functor GrpCat.{u} ⥤ Type u is corepresentable.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CommGrpCat.coyonedaObjIsoForget :
        CategoryTheory.coyoneda.obj (Opposite.op ↧(ULift.{u, 0} (Multiplicative ℤ))) ≅ CategoryTheory.forget CommGrpCat

        The forget functor CommGrpCat.{u} ⥤ Type u is corepresentable.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def AddGrpCat.coyonedaObjIsoForget :
          CategoryTheory.coyoneda.obj (Opposite.op ↧(ULift.{u, 0} ℤ)) ≅ CategoryTheory.forget AddGrpCat

          The forget functor AddGrpCat.{u} ⥤ Type u is corepresentable.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def AddCommGrpCat.coyonedaObjIsoForget :
            CategoryTheory.coyoneda.obj (Opposite.op ↧(ULift.{u, 0} ℤ)) ≅ CategoryTheory.forget AddCommGrpCat

            The forget functor AddCommGrpCat.{u} ⥤ Type u is corepresentable.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance GrpCat.forget_isCorepresentable :
              (CategoryTheory.forget GrpCat).IsCorepresentable
              source
              instance CommGrpCat.forget_isCorepresentable :
              (CategoryTheory.forget CommGrpCat).IsCorepresentable
              source
              instance AddGrpCat.forget_isCorepresentable :
              (CategoryTheory.forget AddGrpCat).IsCorepresentable
              source
              instance AddCommGrpCat.forget_isCorepresentable :
              (CategoryTheory.forget AddCommGrpCat).IsCorepresentable
              source
              theorem uliftZMultiplesHom_apply_add (G : Type u) [AddCommGroup G] (x y : G) :
              (uliftZMultiplesHom G) (x + y) = (uliftZMultiplesHom G) x + (uliftZMultiplesHom G) y
              source
              def AddCommGrpCat.uliftZMultiplesAddEquiv (G : AddCommGrpCat) :
              (↧(ULift.{u_1, 0} ℤ) ⟶ G) ≃+ ↑G

              The additive equivalence (ℤ ⟶ G) ≃+ G

              Equations
              Instances For
                source
                @[simp]
                theorem AddCommGrpCat.uliftZMultiplesAddEquiv_symm_apply_hom_apply (G : AddCommGrpCat) (a✝ : ↑G) (x : ULift.{u_1, 0} ℤ) :
                (Hom.hom (G.uliftZMultiplesAddEquiv.symm a✝)) x = AddEquiv.ulift x • a✝
                source
                @[simp]
                theorem AddCommGrpCat.uliftZMultiplesAddEquiv_apply (G : AddCommGrpCat) (a✝ : ↧(ULift.{u_1, 0} ℤ) ⟶ G) :
                G.uliftZMultiplesAddEquiv a✝ = (AddEquiv.mk' (uliftZMultiplesHom ↑G) ⋯).symm (homAddEquiv a✝)