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.

• carrier : Type v

  The underlying type.

• isRing : Ring ↑self
• isAlgebra : Algebra R ↑self

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

• AlgebraCatMax R = AlgebraCat R

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

Equations

• AlgebraCat.instCoeSortType R = { coe := AlgebraCat.carrier }

@[reducible, inline]

abbrev 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. This is the preferred way to construct a term of AlgebraCat R.

Equations

• AlgebraCat.of R X = AlgebraCat.mk✝ X

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

structure AlgebraCat.Hom {R : Type u} [CommRing R] (A B : AlgebraCat R) : Type v

The type of morphisms in AlgebraCat R.

• hom : ↑A →ₐ[R] ↑B

  The underlying algebra map.

theorem AlgebraCat.Hom.ext {R : Type u} {inst✝ : CommRing R} {A B : AlgebraCat R} {x y : A.Hom B} (hom : x.hom = y.hom) : x = y

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

Equations

• AlgebraCat.instCategory R = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance AlgebraCat.instCoeFunHomForallCarrier (R : Type u) [CommRing R] {M N : AlgebraCat R} : CoeFun (M ⟶ N) fun (x : M ⟶ N) => ↑M → ↑N

Equations

• AlgebraCat.instCoeFunHomForallCarrier R = { coe := fun (f : M ⟶ N) => ⇑f.hom }

@[simp]

theorem AlgebraCat.hom_id (R : Type u) [CommRing R] {A : AlgebraCat R} : (CategoryTheory.CategoryStruct.id A).hom = AlgHom.id R ↑A

theorem AlgebraCat.id_apply (R : Type u) [CommRing R] (A : AlgebraCat R) (a : ↑A) : (CategoryTheory.CategoryStruct.id A).hom a = a

@[simp]

theorem AlgebraCat.hom_comp (R : Type u) [CommRing R] {A B C : AlgebraCat R} (f : A ⟶ B) (g : B ⟶ C) : (CategoryTheory.CategoryStruct.comp f g).hom = g.hom.comp f.hom

theorem AlgebraCat.comp_apply (R : Type u) [CommRing R] {A B C : AlgebraCat R} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A) : (CategoryTheory.CategoryStruct.comp f g).hom a = g.hom (f.hom a)

theorem AlgebraCat.hom_ext (R : Type u) [CommRing R] {A B : AlgebraCat R} {f g : A ⟶ B} (hf : f.hom = g.hom) : f = g

@[reducible, inline]

abbrev AlgebraCat.ofHom {R : Type u} [CommRing R] {X 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 an AlgHom as a morphism in AlgebraCat R.

Equations

• AlgebraCat.ofHom f = { hom := f }

theorem AlgebraCat.hom_ofHom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y] (f : X →ₐ[R] Y) : (AlgebraCat.ofHom f).hom = f

@[simp]

theorem AlgebraCat.ofHom_hom (R : Type u) [CommRing R] {A B : AlgebraCat R} (f : A ⟶ B) : AlgebraCat.ofHom f.hom = f

@[simp]

theorem AlgebraCat.ofHom_id (R : Type u) [CommRing R] {X : Type v} [Ring X] [Algebra R X] : AlgebraCat.ofHom (AlgHom.id R X) = CategoryTheory.CategoryStruct.id (AlgebraCat.of R X)

@[simp]

theorem AlgebraCat.ofHom_comp (R : Type u) [CommRing R] {X Y Z : Type v} [Ring X] [Ring Y] [Ring Z] [Algebra R X] [Algebra R Y] [Algebra R Z] (f : X →ₐ[R] Y) (g : Y →ₐ[R] Z) : AlgebraCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (AlgebraCat.ofHom f) (AlgebraCat.ofHom g)

theorem AlgebraCat.ofHom_apply {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y] (f : X →ₐ[R] Y) (x : X) : (AlgebraCat.ofHom f).hom x = f x

@[simp]

theorem AlgebraCat.inv_hom_apply (R : Type u) [CommRing R] {A B : AlgebraCat R} (e : A ≅ B) (x : ↑A) : e.inv.hom (e.hom.hom x) = x

@[simp]

theorem AlgebraCat.hom_inv_apply (R : Type u) [CommRing R] {A B : AlgebraCat R} (e : A ≅ B) (x : ↑B) : e.hom.hom (e.inv.hom x) = x

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

Equations

• AlgebraCat.instInhabited R = { default := AlgebraCat.of R R }

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

Equations

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

theorem AlgebraCat.forget_obj (R : Type u) [CommRing R] {A : AlgebraCat R} : (CategoryTheory.forget (AlgebraCat R)).obj A = ↑A

theorem AlgebraCat.forget_map (R : Type u) [CommRing R] {A B : AlgebraCat R} (f : A ⟶ B) : (CategoryTheory.forget (AlgebraCat R)).map f = ⇑f.hom

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

Equations

• AlgebraCat.instRingObjForget R = inferInstance

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

Equations

• AlgebraCat.instAlgebraObjForget R = inferInstance

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

Equations

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

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

Equations

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

@[simp]

theorem AlgebraCat.forget₂_module_obj (R : Type u) [CommRing R] (X : AlgebraCat R) : (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X

@[simp]

theorem AlgebraCat.forget₂_module_map (R : Type u) [CommRing R] {X Y : AlgebraCat R} (f : X ⟶ Y) : (CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).map f = ModuleCat.ofHom f.hom.toLinearMap

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.

Equations

• M.ofSelfIso = { hom := CategoryTheory.CategoryStruct.id M, inv := CategoryTheory.CategoryStruct.id M, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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.

Equations

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

@[simp]

theorem AlgebraCat.free_map (R : Type u) [CommRing R] {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : (AlgebraCat.free R).map f = AlgebraCat.ofHom ((FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f))

@[simp]

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

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

The free/forget adjunction for R-algebras.

Equations

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

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

def AlgEquiv.toAlgebraIso {R : Type u} [CommRing R] {X₁ 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.

Equations

• e.toAlgebraIso = { hom := AlgebraCat.ofHom ↑e, inv := AlgebraCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem AlgEquiv.toAlgebraIso_inv_hom {R : Type u} [CommRing R] {X₁ X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) : e.toAlgebraIso.inv.hom = ↑e.symm

@[simp]

theorem AlgEquiv.toAlgebraIso_hom_hom {R : Type u} [CommRing R] {X₁ X₂ : Type u} {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) : e.toAlgebraIso.hom.hom = ↑e

def CategoryTheory.Iso.toAlgEquiv {R : Type u} [CommRing R] {X Y : AlgebraCat R} (i : X ≅ Y) : ↑X ≃ₐ[R] ↑Y

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

Equations

• i.toAlgEquiv = { toFun := ⇑i.hom.hom, invFun := ⇑i.inv.hom, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem CategoryTheory.Iso.toAlgEquiv_apply {R : Type u} [CommRing R] {X Y : AlgebraCat R} (i : X ≅ Y) (a : ↑X) : i.toAlgEquiv a = i.hom.hom a

@[simp]

theorem CategoryTheory.Iso.toAlgEquiv_symm_apply {R : Type u} [CommRing R] {X Y : AlgebraCat R} (i : X ≅ Y) (a : ↑Y) : i.toAlgEquiv.symm a = i.inv.hom a

def algEquivIsoAlgebraIso {R : Type u} [CommRing R] {X 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.

Equations

• algEquivIsoAlgebraIso = { hom := fun (e : X ≃ₐ[R] Y) => e.toAlgebraIso, inv := fun (i : AlgebraCat.of R X ≅ AlgebraCat.of R Y) => i.toAlgEquiv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem algEquivIsoAlgebraIso_inv {R : Type u} [CommRing R] {X 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

@[simp]

theorem algEquivIsoAlgebraIso_hom {R : Type u} [CommRing R] {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] (e : X ≃ₐ[R] Y) : algEquivIsoAlgebraIso.hom e = e.toAlgebraIso

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