The category of commutative algebras over a commutative ring

This file defines the bundled category CommAlgCat of commutative algebras over a fixed commutative ring R along with the forgetful functors to CommRingCat and AlgCat.

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

The category of R-algebras and their morphisms.

• carrier : Type v

  The underlying type.

• commRing : CommRing ↑self
• algebra : Algebra R ↑self

instance CommAlgCat.instCoeSortType {R : Type u} [CommRing R] : CoeSort (CommAlgCat R) (Type v)

@[reducible, inline]

abbrev CommAlgCat.of (R : Type u) [CommRing R] (X : Type v) [CommRing X] [Algebra R X] : CommAlgCat 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 CommAlgCat R.

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

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

The type of morphisms in CommAlgCat R.

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

  The underlying algebra map.

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

theorem CommAlgCat.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {A B : CommAlgCat R} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'

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

instance CommAlgCat.instConcreteCategoryAlgHomCarrier {R : Type u} [CommRing R] : CategoryTheory.ConcreteCategory (CommAlgCat R) fun (x1 x2 : CommAlgCat R) => ↑x1 →ₐ[R] ↑x2

@[reducible, inline]

abbrev CommAlgCat.Hom.hom {R : Type u} [CommRing R] {A B : CommAlgCat R} (f : A.Hom B) : ↑A →ₐ[R] ↑B

Turn a morphism in CommAlgCat back into an AlgHom.

@[reducible, inline]

abbrev CommAlgCat.ofHom {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Algebra R X] [CommRing Y] [Algebra R Y] (f : X →ₐ[R] Y) : of R X ⟶ of R Y

Typecheck an AlgHom as a morphism in CommAlgCat.

def CommAlgCat.Hom.Simps.hom {R : Type u} [CommRing R] (A B : CommAlgCat R) (f : A.Hom B) : ↑A →ₐ[R] ↑B

Use the ConcreteCategory.hom projection for @[simps] lemmas.

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

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

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

@[simp]

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

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

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

theorem CommAlgCat.hom_ext_iff {R : Type u} [CommRing R] {A B : CommAlgCat R} {f g : A ⟶ B} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

instance CommAlgCat.instInhabited {R : Type u} [CommRing R] : Inhabited (CommAlgCat R)

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

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

instance CommAlgCat.instCommRingObjForgetAlgHomCarrier {R : Type u} [CommRing R] {A : CommAlgCat R} : CommRing ((CategoryTheory.forget (CommAlgCat R)).obj A)

instance CommAlgCat.instAlgebraObjForgetAlgHomCarrier {R : Type u} [CommRing R] {A : CommAlgCat R} : Algebra R ((CategoryTheory.forget (CommAlgCat R)).obj A)

instance CommAlgCat.hasForgetToCommRingCat {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (CommAlgCat R) CommRingCat

instance CommAlgCat.hasForgetToAlgCat {R : Type u} [CommRing R] : CategoryTheory.HasForget₂ (CommAlgCat R) (AlgCat R)

@[simp]

theorem CommAlgCat.forget₂_commRingCat_obj {R : Type u} [CommRing R] (A : CommAlgCat R) : (CategoryTheory.forget₂ (CommAlgCat R) CommRingCat).obj A = { carrier := ↑A, commRing := A.commRing }

@[simp]

theorem CommAlgCat.forget₂_commRingCat_map {R : Type u} [CommRing R] {A B : CommAlgCat R} (f : A ⟶ B) : (CategoryTheory.forget₂ (CommAlgCat R) CommRingCat).map f = CommRingCat.ofHom ↑(Hom.hom f)

@[simp]

theorem CommAlgCat.forget₂_algCat_obj {R : Type u} [CommRing R] (A : CommAlgCat R) : (CategoryTheory.forget₂ (CommAlgCat R) (AlgCat R)).obj A = AlgCat.of R ↑A

@[simp]

theorem CommAlgCat.forget₂_algCat_map {R : Type u} [CommRing R] {A B : CommAlgCat R} (f : A ⟶ B) : (CategoryTheory.forget₂ (CommAlgCat R) (AlgCat R)).map f = AlgCat.ofHom (Hom.hom f)

def CommAlgCat.isoMk {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : Algebra R X} {x✝³ : Algebra R Y} (e : X ≃ₐ[R] Y) : of R X ≅ of R Y

Build an isomorphism in the category CommAlgCat R from an AlgEquiv between commutative Algebras.

@[simp]

theorem CommAlgCat.isoMk_hom {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : Algebra R X} {x✝³ : Algebra R Y} (e : X ≃ₐ[R] Y) : (isoMk e).hom = ofHom ↑e

@[simp]

theorem CommAlgCat.isoMk_inv {R : Type u} [CommRing R] {X Y : Type v} {x✝ : CommRing X} {x✝¹ : CommRing Y} {x✝² : Algebra R X} {x✝³ : Algebra R Y} (e : X ≃ₐ[R] Y) : (isoMk e).inv = ofHom ↑e.symm

def CommAlgCat.algEquivOfIso {R : Type u} [CommRing R] {A B : CommAlgCat R} (i : A ≅ B) : ↑A ≃ₐ[R] ↑B

Build an AlgEquiv from an isomorphism in the category CommAlgCat R.

@[simp]

theorem CommAlgCat.algEquivOfIso_apply {R : Type u} [CommRing R] {A B : CommAlgCat R} (i : A ≅ B) (a : ↑A) : (algEquivOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a

@[simp]

theorem CommAlgCat.algEquivOfIso_symm_apply {R : Type u} [CommRing R] {A B : CommAlgCat R} (i : A ≅ B) (a : ↑B) : (algEquivOfIso i).symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a

@[deprecated CommAlgCat.algEquivOfIso (since := "2025-08-22")]

def CommAlgCat.ofIso {R : Type u} [CommRing R] {A B : CommAlgCat R} (i : A ≅ B) : ↑A ≃ₐ[R] ↑B

Alias of CommAlgCat.algEquivOfIso.

---

Build an AlgEquiv from an isomorphism in the category CommAlgCat R.

def CommAlgCat.isoEquivAlgEquiv {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Algebra R X] [CommRing Y] [Algebra R Y] : (of R X ≅ of R Y) ≃ X ≃ₐ[R] Y

Algebra equivalences between Algebras are the same as isomorphisms in CommAlgCat.

@[simp]

theorem CommAlgCat.isoEquivAlgEquiv_symm_apply {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Algebra R X] [CommRing Y] [Algebra R Y] (e : X ≃ₐ[R] Y) : isoEquivAlgEquiv.symm e = isoMk e

@[simp]

theorem CommAlgCat.isoEquivAlgEquiv_apply {R : Type u} [CommRing R] {X Y : Type v} [CommRing X] [Algebra R X] [CommRing Y] [Algebra R Y] (i : of R X ≅ of R Y) : isoEquivAlgEquiv i = algEquivOfIso i

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

def CommAlgCat.uliftFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor (CommAlgCat R) (CommAlgCat R)

Universe lift functor for commutative algebras.

def CommAlgCat.fullyFaithfulUliftFunctor (R : Type u) [CommRing R] : (uliftFunctor R).FullyFaithful

The universe lift functor for commutative algebras is fully faithful.

instance CommAlgCat.instFullUliftFunctor (R : Type u) [CommRing R] : (uliftFunctor R).Full

instance CommAlgCat.instFaithfulUliftFunctor (R : Type u) [CommRing R] : (uliftFunctor R).Faithful

def commAlgCatEquivUnder (R : CommRingCat) : CommAlgCat ↑R ≌ CategoryTheory.Under R

The category of commutative algebras over a commutative ring R is the same as commutative rings under R.

@[simp]

theorem commAlgCatEquivUnder_functor_map (R : CommRingCat) {A B : CommAlgCat ↑R} (f : A ⟶ B) : (commAlgCatEquivUnder R).functor.map f = (CommAlgCat.Hom.hom f).toUnder

@[simp]

theorem commAlgCatEquivUnder_inverse_obj_carrier (R : CommRingCat) (A : CategoryTheory.Under R) : ↑((commAlgCatEquivUnder R).inverse.obj A) = ↑A.right

@[simp]

theorem commAlgCatEquivUnder_counitIso (R : CommRingCat) : (commAlgCatEquivUnder R).counitIso = CategoryTheory.Iso.refl ({ obj := fun (A : CategoryTheory.Under R) => CommAlgCat.of ↑R ↑A.right, map := fun {A B : CategoryTheory.Under R} (f : A ⟶ B) => CommAlgCat.ofHom (CommRingCat.toAlgHom f), map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (A : CommAlgCat ↑R) => R.mkUnder ↑A, map := fun {A B : CommAlgCat ↑R} (f : A ⟶ B) => (CommAlgCat.Hom.hom f).toUnder, map_id := ⋯, map_comp := ⋯ })

@[simp]

theorem commAlgCatEquivUnder_inverse_map (R : CommRingCat) {A B : CategoryTheory.Under R} (f : A ⟶ B) : (commAlgCatEquivUnder R).inverse.map f = CommAlgCat.ofHom (CommRingCat.toAlgHom f)

@[simp]

theorem commAlgCatEquivUnder_functor_obj (R : CommRingCat) (A : CommAlgCat ↑R) : (commAlgCatEquivUnder R).functor.obj A = R.mkUnder ↑A

@[simp]

theorem commAlgCatEquivUnder_unitIso (R : CommRingCat) : (commAlgCatEquivUnder R).unitIso = CategoryTheory.NatIso.ofComponents (fun (A : CommAlgCat ↑R) => CommAlgCat.isoMk (let __RingEquiv := RingEquiv.refl ↑A; { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })) ⋯

instance instHasColimitsCommAlgCat {R : Type u} [CommRing R] : CategoryTheory.Limits.HasColimits (CommAlgCat R)

instance instHasLimitsCommAlgCat {R : Type u} [CommRing R] : CategoryTheory.Limits.HasLimits (CommAlgCat R)