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.

• _mkInternal :: (
• carrier : Type v

  The underlying type.

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

@[instance_reducible]

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

Equations

• CommAlgCat.instCoeSortType = { coe := CommAlgCat.carrier }

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

Equations

• ↧X = { carrier := X, commRing := inst✝¹, algebra := inst✝ }

def CommAlgCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prints CommAlgCat.of R X as ↧X.

Equations

• CommAlgCat.delabOf = CategoryTheory.delabOf

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

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

The type of morphisms in CommAlgCat R.

• _mkInternal :: (
• 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_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[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) : ↧X ⟶ ↧Y

Typecheck an AlgHom as a morphism in CommAlgCat.

Equations

• CommAlgCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

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.

Equations

• CommAlgCat.Hom.Simps.hom A B f = f.hom

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 ↧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_reducible]

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

Equations

• CommAlgCat.instInhabited = { default := ↧R }

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

@[deprecated CategoryTheory.ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-06")]

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

@[instance_reducible]

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

Equations

• CommAlgCat.instCommRingObjForgetAlgHomCarrier = A.commRing

@[instance_reducible]

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

Equations

• CommAlgCat.instAlgebraObjForgetAlgHomCarrier = A.algebra

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[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 = ↧↑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.homEquivCommRingCat {R : Type u} [CommRing R] (A B : CommAlgCat R) : (A ⟶ B) ≃ { f : ↧↑A ⟶ ↧↑B // (CommRingCat.Hom.hom f).comp (algebraMap R ↑A) = algebraMap R ↑B }

The bijection between the set of morphisms A ⟶ B in CommAlgCat and the set of morphisms A ⟶ B in CommRingCat commuting with the corresponding algebra maps R → A and R → B.

Equations

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

@[simp]

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

@[simp]

theorem CommAlgCat.homEquivCommRingCat_symm_apply {R : Type u} [CommRing R] (A B : CommAlgCat R) (f : { f : ↧↑A ⟶ ↧↑B // (CommRingCat.Hom.hom f).comp (algebraMap R ↑A) = algebraMap R ↑B }) : (A.homEquivCommRingCat B).symm f = ofHom { toRingHom := CommRingCat.Hom.hom ↑f, commutes' := ⋯ }

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) : ↧X ≅ ↧Y

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

Equations

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

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

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

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.

Equations

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

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

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

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

Equations

• CommAlgCat.isoEquivAlgEquiv = { toFun := CommAlgCat.algEquivOfIso, invFun := CommAlgCat.isoMk, left_inv := ⋯, right_inv := ⋯ }

@[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 : ↧X ≅ ↧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.

Equations

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

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

The universe lift functor for commutative algebras is fully faithful.

Equations

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

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.

Equations

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

@[simp]

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

@[simp]

theorem commAlgCatEquivUnder_counitIso (R : CommRingCat) : (commAlgCatEquivUnder R).counitIso = CategoryTheory.Iso.refl ({ obj := fun (A : CategoryTheory.Under 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_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' := ⋯ })) ⋯

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

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

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