Documentation

Mathlib.Algebra.Category.AlgebraCat.Basic

Category instance for algebras over a commutative ring #

We introduce the bundled category AlgebraCat of algebras over a fixed commutative ring R along with the forgetful functors to RingCat and ModuleCat. We furthermore show that the functor associating to a type the free R-algebra on that type is left adjoint to the forgetful functor.

structure AlgebraCat (R : Type u) [CommRing R] :
Type (max u (v + 1))

The category of R-algebras and their morphisms.

Instances For
    @[reducible, inline]
    abbrev AlgebraCatMax (R : Type u₁) [CommRing R] :
    Type (max u₁ ((max v₁ v₂) + 1))

    An alias for AlgebraCat.{max u₁ u₂}, to deal around unification issues. Since the universe the ring lives in can be inferred, we put that last.

    Equations
    Instances For
      Equations
      instance AlgebraCat.instFunLikeHomCarrier (R : Type u) [CommRing R] {M : AlgebraCat R} {N : AlgebraCat R} :
      FunLike (M N) M N
      Equations
      instance AlgebraCat.instAlgHomClassHomCarrier (R : Type u) [CommRing R] {M : AlgebraCat R} {N : AlgebraCat R} :
      AlgHomClass (M N) R M N
      Equations
      • =
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      def AlgebraCat.of (R : Type u) [CommRing R] (X : Type v) [Ring X] [Algebra R X] :

      The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.

      Equations
      Instances For
        def AlgebraCat.ofHom {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y] (f : X →ₐ[R] Y) :

        Typecheck a AlgHom as a morphism in AlgebraCat R.

        Equations
        Instances For
          @[simp]
          theorem AlgebraCat.ofHom_apply {R : Type u} [CommRing R] {X : Type v} {Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y] (f : X →ₐ[R] Y) (x : X) :
          @[simp]
          theorem AlgebraCat.coe_of (R : Type u) [CommRing R] (X : Type u) [Ring X] [Algebra R X] :
          (AlgebraCat.of R X) = X
          @[simp]
          @[simp]
          def AlgebraCat.ofSelfIso {R : Type u} [CommRing R] (M : AlgebraCat R) :

          Forgetting to the underlying type and then building the bundled object returns the original algebra.

          Equations
          Instances For
            @[simp]
            theorem AlgebraCat.id_apply {R : Type u} [CommRing R] {M : ModuleCat R} (m : M) :
            @[simp]
            theorem AlgebraCat.coe_comp {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {U : ModuleCat R} (f : M N) (g : N U) :
            @[simp]
            theorem AlgebraCat.free_map (R : Type u) [CommRing R] :
            ∀ {X Y : Type u} (f : X Y), (AlgebraCat.free R).map f = (FreeAlgebra.lift R) (FreeAlgebra.ι R f)
            @[simp]
            theorem AlgebraCat.free_obj_carrier (R : Type u) [CommRing R] (S : Type u) :
            ((AlgebraCat.free R).obj S) = FreeAlgebra R S

            The "free algebra" functor, sending a type S to the free algebra on S.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              The free/forget adjunction for R-algebras.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • =
                @[simp]
                theorem AlgEquiv.toAlgebraIso_hom {R : Type u} [CommRing R] {X₁ : Type u} {X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
                e.toAlgebraIso.hom = e
                @[simp]
                theorem AlgEquiv.toAlgebraIso_inv {R : Type u} [CommRing R] {X₁ : Type u} {X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
                e.toAlgebraIso.inv = e.symm
                def AlgEquiv.toAlgebraIso {R : Type u} [CommRing R] {X₁ : Type u} {X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :

                Build an isomorphism in the category AlgebraCat R from a AlgEquiv between Algebras.

                Equations
                • e.toAlgebraIso = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
                Instances For
                  @[simp]
                  theorem CategoryTheory.Iso.toAlgEquiv_apply {R : Type u} [CommRing R] {X : AlgebraCat R} {Y : AlgebraCat R} (i : X Y) (a : X) :
                  i.toAlgEquiv a = i.hom a
                  @[simp]
                  theorem CategoryTheory.Iso.toAlgEquiv_symm_apply {R : Type u} [CommRing R] {X : AlgebraCat R} {Y : AlgebraCat R} (i : X Y) (a : Y) :
                  i.toAlgEquiv.symm a = i.inv a
                  def CategoryTheory.Iso.toAlgEquiv {R : Type u} [CommRing R] {X : AlgebraCat R} {Y : AlgebraCat R} (i : X Y) :
                  X ≃ₐ[R] Y

                  Build a AlgEquiv from an isomorphism in the category AlgebraCat R.

                  Equations
                  • i.toAlgEquiv = let __src := i.hom; { toFun := i.hom, invFun := i.inv, left_inv := , right_inv := , map_mul' := , map_add' := , commutes' := }
                  Instances For
                    @[simp]
                    theorem algEquivIsoAlgebraIso_hom {R : Type u} [CommRing R] {X : Type u} {Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] (e : X ≃ₐ[R] Y) :
                    algEquivIsoAlgebraIso.hom e = e.toAlgebraIso
                    @[simp]
                    theorem algEquivIsoAlgebraIso_inv {R : Type u} [CommRing R] {X : Type u} {Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] (i : AlgebraCat.of R X AlgebraCat.of R Y) :
                    algEquivIsoAlgebraIso.inv i = i.toAlgEquiv
                    def algEquivIsoAlgebraIso {R : Type u} [CommRing R] {X : Type u} {Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] :

                    Algebra equivalences between Algebras are the same as (isomorphic to) isomorphisms in AlgebraCat.

                    Equations
                    Instances For
                      instance AlgebraCat.forget_reflects_isos {R : Type u} [CommRing R] :
                      (CategoryTheory.forget (AlgebraCat R)).ReflectsIsomorphisms
                      Equations
                      • =

                      @[simp] lemmas for AlgHom.comp and categorical identities.

                      @[simp]
                      theorem AlgHom.comp_id_algebraCat {R : Type u_1} [CommRing R] {G : AlgebraCat R} {H : Type u} [Ring H] [Algebra R H] (f : G →ₐ[R] H) :
                      @[simp]
                      theorem AlgHom.id_algebraCat_comp {R : Type u_1} [CommRing R] {G : Type u} [Ring G] [Algebra R G] {H : AlgebraCat R} (f : G →ₐ[R] H) :