# 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) [] :
Type (max u (v + 1))

The category of R-algebras and their morphisms.

Instances For
@[inline, reducible]
abbrev AlgebraCatMax (R : Type u₁) [] :
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.

Instances For
def AlgebraCat.of (R : Type u) [] (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.

Instances For
def AlgebraCat.ofHom {R : Type u} [] {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.

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

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

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

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

Instances For
def AlgebraCat.adj (R : Type u) [] :

The free/forget adjunction for R-algebras.

Instances For
@[simp]
theorem AlgEquiv.toAlgebraIso_inv {R : Type u} [] {X₁ : Type u} {X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
().inv = ↑()
@[simp]
theorem AlgEquiv.toAlgebraIso_hom {R : Type u} [] {X₁ : Type u} {X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
().hom = e
def AlgEquiv.toAlgebraIso {R : Type u} [] {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.

Instances For
@[simp]
theorem CategoryTheory.Iso.toAlgEquiv_apply {R : Type u} [] {X : } {Y : } (i : X Y) (a : X) :
= i.hom a
@[simp]
theorem CategoryTheory.Iso.toAlgEquiv_symm_apply {R : Type u} [] {X : } {Y : } (i : X Y) (a : Y) :
= i.inv a
def CategoryTheory.Iso.toAlgEquiv {R : Type u} [] {X : } {Y : } (i : X Y) :
X ≃ₐ[R] Y

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

Instances For
@[simp]
theorem algEquivIsoAlgebraIso_inv {R : Type u} [] {X : Type u} {Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] (i : ) :
algEquivIsoAlgebraIso.inv i =
@[simp]
theorem algEquivIsoAlgebraIso_hom {R : Type u} [] {X : Type u} {Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] (e : X ≃ₐ[R] Y) :
algEquivIsoAlgebraIso.hom e =
def algEquivIsoAlgebraIso {R : Type u} [] {X : Type u} {Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] :
(X ≃ₐ[R] Y)

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

Instances For