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))

• carrier : Type v
• isRing : Ring ↑s
• isAlgebra : Algebra R ↑s

The category of R-algebras and their morphisms.

@[inline, reducible]

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.

instance AlgebraCat.instCoeSortAlgebraCatType (R : Type u) [CommRing R] : CoeSort (AlgebraCat R) (Type v)

instance AlgebraCat.instCategoryAlgebraCat (R : Type u) [CommRing R] : CategoryTheory.Category.{v, max (v + 1) u} (AlgebraCat R)

instance AlgebraCat.instAlgHomClassHomAlgebraCatToQuiverToCategoryStructInstCategoryAlgebraCatCarrierToCommSemiringToSemiringIsRingIsAlgebra (R : Type u) [CommRing R] {M : AlgebraCat R} {N : AlgebraCat R} : AlgHomClass (M ⟶ N) R ↑M ↑N

instance AlgebraCat.instConcreteCategoryAlgebraCatInstCategoryAlgebraCat (R : Type u) [CommRing R] : CategoryTheory.ConcreteCategory (AlgebraCat R)

instance AlgebraCat.instRingObjAlgebraCatToQuiverToCategoryStructInstCategoryAlgebraCatTypeToQuiverToCategoryStructTypesToPrefunctorForgetInstConcreteCategoryAlgebraCatInstCategoryAlgebraCat (R : Type u) [CommRing R] {S : AlgebraCat R} : Ring ((CategoryTheory.forget (AlgebraCat R)).obj S)

instance AlgebraCat.instAlgebraObjAlgebraCatToQuiverToCategoryStructInstCategoryAlgebraCatTypeToQuiverToCategoryStructTypesToPrefunctorForgetInstConcreteCategoryAlgebraCatInstCategoryAlgebraCatToCommSemiringToSemiringInstRingObjAlgebraCatToQuiverToCategoryStructInstCategoryAlgebraCatTypeToQuiverToCategoryStructTypesToPrefunctorForgetInstConcreteCategoryAlgebraCatInstCategoryAlgebraCat (R : Type u) [CommRing R] {S : AlgebraCat R} : Algebra R ((CategoryTheory.forget (AlgebraCat R)).obj S)

instance AlgebraCat.hasForgetToRing (R : Type u) [CommRing R] : CategoryTheory.HasForget₂ (AlgebraCat R) RingCat

instance AlgebraCat.hasForgetToModule (R : Type u) [CommRing R] : CategoryTheory.HasForget₂ (AlgebraCat R) (ModuleCat R)

def AlgebraCat.of (R : Type u) [CommRing R] (X : Type v) [Ring X] [Algebra R X] : AlgebraCat R

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

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) : AlgebraCat.of R X ⟶ AlgebraCat.of R Y

Typecheck a AlgHom as a morphism in AlgebraCat R.

@[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) : ↑(AlgebraCat.ofHom f) x = ↑f x

instance AlgebraCat.instInhabitedAlgebraCat (R : Type u) [CommRing R] : Inhabited (AlgebraCat R)

@[simp]

theorem AlgebraCat.coe_of (R : Type u) [CommRing R] (X : Type u) [Ring X] [Algebra R X] : ↑(AlgebraCat.of R X) = X

@[simp]

theorem AlgebraCat.ofSelfIso_hom {R : Type u} [CommRing R] (M : AlgebraCat R) : (AlgebraCat.ofSelfIso M).hom = CategoryTheory.CategoryStruct.id M

@[simp]

theorem AlgebraCat.ofSelfIso_inv {R : Type u} [CommRing R] (M : AlgebraCat R) : (AlgebraCat.ofSelfIso M).inv = CategoryTheory.CategoryStruct.id M

def AlgebraCat.ofSelfIso {R : Type u} [CommRing R] (M : AlgebraCat R) : AlgebraCat.of R ↑M ≅ M

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

@[simp]

theorem AlgebraCat.id_apply {R : Type u} [CommRing R] {M : ModuleCat R} (m : ↑M) : ↑(CategoryTheory.CategoryStruct.id M) 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) : ↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

@[simp]

theorem AlgebraCat.free_obj_carrier (R : Type u) [CommRing R] (S : Type u) : ↑((AlgebraCat.free R).obj S) = FreeAlgebra R S

@[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)

def AlgebraCat.free (R : Type u) [CommRing R] : CategoryTheory.Functor (Type u) (AlgebraCat R)

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

def AlgebraCat.adj (R : Type u) [CommRing R] : AlgebraCat.free R ⊣ CategoryTheory.forget (AlgebraCat R)

The free/forget adjunction for R-algebras.

instance AlgebraCat.instIsRightAdjointTypeTypesAlgebraCatInstCategoryAlgebraCatForgetInstConcreteCategoryAlgebraCatInstCategoryAlgebraCat (R : Type u) [CommRing R] : CategoryTheory.IsRightAdjoint (CategoryTheory.forget (AlgebraCat R))

@[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₂) : (AlgEquiv.toAlgebraIso e).inv = ↑(AlgEquiv.symm e)

@[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₂) : (AlgEquiv.toAlgebraIso e).hom = ↑e

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₂) : AlgebraCat.of R X₁ ≅ AlgebraCat.of R X₂

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

@[simp]

theorem CategoryTheory.Iso.toAlgEquiv_apply {R : Type u} [CommRing R] {X : AlgebraCat R} {Y : AlgebraCat R} (i : X ≅ Y) (a : ↑X) : ↑(CategoryTheory.Iso.toAlgEquiv i) 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) : ↑(AlgEquiv.symm (CategoryTheory.Iso.toAlgEquiv i)) 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.

@[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 = CategoryTheory.Iso.toAlgEquiv i

@[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 = AlgEquiv.toAlgebraIso e

def algEquivIsoAlgebraIso {R : Type u} [CommRing R] {X : Type u} {Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] : (X ≃ₐ[R] Y) ≅ AlgebraCat.of R X ≅ AlgebraCat.of R Y

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

instance instCoeOutSubalgebraToCommSemiringToSemiringAlgebraCat {R : Type u} [CommRing R] (X : Type u) [Ring X] [Algebra R X] : CoeOut (Subalgebra R X) (AlgebraCat R)

instance AlgebraCat.forget_reflects_isos {R : Type u} [CommRing R] : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget (AlgebraCat R))