Restriction of scalars for commutative algebra categories

Given a ring homomorphism k → K, a commutative K-algebra is in particular a commutative k-algebra, and a K-algebra homomorphism is a k-algebra homomorphism. This file packages that change of rings as a functor CommAlgCat K ⥤ CommAlgCat k.

Mathlib provides the analogous AlgCat.restrictScalars on the (not-necessarily-commutative) algebra category; this is its commutative counterpart.

Main declarations

• TauCeti.CommAlgCat.restrictScalarsObj: the underlying commutative k-algebra of a commutative K-algebra, along a fixed ring homomorphism k →+* K.
• TauCeti.CommAlgCat.restrictScalars: the restriction-of-scalars functor CommAlgCat K ⥤ CommAlgCat k along a fixed ring homomorphism k →+* K.
• TauCeti.CommAlgCat.restrictScalarsMap_hom: the underlying algebra hom of a restricted categorical morphism.

@[reducible, inline]

noncomputable abbrev TauCeti.CommAlgCat.restrictScalarsObj {k : Type u} {K : Type w} [CommRing k] [CommRing K] (f : k →+* K) (A : CommAlgCat K) : CommAlgCat k

Restrict a commutative K-algebra to a commutative k-algebra along f : k →+* K.

Equations

• TauCeti.CommAlgCat.restrictScalarsObj f A = CommAlgCat.of k ↑A

@[simp]

theorem TauCeti.CommAlgCat.algebraMap_restrictScalarsObj {k : Type u} {K : Type w} [CommRing k] [CommRing K] (f : k →+* K) (A : CommAlgCat K) (r : k) : (algebraMap k ↑(restrictScalarsObj f A)) r = (algebraMap K ↑A) (f r)

The restricted k-algebra structure has scalar map algebraMap K A ∘ f.

@[reducible, inline]

noncomputable abbrev TauCeti.CommAlgCat.restrictScalarsMap {k : Type u} {K : Type w} [CommRing k] [CommRing K] {A B : CommAlgCat K} (f : k →+* K) (χ : A ⟶ B) : restrictScalarsObj f A ⟶ restrictScalarsObj f B

Restrict a morphism of commutative K-algebras to a morphism of commutative k-algebras along f : k →+* K.

Equations

• TauCeti.CommAlgCat.restrictScalarsMap f χ = CommAlgCat.ofHom (AlgHom.restrictScalars k (CommAlgCat.Hom.hom χ))

@[simp]

theorem TauCeti.CommAlgCat.restrictScalarsMap_hom {k : Type u} {K : Type w} [CommRing k] [CommRing K] {A B : CommAlgCat K} (f : k →+* K) (χ : A ⟶ B) : CommAlgCat.Hom.hom (restrictScalarsMap f χ) = AlgHom.restrictScalars k (CommAlgCat.Hom.hom χ)

The underlying algebra hom of a restricted categorical morphism is restriction of scalars on the original algebra hom.

@[reducible, inline]

noncomputable abbrev TauCeti.CommAlgCat.restrictScalars {k : Type u} {K : Type w} [CommRing k] [CommRing K] (f : k →+* K) : CategoryTheory.Functor (CommAlgCat K) (CommAlgCat k)

The restriction-of-scalars functor CommAlgCat K ⥤ CommAlgCat k along f : k →+* K.

Equations

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

@[simp]

theorem TauCeti.CommAlgCat.restrictScalars_obj {k : Type u} {K : Type w} [CommRing k] [CommRing K] (f : k →+* K) (A : CommAlgCat K) : (restrictScalars f).obj A = restrictScalarsObj f A

The object part of restrictScalars is restriction of scalars on algebras.

@[simp]

theorem TauCeti.CommAlgCat.restrictScalars_map {k : Type u} {K : Type w} [CommRing k] [CommRing K] (f : k →+* K) {A B : CommAlgCat K} (χ : A ⟶ B) : (restrictScalars f).map χ = restrictScalarsMap f χ

The morphism part of restrictScalars is restriction of scalars on morphisms.