The category of commutative rings has all colimits.

This file uses a "pre-automated" approach, just as for Mathlib/Algebra/Category/MonCat/Colimits.lean. It is a very uniform approach, that conceivably could be synthesised directly by a tactic that analyses the shape of CommRing and RingHom.

We build the colimit of a diagram in RingCat by constructing the free ring on the disjoint union of all the rings in the diagram, then taking the quotient by the ring laws within each ring, and the identifications given by the morphisms in the diagram.

inductive RingCat.Colimits.Prequotient {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Type v

An inductive type representing all ring expressions (without Relations) on a collection of types indexed by the objects of J.

• of: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J RingCat} → (j : J) → ↑(F.obj j) → RingCat.Colimits.Prequotient F
• zero: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J RingCat} → RingCat.Colimits.Prequotient F
• one: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J RingCat} → RingCat.Colimits.Prequotient F
• neg: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J RingCat} → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F
• add: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J RingCat} → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F
• mul: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J RingCat} → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F

instance RingCat.Colimits.instInhabitedPrequotient {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Inhabited (RingCat.Colimits.Prequotient F)

Equations

• RingCat.Colimits.instInhabitedPrequotient F = { default := RingCat.Colimits.Prequotient.zero }

inductive RingCat.Colimits.Relation {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F → Prop

The Relation on Prequotient saying when two expressions are equal because of the ring laws, or because one element is mapped to another by a morphism in the diagram.

• refl: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x x
• symm: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x y → RingCat.Colimits.Relation F y x
• trans: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x y → RingCat.Colimits.Relation F y z → RingCat.Colimits.Relation F x z
• map: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j j' : J) (f : j ⟶ j') (x : ↑(F.obj j)), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j' ((F.map f) x)) (RingCat.Colimits.Prequotient.of j x)
• zero: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j 0) RingCat.Colimits.Prequotient.zero
• one: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j 1) RingCat.Colimits.Prequotient.one
• neg: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J) (x : ↑(F.obj j)), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j (-x)) (RingCat.Colimits.Prequotient.of j x).neg
• add: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J) (x y : ↑(F.obj j)), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j (x + y)) ((RingCat.Colimits.Prequotient.of j x).add (RingCat.Colimits.Prequotient.of j y))
• mul: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (j : J) (x y : ↑(F.obj j)), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.of j (x * y)) ((RingCat.Colimits.Prequotient.of j x).mul (RingCat.Colimits.Prequotient.of j y))
• neg_1: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x x' : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x x' → RingCat.Colimits.Relation F x.neg x'.neg
• add_1: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x x' y : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x x' → RingCat.Colimits.Relation F (x.add y) (x'.add y)
• add_2: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y y' : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F y y' → RingCat.Colimits.Relation F (x.add y) (x.add y')
• mul_1: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x x' y : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F x x' → RingCat.Colimits.Relation F (x.mul y) (x'.mul y)
• mul_2: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y y' : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F y y' → RingCat.Colimits.Relation F (x.mul y) (x.mul y')
• zero_add: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.zero.add x) x
• add_zero: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.add RingCat.Colimits.Prequotient.zero) x
• one_mul: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.one.mul x) x
• mul_one: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.mul RingCat.Colimits.Prequotient.one) x
• neg_add_cancel: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.neg.add x) RingCat.Colimits.Prequotient.zero
• add_comm: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.add y) (y.add x)
• add_assoc: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F ((x.add y).add z) (x.add (y.add z))
• mul_assoc: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F ((x.mul y).mul z) (x.mul (y.mul z))
• left_distrib: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.mul (y.add z)) ((x.mul y).add (x.mul z))
• right_distrib: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F ((x.add y).mul z) ((x.mul z).add (y.mul z))
• zero_mul: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.zero.mul x) RingCat.Colimits.Prequotient.zero
• mul_zero: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat} (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.mul RingCat.Colimits.Prequotient.zero) RingCat.Colimits.Prequotient.zero

instance RingCat.Colimits.colimitSetoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Setoid (RingCat.Colimits.Prequotient F)

The setoid corresponding to commutative expressions modulo monoid Relations and identifications.

Equations

• RingCat.Colimits.colimitSetoid F = { r := RingCat.Colimits.Relation F, iseqv := ⋯ }

def RingCat.Colimits.ColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Type v

The underlying type of the colimit of a diagram in CommRingCat.

Equations

• RingCat.Colimits.ColimitType F = Quotient (RingCat.Colimits.colimitSetoid F)

instance RingCat.Colimits.ColimitType.instZero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Zero (RingCat.Colimits.ColimitType F)

Equations

• RingCat.Colimits.ColimitType.instZero F = { zero := ⟦RingCat.Colimits.Prequotient.zero⟧ }

instance RingCat.Colimits.ColimitType.instAdd {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Add (RingCat.Colimits.ColimitType F)

Equations

• RingCat.Colimits.ColimitType.instAdd F = { add := Quotient.map₂ RingCat.Colimits.Prequotient.add ⋯ }

instance RingCat.Colimits.ColimitType.instNeg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Neg (RingCat.Colimits.ColimitType F)

Equations

• RingCat.Colimits.ColimitType.instNeg F = { neg := Quotient.map RingCat.Colimits.Prequotient.neg ⋯ }

instance RingCat.Colimits.ColimitType.AddGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : AddGroup (RingCat.Colimits.ColimitType F)

Equations

• RingCat.Colimits.ColimitType.AddGroup F = AddGroup.mk ⋯

instance RingCat.Colimits.InhabitedColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Inhabited (RingCat.Colimits.ColimitType F)

Equations

• RingCat.Colimits.InhabitedColimitType F = { default := 0 }

instance RingCat.Colimits.ColimitType.AddGroupWithOne {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : AddGroupWithOne (RingCat.Colimits.ColimitType F)

Equations

• RingCat.Colimits.ColimitType.AddGroupWithOne F = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance RingCat.Colimits.instRingColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Ring (RingCat.Colimits.ColimitType F)

Equations

• RingCat.Colimits.instRingColimitType F = Ring.mk ⋯ AddGroupWithOne.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RingCat.Colimits.quot_zero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) RingCat.Colimits.Prequotient.zero = 0

@[simp]

theorem RingCat.Colimits.quot_one {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) RingCat.Colimits.Prequotient.one = 1

@[simp]

theorem RingCat.Colimits.quot_neg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (x : RingCat.Colimits.Prequotient F) : Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x.neg = -Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x

@[simp]

theorem RingCat.Colimits.quot_add {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (x : RingCat.Colimits.Prequotient F) (y : RingCat.Colimits.Prequotient F) : Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) (x.add y) = Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x + Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) y

@[simp]

theorem RingCat.Colimits.quot_mul {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (x : RingCat.Colimits.Prequotient F) (y : RingCat.Colimits.Prequotient F) : Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) (x.mul y) = Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x * Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) y

def RingCat.Colimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : RingCat

The bundled ring giving the colimit of a diagram.

Equations

• RingCat.Colimits.colimit F = RingCat.of (RingCat.Colimits.ColimitType F)

def RingCat.Colimits.coconeFun {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (j : J) (x : ↑(F.obj j)) : RingCat.Colimits.ColimitType F

The function from a given ring in the diagram to the colimit ring.

Equations

• RingCat.Colimits.coconeFun F j x = Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) (RingCat.Colimits.Prequotient.of j x)

def RingCat.Colimits.coconeMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (j : J) : F.obj j ⟶ RingCat.Colimits.colimit F

The ring homomorphism from a given ring in the diagram to the colimit ring.

Equations

• RingCat.Colimits.coconeMorphism F j = { toFun := RingCat.Colimits.coconeFun F j, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingCat.Colimits.cocone_naturality {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) {j : J} {j' : J} (f : j ⟶ j') : CategoryTheory.CategoryStruct.comp (F.map f) (RingCat.Colimits.coconeMorphism F j') = RingCat.Colimits.coconeMorphism F j

@[simp]

theorem RingCat.Colimits.cocone_naturality_components {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (j : J) (j' : J) (f : j ⟶ j') (x : ↑(F.obj j)) : (RingCat.Colimits.coconeMorphism F j') ((F.map f) x) = (RingCat.Colimits.coconeMorphism F j) x

def RingCat.Colimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit ring.

Equations

• RingCat.Colimits.colimitCocone F = { pt := RingCat.Colimits.colimit F, ι := { app := RingCat.Colimits.coconeMorphism F, naturality := ⋯ } }

def RingCat.Colimits.descFunLift {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (s : CategoryTheory.Limits.Cocone F) : RingCat.Colimits.Prequotient F → ↑s.pt

The function from the free ring on the diagram to the cone point of any other cocone.

Equations

• RingCat.Colimits.descFunLift F s (RingCat.Colimits.Prequotient.of j x_1) = (s.ι.app j) x_1
• RingCat.Colimits.descFunLift F s RingCat.Colimits.Prequotient.zero = 0
• RingCat.Colimits.descFunLift F s RingCat.Colimits.Prequotient.one = 1
• RingCat.Colimits.descFunLift F s x_1.neg = -RingCat.Colimits.descFunLift F s x_1
• RingCat.Colimits.descFunLift F s (x_1.add y) = RingCat.Colimits.descFunLift F s x_1 + RingCat.Colimits.descFunLift F s y
• RingCat.Colimits.descFunLift F s (x_1.mul y) = RingCat.Colimits.descFunLift F s x_1 * RingCat.Colimits.descFunLift F s y

def RingCat.Colimits.descFun {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (s : CategoryTheory.Limits.Cocone F) : RingCat.Colimits.ColimitType F → ↑s.pt

The function from the colimit ring to the cone point of any other cocone.

Equations

• RingCat.Colimits.descFun F s = Quot.lift (RingCat.Colimits.descFunLift F s) ⋯

def RingCat.Colimits.descMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) (s : CategoryTheory.Limits.Cocone F) : RingCat.Colimits.colimit F ⟶ s.pt

The ring homomorphism from the colimit ring to the cone point of any other cocone.

Equations

• RingCat.Colimits.descMorphism F s = { toFun := RingCat.Colimits.descFun F s, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def RingCat.Colimits.colimitIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat) : CategoryTheory.Limits.IsColimit (RingCat.Colimits.colimitCocone F)

Evidence that the proposed colimit is the colimit.

Equations

• RingCat.Colimits.colimitIsColimit F = { desc := fun (s : CategoryTheory.Limits.Cocone F) => RingCat.Colimits.descMorphism F s, fac := ⋯, uniq := ⋯ }

instance RingCat.Colimits.hasColimits_ringCat : CategoryTheory.Limits.HasColimits RingCat

Equations

• RingCat.Colimits.hasColimits_ringCat = ⋯

We build the colimit of a diagram in CommRingCat by constructing the free commutative ring on the disjoint union of all the commutative rings in the diagram, then taking the quotient by the commutative ring laws within each commutative ring, and the identifications given by the morphisms in the diagram.

inductive CommRingCat.Colimits.Prequotient {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Type v

An inductive type representing all commutative ring expressions (without Relations) on a collection of types indexed by the objects of J.

• of: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J CommRingCat} → (j : J) → ↑(F.obj j) → CommRingCat.Colimits.Prequotient F
• zero: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J CommRingCat} → CommRingCat.Colimits.Prequotient F
• one: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J CommRingCat} → CommRingCat.Colimits.Prequotient F
• neg: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J CommRingCat} → CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F
• add: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J CommRingCat} → CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F
• mul: {J : Type v} → [inst : CategoryTheory.SmallCategory J] → {F : CategoryTheory.Functor J CommRingCat} → CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F

instance CommRingCat.Colimits.instInhabitedPrequotient {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Inhabited (CommRingCat.Colimits.Prequotient F)

Equations

• CommRingCat.Colimits.instInhabitedPrequotient F = { default := CommRingCat.Colimits.Prequotient.zero }

inductive CommRingCat.Colimits.Relation {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : CommRingCat.Colimits.Prequotient F → CommRingCat.Colimits.Prequotient F → Prop

The Relation on Prequotient saying when two expressions are equal because of the commutative ring laws, or because one element is mapped to another by a morphism in the diagram.

• refl: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F x x
• symm: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F x y → CommRingCat.Colimits.Relation F y x
• trans: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F x y → CommRingCat.Colimits.Relation F y z → CommRingCat.Colimits.Relation F x z
• map: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j j' : J) (f : j ⟶ j') (x : ↑(F.obj j)), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j' ((F.map f) x)) (CommRingCat.Colimits.Prequotient.of j x)
• zero: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j 0) CommRingCat.Colimits.Prequotient.zero
• one: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j 1) CommRingCat.Colimits.Prequotient.one
• neg: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J) (x : ↑(F.obj j)), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j (-x)) (CommRingCat.Colimits.Prequotient.of j x).neg
• add: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J) (x y : ↑(F.obj j)), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j (x + y)) ((CommRingCat.Colimits.Prequotient.of j x).add (CommRingCat.Colimits.Prequotient.of j y))
• mul: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J) (x y : ↑(F.obj j)), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j (x * y)) ((CommRingCat.Colimits.Prequotient.of j x).mul (CommRingCat.Colimits.Prequotient.of j y))
• neg_1: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x x' : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F x x' → CommRingCat.Colimits.Relation F x.neg x'.neg
• add_1: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x x' y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F x x' → CommRingCat.Colimits.Relation F (x.add y) (x'.add y)
• add_2: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y y' : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F y y' → CommRingCat.Colimits.Relation F (x.add y) (x.add y')
• mul_1: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x x' y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F x x' → CommRingCat.Colimits.Relation F (x.mul y) (x'.mul y)
• mul_2: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y y' : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F y y' → CommRingCat.Colimits.Relation F (x.mul y) (x.mul y')
• zero_add: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.zero.add x) x
• add_zero: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.add CommRingCat.Colimits.Prequotient.zero) x
• one_mul: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.one.mul x) x
• mul_one: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.mul CommRingCat.Colimits.Prequotient.one) x
• neg_add_cancel: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.neg.add x) CommRingCat.Colimits.Prequotient.zero
• add_comm: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.add y) (y.add x)
• mul_comm: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.mul y) (y.mul x)
• add_assoc: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F ((x.add y).add z) (x.add (y.add z))
• mul_assoc: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F ((x.mul y).mul z) (x.mul (y.mul z))
• left_distrib: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.mul (y.add z)) ((x.mul y).add (x.mul z))
• right_distrib: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F ((x.add y).mul z) ((x.mul z).add (y.mul z))
• zero_mul: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.zero.mul x) CommRingCat.Colimits.Prequotient.zero
• mul_zero: ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F (x.mul CommRingCat.Colimits.Prequotient.zero) CommRingCat.Colimits.Prequotient.zero

instance CommRingCat.Colimits.colimitSetoid {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Setoid (CommRingCat.Colimits.Prequotient F)

The setoid corresponding to commutative expressions modulo monoid Relations and identifications.

Equations

• CommRingCat.Colimits.colimitSetoid F = { r := CommRingCat.Colimits.Relation F, iseqv := ⋯ }

def CommRingCat.Colimits.ColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Type v

The underlying type of the colimit of a diagram in CommRingCat.

Equations

• CommRingCat.Colimits.ColimitType F = Quotient (CommRingCat.Colimits.colimitSetoid F)

instance CommRingCat.Colimits.ColimitType.instZero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Zero (CommRingCat.Colimits.ColimitType F)

Equations

• CommRingCat.Colimits.ColimitType.instZero F = { zero := ⟦CommRingCat.Colimits.Prequotient.zero⟧ }

instance CommRingCat.Colimits.ColimitType.instAdd {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Add (CommRingCat.Colimits.ColimitType F)

Equations

• CommRingCat.Colimits.ColimitType.instAdd F = { add := Quotient.map₂ CommRingCat.Colimits.Prequotient.add ⋯ }

instance CommRingCat.Colimits.ColimitType.instNeg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Neg (CommRingCat.Colimits.ColimitType F)

Equations

• CommRingCat.Colimits.ColimitType.instNeg F = { neg := Quotient.map CommRingCat.Colimits.Prequotient.neg ⋯ }

instance CommRingCat.Colimits.ColimitType.AddGroup {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : AddGroup (CommRingCat.Colimits.ColimitType F)

Equations

• CommRingCat.Colimits.ColimitType.AddGroup F = AddGroup.mk ⋯

instance CommRingCat.Colimits.InhabitedColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Inhabited (CommRingCat.Colimits.ColimitType F)

Equations

• CommRingCat.Colimits.InhabitedColimitType F = { default := 0 }

instance CommRingCat.Colimits.ColimitType.AddGroupWithOne {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : AddGroupWithOne (CommRingCat.Colimits.ColimitType F)

Equations

• CommRingCat.Colimits.ColimitType.AddGroupWithOne F = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance CommRingCat.Colimits.instCommRingColimitType {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : CommRing (CommRingCat.Colimits.ColimitType F)

Equations

• CommRingCat.Colimits.instCommRingColimitType F = CommRing.mk ⋯

@[simp]

theorem CommRingCat.Colimits.quot_zero {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) CommRingCat.Colimits.Prequotient.zero = 0

@[simp]

theorem CommRingCat.Colimits.quot_one {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) CommRingCat.Colimits.Prequotient.one = 1

@[simp]

theorem CommRingCat.Colimits.quot_neg {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x : CommRingCat.Colimits.Prequotient F) : Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x.neg = -Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x

@[simp]

theorem CommRingCat.Colimits.quot_add {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x : CommRingCat.Colimits.Prequotient F) (y : CommRingCat.Colimits.Prequotient F) : Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) (x.add y) = Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x + Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) y

@[simp]

theorem CommRingCat.Colimits.quot_mul {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (x : CommRingCat.Colimits.Prequotient F) (y : CommRingCat.Colimits.Prequotient F) : Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) (x.mul y) = Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x * Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) y

def CommRingCat.Colimits.colimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : CommRingCat

The bundled commutative ring giving the colimit of a diagram.

Equations

• CommRingCat.Colimits.colimit F = CommRingCat.of (CommRingCat.Colimits.ColimitType F)

def CommRingCat.Colimits.coconeFun {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (j : J) (x : ↑(F.obj j)) : CommRingCat.Colimits.ColimitType F

The function from a given commutative ring in the diagram to the colimit commutative ring.

Equations

• CommRingCat.Colimits.coconeFun F j x = Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) (CommRingCat.Colimits.Prequotient.of j x)

def CommRingCat.Colimits.coconeMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (j : J) : F.obj j ⟶ CommRingCat.Colimits.colimit F

The ring homomorphism from a given commutative ring in the diagram to the colimit commutative ring.

Equations

• CommRingCat.Colimits.coconeMorphism F j = { toFun := CommRingCat.Colimits.coconeFun F j, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CommRingCat.Colimits.cocone_naturality {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) {j : J} {j' : J} (f : j ⟶ j') : CategoryTheory.CategoryStruct.comp (F.map f) (CommRingCat.Colimits.coconeMorphism F j') = CommRingCat.Colimits.coconeMorphism F j

@[simp]

theorem CommRingCat.Colimits.cocone_naturality_components {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (j : J) (j' : J) (f : j ⟶ j') (x : ↑(F.obj j)) : (CommRingCat.Colimits.coconeMorphism F j') ((F.map f) x) = (CommRingCat.Colimits.coconeMorphism F j) x

def CommRingCat.Colimits.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit commutative ring.

Equations

• CommRingCat.Colimits.colimitCocone F = { pt := CommRingCat.Colimits.colimit F, ι := { app := CommRingCat.Colimits.coconeMorphism F, naturality := ⋯ } }

def CommRingCat.Colimits.descFunLift {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (s : CategoryTheory.Limits.Cocone F) : CommRingCat.Colimits.Prequotient F → ↑s.pt

The function from the free commutative ring on the diagram to the cone point of any other cocone.

Equations

• CommRingCat.Colimits.descFunLift F s (CommRingCat.Colimits.Prequotient.of j x_1) = (s.ι.app j) x_1
• CommRingCat.Colimits.descFunLift F s CommRingCat.Colimits.Prequotient.zero = 0
• CommRingCat.Colimits.descFunLift F s CommRingCat.Colimits.Prequotient.one = 1
• CommRingCat.Colimits.descFunLift F s x_1.neg = -CommRingCat.Colimits.descFunLift F s x_1
• CommRingCat.Colimits.descFunLift F s (x_1.add y) = CommRingCat.Colimits.descFunLift F s x_1 + CommRingCat.Colimits.descFunLift F s y
• CommRingCat.Colimits.descFunLift F s (x_1.mul y) = CommRingCat.Colimits.descFunLift F s x_1 * CommRingCat.Colimits.descFunLift F s y

def CommRingCat.Colimits.descFun {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (s : CategoryTheory.Limits.Cocone F) : CommRingCat.Colimits.ColimitType F → ↑s.pt

The function from the colimit commutative ring to the cone point of any other cocone.

Equations

• CommRingCat.Colimits.descFun F s = Quot.lift (CommRingCat.Colimits.descFunLift F s) ⋯

def CommRingCat.Colimits.descMorphism {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) (s : CategoryTheory.Limits.Cocone F) : CommRingCat.Colimits.colimit F ⟶ s.pt

The ring homomorphism from the colimit commutative ring to the cone point of any other cocone.

Equations

• CommRingCat.Colimits.descMorphism F s = { toFun := CommRingCat.Colimits.descFun F s, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def CommRingCat.Colimits.colimitIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) : CategoryTheory.Limits.IsColimit (CommRingCat.Colimits.colimitCocone F)

Evidence that the proposed colimit is the colimit.

Equations

• CommRingCat.Colimits.colimitIsColimit F = { desc := fun (s : CategoryTheory.Limits.Cocone F) => CommRingCat.Colimits.descMorphism F s, fac := ⋯, uniq := ⋯ }

instance CommRingCat.Colimits.hasColimits_commRingCat : CategoryTheory.Limits.HasColimits CommRingCat

Equations

• CommRingCat.Colimits.hasColimits_commRingCat = ⋯