commAlgCatEquivUnder

Mathlib.Algebra.Category.CommAlgCat.Basic

URI: https://scilib.ai/kg/mathlib#commAlgCatEquivUnder

Lean4

/-- The category of commutative algebras over a commutative ring `R` is the same as commutative
rings under `R`. -/
@[simps]
def commAlgCatEquivUnder (R : CommRingCat) : CommAlgCat R ≌ Under R
    where
  functor.obj A := R.mkUnder A
  functor.map {A B} f := f.hom.toUnder
  inverse.obj A := .of _ A
  inverse.map {A B} f := CommAlgCat.ofHom <| CommRingCat.toAlgHom f
  unitIso := NatIso.ofComponents fun A ↦ CommAlgCat.isoMk { toRingEquiv := .refl A, commutes' _ := rfl }
  counitIso :=
    .refl
      _
        -- TODO: Generalize to `UnivLE.{u, v}` once `commAlgCatEquivUnder` is generalized.

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru