Ring objects in cartesian monoidal categories

If C is a cartesian monoidal category and X : C, we introduce a typeclass RingObj X which says that X is a ring object: it has a commutative additive group structure and a multiplicative monoid structure that is distributive over the additive structure. We also introduce a typeclass CommRingObj X which further requires that the multiplicative law is commutative.

The categories of bundled ring objects and bundled commutative ring objects are denoted RingObjCat C and CommRingObjCat C respectively.

TODO

• develop the theory of bimonoidal categories and relate this with Rig-objects

theorem CategoryTheory.mul_add_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (R : C) [MonObj R] [AddMonObj R] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R AddMonObj.add) MonObj.mul = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R (SemiCartesianMonoidalCategory.fst R R)) MonObj.mul) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R (SemiCartesianMonoidalCategory.snd R R)) MonObj.mul)) AddMonObj.add ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c

theorem CategoryTheory.add_mul_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (R : C) [MonObj R] [AddMonObj R] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.add R) MonObj.mul = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (SemiCartesianMonoidalCategory.fst R R) R) MonObj.mul) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (SemiCartesianMonoidalCategory.snd R R) R) MonObj.mul)) AddMonObj.add ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c

class CategoryTheory.RingObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : C) extends CategoryTheory.AddGrpObj R, CategoryTheory.IsCommAddMonObj R, CategoryTheory.MonObj R : Type v

A ring object in a cartesian monoidal category is an object that is equipped with an additive group structure and a (multiplicative) monoid structure that is left and right distributive over the additive structure.

• zero : MonoidalCategoryStruct.tensorUnit C ⟶ R
• add : MonoidalCategoryStruct.tensorObj R R ⟶ R
• zero_add : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight zero R) add = (MonoidalCategoryStruct.leftUnitor R).hom
• add_zero : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R zero) add = (MonoidalCategoryStruct.rightUnitor R).hom
• add_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight add R) add = CategoryStruct.comp (MonoidalCategoryStruct.associator R R R).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R add) add)
• neg : R ⟶ R
• left_neg : CategoryStruct.comp (CartesianMonoidalCategory.lift neg (CategoryStruct.id R)) AddMonObj.add = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit R) AddMonObj.zero
• right_neg : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.id R) neg) AddMonObj.add = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit R) AddMonObj.zero
• add_comm : CategoryStruct.comp (β_ R R).hom AddMonObj.add = AddMonObj.add
• one : MonoidalCategoryStruct.tensorUnit C ⟶ R
• mul : MonoidalCategoryStruct.tensorObj R R ⟶ R
• one_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one R) mul = (MonoidalCategoryStruct.leftUnitor R).hom
• mul_one : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R one) mul = (MonoidalCategoryStruct.rightUnitor R).hom
• mul_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul R) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator R R R).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R mul) mul)
• mul_add : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R AddMonObj.add) MonObj.mul = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R (SemiCartesianMonoidalCategory.fst R R)) MonObj.mul) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R (SemiCartesianMonoidalCategory.snd R R)) MonObj.mul)) AddMonObj.add
• add_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.add R) MonObj.mul = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (SemiCartesianMonoidalCategory.fst R R) R) MonObj.mul) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (SemiCartesianMonoidalCategory.snd R R) R) MonObj.mul)) AddMonObj.add

theorem CategoryTheory.Hom.mul_add {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R : C} [RingObj R] {X : C} (a b c : X ⟶ R) : a * (b + c) = a * b + a * c

theorem CategoryTheory.Hom.add_mul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R : C} [RingObj R] {X : C} (a b c : X ⟶ R) : (a + b) * c = a * c + b * c

@[reducible, inline]

abbrev CategoryTheory.Hom.ring {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R : C} [RingObj R] {X : C} : Ring (X ⟶ R)

If G is a ring object, then Hom(X, G) has a ring structure.

Equations

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

class CategoryTheory.CommRingObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : C) extends CategoryTheory.RingObj R, CategoryTheory.IsCommMonObj R : Type v

A commutative ring object in a cartesian monoidal category is a ring object such that the multiplicative law is commutative.

• zero : MonoidalCategoryStruct.tensorUnit C ⟶ R
• add : MonoidalCategoryStruct.tensorObj R R ⟶ R
• zero_add : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight zero R) add = (MonoidalCategoryStruct.leftUnitor R).hom
• add_zero : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R zero) add = (MonoidalCategoryStruct.rightUnitor R).hom
• add_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight add R) add = CategoryStruct.comp (MonoidalCategoryStruct.associator R R R).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R add) add)
• neg : R ⟶ R
• left_neg : CategoryStruct.comp (CartesianMonoidalCategory.lift neg (CategoryStruct.id R)) AddMonObj.add = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit R) AddMonObj.zero
• right_neg : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.id R) neg) AddMonObj.add = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit R) AddMonObj.zero
• add_comm : CategoryStruct.comp (β_ R R).hom AddMonObj.add = AddMonObj.add
• one : MonoidalCategoryStruct.tensorUnit C ⟶ R
• mul : MonoidalCategoryStruct.tensorObj R R ⟶ R
• one_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one R) mul = (MonoidalCategoryStruct.leftUnitor R).hom
• mul_one : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R one) mul = (MonoidalCategoryStruct.rightUnitor R).hom
• mul_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul R) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator R R R).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R mul) mul)
• mul_add : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R AddMonObj.add) MonObj.mul = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R (SemiCartesianMonoidalCategory.fst R R)) MonObj.mul) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft R (SemiCartesianMonoidalCategory.snd R R)) MonObj.mul)) AddMonObj.add
• add_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.add R) MonObj.mul = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (SemiCartesianMonoidalCategory.fst R R) R) MonObj.mul) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (SemiCartesianMonoidalCategory.snd R R) R) MonObj.mul)) AddMonObj.add
• mul_comm : CategoryStruct.comp (β_ R R).hom MonObj.mul = MonObj.mul

@[reducible, inline]

abbrev CategoryTheory.Hom.commRing {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R X : C} [CommRingObj R] : CommRing (X ⟶ R)

If G is a commutative ring object, then Hom(X, G) has a commutative ring structure.

Equations

• CategoryTheory.Hom.commRing = { toRing := CategoryTheory.Hom.ring, mul_comm := ⋯ }

class CategoryTheory.IsRingHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {R₁ R₂ : C} [AddMonObj R₁] [AddMonObj R₂] [MonObj R₁] [MonObj R₂] (f : R₁ ⟶ R₂) extends CategoryTheory.IsAddMonHom f, CategoryTheory.IsMonHom f : Prop

The property that a morphism between ring objects is a ring morphism.

• zero_hom : CategoryStruct.comp AddMonObj.zero f = AddMonObj.zero
• add_hom : CategoryStruct.comp AddMonObj.add f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) AddMonObj.add
• one_hom : CategoryStruct.comp MonObj.one f = MonObj.one
• mul_hom : CategoryStruct.comp MonObj.mul f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) MonObj.mul

instance CategoryTheory.IsRingHom.id {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (R : C) [AddMonObj R] [MonObj R] : IsRingHom (CategoryStruct.id R)

instance CategoryTheory.IsRingHom.comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {R₁ R₂ R₃ : C} [AddMonObj R₁] [AddMonObj R₂] [AddMonObj R₃] [MonObj R₁] [MonObj R₂] [MonObj R₃] (f : R₁ ⟶ R₂) (g : R₂ ⟶ R₃) [IsRingHom f] [IsRingHom g] : IsRingHom (CategoryStruct.comp f g)

structure CategoryTheory.RingObjCat (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Type (max u v)

The category of ring objects in a cartesian monoidal category.

• X : C

  The underlying object in the ambient monoidal category

• ringObj : RingObj self.X

structure CategoryTheory.RingObjCat.Hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R₁ R₂ : RingObjCat C) : Type v

A morphism of ring objects.

• hom : R₁.X ⟶ R₂.X

  The underlying morphism

• isRingHom : IsRingHom self.hom

theorem CategoryTheory.RingObjCat.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : CartesianMonoidalCategory C} {inst✝² : BraidedCategory C} {R₁ R₂ : RingObjCat C} {x y : R₁.Hom R₂} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.RingObjCat.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : CartesianMonoidalCategory C} {inst✝² : BraidedCategory C} {R₁ R₂ : RingObjCat C} {x y : R₁.Hom R₂} (hom : x.hom = y.hom) : x = y

@[implicit_reducible]

instance CategoryTheory.RingObjCat.instCategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Category.{v, max u v} (RingObjCat C)

Equations

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

@[simp]

theorem CategoryTheory.RingObjCat.id_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : RingObjCat C) : (CategoryStruct.id X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.RingObjCat.comp_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ Z✝ : RingObjCat C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.RingObjCat.hom_ext {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R₁ R₂ : RingObjCat C} {f g : R₁ ⟶ R₂} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.RingObjCat.hom_ext_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R₁ R₂ : RingObjCat C} {f g : R₁ ⟶ R₂} : f = g ↔ f.hom = g.hom

def CategoryTheory.RingObjCat.forget (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Functor (RingObjCat C) C

The forgetful functor from the category of ring objects in C to C.

Equations

• CategoryTheory.RingObjCat.forget C = { obj := fun (R : CategoryTheory.RingObjCat C) => R.X, map := fun {X Y : CategoryTheory.RingObjCat C} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.RingObjCat.forget_obj (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : RingObjCat C) : (forget C).obj R = R.X

@[simp]

theorem CategoryTheory.RingObjCat.forget_map (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : RingObjCat C} (f : X✝ ⟶ Y✝) : (forget C).map f = f.hom

instance CategoryTheory.RingObjCat.instFaithfulForget {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : (forget C).Faithful

def CategoryTheory.RingObjCat.forget₂Mon (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Functor (RingObjCat C) (Mon C)

The forgetful functor from the category of ring objects in C to the category of monoid objects in C.

Equations

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

@[simp]

theorem CategoryTheory.RingObjCat.forget₂Mon_map_hom (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : RingObjCat C} (f : X✝ ⟶ Y✝) : ((forget₂Mon C).map f).hom = f.hom

@[simp]

theorem CategoryTheory.RingObjCat.forget₂Mon_obj_X (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : RingObjCat C) : ((forget₂Mon C).obj R).X = R.X

@[simp]

theorem CategoryTheory.RingObjCat.forget₂Mon_obj_mon (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : RingObjCat C) : ((forget₂Mon C).obj R).mon = R.ringObj.toMonObj

def CategoryTheory.RingObjCat.forget₂AddMon (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Functor (RingObjCat C) (AddMon C)

The forgetful functor from the category of ring objects in C to the category of additive monoid objects in C.

Equations

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

@[simp]

theorem CategoryTheory.RingObjCat.forget₂AddMon_obj_X (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : RingObjCat C) : ((forget₂AddMon C).obj R).X = R.X

@[simp]

theorem CategoryTheory.RingObjCat.forget₂AddMon_map_hom (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : RingObjCat C} (f : X✝ ⟶ Y✝) : ((forget₂AddMon C).map f).hom = f.hom

@[simp]

theorem CategoryTheory.RingObjCat.forget₂AddMon_obj_addMon (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : RingObjCat C) : ((forget₂AddMon C).obj R).addMon = R.ringObj.toAddMonObj

structure CategoryTheory.CommRingObjCat (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Type (max u v)

The category of commutative ring objects in a cartesian monoidal category.

• X : C

  The underlying object in the ambient monoidal category

• commRingObj : CommRingObj self.X

structure CategoryTheory.CommRingObjCat.Hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R₁ R₂ : CommRingObjCat C) : Type v

A morphism of commutative ring objects.

• hom : R₁.X ⟶ R₂.X

  The underlying morphism

• isRingHom : IsRingHom self.hom

theorem CategoryTheory.CommRingObjCat.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : CartesianMonoidalCategory C} {inst✝² : BraidedCategory C} {R₁ R₂ : CommRingObjCat C} {x y : R₁.Hom R₂} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.CommRingObjCat.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {inst✝¹ : CartesianMonoidalCategory C} {inst✝² : BraidedCategory C} {R₁ R₂ : CommRingObjCat C} {x y : R₁.Hom R₂} : x = y ↔ x.hom = y.hom

@[implicit_reducible]

instance CategoryTheory.CommRingObjCat.instCategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Category.{v, max u v} (CommRingObjCat C)

Equations

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

@[simp]

theorem CategoryTheory.CommRingObjCat.id_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommRingObjCat C) : (CategoryStruct.id X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.CommRingObjCat.comp_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ Z✝ : CommRingObjCat C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.CommRingObjCat.hom_ext {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R₁ R₂ : CommRingObjCat C} {f g : R₁ ⟶ R₂} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.CommRingObjCat.hom_ext_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R₁ R₂ : CommRingObjCat C} {f g : R₁ ⟶ R₂} : f = g ↔ f.hom = g.hom

def CategoryTheory.CommRingObjCat.forget (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Functor (CommRingObjCat C) C

The forgetful functor from the category of ring objects in C to C.

Equations

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

@[simp]

theorem CategoryTheory.CommRingObjCat.forget_obj (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : CommRingObjCat C) : (forget C).obj R = R.X

@[simp]

theorem CategoryTheory.CommRingObjCat.forget_map (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : CommRingObjCat C} (f : X✝ ⟶ Y✝) : (forget C).map f = f.hom

def CategoryTheory.CommRingObjCat.forget₂RingObjCat (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Functor (CommRingObjCat C) (RingObjCat C)

The forgetful functor from the category of commutative ring objects to the category of ring objects.

Equations

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

@[simp]

theorem CategoryTheory.CommRingObjCat.forget₂RingObjCat_map_hom (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : CommRingObjCat C} (f : X✝ ⟶ Y✝) : ((forget₂RingObjCat C).map f).hom = f.hom

@[simp]

theorem CategoryTheory.CommRingObjCat.forget₂RingObjCat_obj_X (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (R : CommRingObjCat C) : ((forget₂RingObjCat C).obj R).X = R.X

def CategoryTheory.CommRingObjCat.fullyFaithfulForget₂RingObjCat (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : (forget₂RingObjCat C).FullyFaithful

The forgetful functor CommRingObjCat C ⥤ RingObjCat C is fully faithful.

Equations

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

instance CategoryTheory.CommRingObjCat.instFaithfulRingObjCatForget₂RingObjCat {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : (forget₂RingObjCat C).Faithful

instance CategoryTheory.CommRingObjCat.instFullRingObjCatForget₂RingObjCat {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : (forget₂RingObjCat C).Full

instance CategoryTheory.CommRingObjCat.instFaithfulForget {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : (forget C).Faithful