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.
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
Instances For
Equations
- RingCat.Colimits.instInhabitedPrequotient F = { default := RingCat.Colimits.Prequotient.zero }
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
Instances For
The setoid corresponding to commutative expressions modulo monoid Relations and identifications.
Equations
- RingCat.Colimits.colimitSetoid F = { r := RingCat.Colimits.Relation F, iseqv := ⋯ }
The underlying type of the colimit of a diagram in CommRingCat
.
Equations
Instances For
Equations
- RingCat.Colimits.ColimitType.instZero F = { zero := ⟦RingCat.Colimits.Prequotient.zero⟧ }
Equations
- RingCat.Colimits.ColimitType.instAdd F = { add := Quotient.map₂ RingCat.Colimits.Prequotient.add ⋯ }
Equations
- RingCat.Colimits.ColimitType.instNeg F = { neg := Quotient.map RingCat.Colimits.Prequotient.neg ⋯ }
Equations
Equations
- RingCat.Colimits.InhabitedColimitType F = { default := 0 }
Equations
- RingCat.Colimits.ColimitType.AddGroupWithOne F = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- RingCat.Colimits.instRingColimitType F = Ring.mk ⋯ AddGroupWithOne.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The bundled ring giving the colimit of a diagram.
Equations
Instances For
The function from a given ring in the diagram to the colimit ring.
Equations
- RingCat.Colimits.coconeFun F j x = Quot.mk Setoid.r (RingCat.Colimits.Prequotient.of j x)
Instances For
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' := ⋯ }
Instances For
The cocone over the proposed colimit ring.
Equations
- RingCat.Colimits.colimitCocone F = { pt := RingCat.Colimits.colimit F, ι := { app := RingCat.Colimits.coconeMorphism F, naturality := ⋯ } }
Instances For
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
Instances For
The function from the colimit ring to the cone point of any other cocone.
Equations
Instances For
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' := ⋯ }
Instances For
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 := ⋯ }
Instances For
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.
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
Instances For
Equations
- CommRingCat.Colimits.instInhabitedPrequotient F = { default := CommRingCat.Colimits.Prequotient.zero }
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
Instances For
The setoid corresponding to commutative expressions modulo monoid Relations and identifications.
Equations
- CommRingCat.Colimits.colimitSetoid F = { r := CommRingCat.Colimits.Relation F, iseqv := ⋯ }
The underlying type of the colimit of a diagram in CommRingCat
.
Instances For
Equations
- CommRingCat.Colimits.ColimitType.instZero F = { zero := ⟦CommRingCat.Colimits.Prequotient.zero⟧ }
Equations
- CommRingCat.Colimits.ColimitType.instAdd F = { add := Quotient.map₂ CommRingCat.Colimits.Prequotient.add ⋯ }
Equations
- CommRingCat.Colimits.ColimitType.instNeg F = { neg := Quotient.map CommRingCat.Colimits.Prequotient.neg ⋯ }
Equations
Equations
- CommRingCat.Colimits.InhabitedColimitType F = { default := 0 }
Equations
- CommRingCat.Colimits.ColimitType.AddGroupWithOne F = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
The bundled commutative ring giving the colimit of a diagram.
Instances For
The function from a given commutative ring in the diagram to the colimit commutative ring.
Equations
- CommRingCat.Colimits.coconeFun F j x = Quot.mk Setoid.r (CommRingCat.Colimits.Prequotient.of j x)
Instances For
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' := ⋯ }
Instances For
The cocone over the proposed colimit commutative ring.
Equations
- CommRingCat.Colimits.colimitCocone F = { pt := CommRingCat.Colimits.colimit F, ι := { app := CommRingCat.Colimits.coconeMorphism F, naturality := ⋯ } }
Instances For
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
Instances For
The function from the colimit commutative ring to the cone point of any other cocone.
Equations
Instances For
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' := ⋯ }
Instances For
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 := ⋯ }