The category of commutative rings has all colimits.
This file uses a "pre-automated" approach, just as for Mon/colimits.lean.
It is a very uniform approach, that conceivably could be synthesised directly
by a tactic that analyses the shape of comm_ring and ring_hom.
We build the colimit of a diagram in CommRing 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.
- of : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (j : J), ↥(F.obj j) → CommRing.colimits.prequotient F
- zero : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing), CommRing.colimits.prequotient F
- one : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing), CommRing.colimits.prequotient F
- neg : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing), CommRing.colimits.prequotient F → CommRing.colimits.prequotient F
- add : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing), CommRing.colimits.prequotient F → CommRing.colimits.prequotient F → CommRing.colimits.prequotient F
- mul : Π {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing), CommRing.colimits.prequotient F → CommRing.colimits.prequotient F → CommRing.colimits.prequotient F
An inductive type representing all commutative ring expressions (without relations)
on a collection of types indexed by the objects of J.
@[instance]
def
CommRing.colimits.inhabited
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
Equations
inductive
CommRing.colimits.relation
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
- refl : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x : CommRing.colimits.prequotient F), CommRing.colimits.relation F x x
- symm : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y : CommRing.colimits.prequotient F), CommRing.colimits.relation F x y → CommRing.colimits.relation F y x
- trans : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y z : CommRing.colimits.prequotient F), CommRing.colimits.relation F x y → CommRing.colimits.relation F y z → CommRing.colimits.relation F x z
- map : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (j j' : J) (f : j ⟶ j') (x : ↥(F.obj j)), CommRing.colimits.relation F (CommRing.colimits.prequotient.of j' (⇑(F.map f) x)) (CommRing.colimits.prequotient.of j x)
- zero : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (j : J), CommRing.colimits.relation F (CommRing.colimits.prequotient.of j 0) CommRing.colimits.prequotient.zero
- one : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (j : J), CommRing.colimits.relation F (CommRing.colimits.prequotient.of j 1) CommRing.colimits.prequotient.one
- neg : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (j : J) (x : ↥(F.obj j)), CommRing.colimits.relation F (CommRing.colimits.prequotient.of j (-x)) (CommRing.colimits.prequotient.of j x).neg
- add : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (j : J) (x y : ↥(F.obj j)), CommRing.colimits.relation F (CommRing.colimits.prequotient.of j (x + y)) ((CommRing.colimits.prequotient.of j x).add (CommRing.colimits.prequotient.of j y))
- mul : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (j : J) (x y : ↥(F.obj j)), CommRing.colimits.relation F (CommRing.colimits.prequotient.of j (x * y)) ((CommRing.colimits.prequotient.of j x).mul (CommRing.colimits.prequotient.of j y))
- neg_1 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x x' : CommRing.colimits.prequotient F), CommRing.colimits.relation F x x' → CommRing.colimits.relation F x.neg x'.neg
- add_1 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x x' y : CommRing.colimits.prequotient F), CommRing.colimits.relation F x x' → CommRing.colimits.relation F (x.add y) (x'.add y)
- add_2 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y y' : CommRing.colimits.prequotient F), CommRing.colimits.relation F y y' → CommRing.colimits.relation F (x.add y) (x.add y')
- mul_1 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x x' y : CommRing.colimits.prequotient F), CommRing.colimits.relation F x x' → CommRing.colimits.relation F (x.mul y) (x'.mul y)
- mul_2 : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y y' : CommRing.colimits.prequotient F), CommRing.colimits.relation F y y' → CommRing.colimits.relation F (x.mul y) (x.mul y')
- zero_add : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x : CommRing.colimits.prequotient F), CommRing.colimits.relation F (CommRing.colimits.prequotient.zero.add x) x
- add_zero : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x : CommRing.colimits.prequotient F), CommRing.colimits.relation F (x.add CommRing.colimits.prequotient.zero) x
- one_mul : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x : CommRing.colimits.prequotient F), CommRing.colimits.relation F (CommRing.colimits.prequotient.one.mul x) x
- mul_one : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x : CommRing.colimits.prequotient F), CommRing.colimits.relation F (x.mul CommRing.colimits.prequotient.one) x
- add_left_neg : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x : CommRing.colimits.prequotient F), CommRing.colimits.relation F (x.neg.add x) CommRing.colimits.prequotient.zero
- add_comm : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y : CommRing.colimits.prequotient F), CommRing.colimits.relation F (x.add y) (y.add x)
- mul_comm : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y : CommRing.colimits.prequotient F), CommRing.colimits.relation F (x.mul y) (y.mul x)
- add_assoc : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y z : CommRing.colimits.prequotient F), CommRing.colimits.relation F ((x.add y).add z) (x.add (y.add z))
- mul_assoc : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y z : CommRing.colimits.prequotient F), CommRing.colimits.relation F ((x.mul y).mul z) (x.mul (y.mul z))
- left_distrib : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y z : CommRing.colimits.prequotient F), CommRing.colimits.relation F (x.mul (y.add z)) ((x.mul y).add (x.mul z))
- right_distrib : ∀ {J : Type v} [_inst_1 : category_theory.small_category J] (F : J ⥤ CommRing) (x y z : CommRing.colimits.prequotient F), CommRing.colimits.relation F ((x.add y).mul z) ((x.mul z).add (y.mul z))
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.
@[instance]
def
CommRing.colimits.colimit_setoid
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
The setoid corresponding to commutative expressions modulo monoid relations and identifications.
Equations
- CommRing.colimits.colimit_setoid F = {r := CommRing.colimits.relation F, iseqv := _}
The underlying type of the colimit of a diagram in CommRing.
Equations
@[instance]
def
CommRing.colimits.colimit_type.inhabited
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
@[instance]
def
CommRing.colimits.comm_ring
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
Equations
- CommRing.colimits.comm_ring F = {add := quot.lift (λ (x : CommRing.colimits.prequotient F), quot.lift (λ (y : CommRing.colimits.prequotient F), quot.mk setoid.r (x.add y)) _) _, add_assoc := _, zero := quot.mk setoid.r CommRing.colimits.prequotient.zero, zero_add := _, add_zero := _, neg := quot.lift (λ (x : CommRing.colimits.prequotient F), quot.mk setoid.r x.neg) _, add_left_neg := _, add_comm := _, mul := quot.lift (λ (x : CommRing.colimits.prequotient F), quot.lift (λ (y : CommRing.colimits.prequotient F), quot.mk setoid.r (x.mul y)) _) _, mul_assoc := _, one := quot.mk setoid.r CommRing.colimits.prequotient.one, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[simp]
theorem
CommRing.colimits.quot_zero
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
quot.mk setoid.r CommRing.colimits.prequotient.zero = 0
@[simp]
theorem
CommRing.colimits.quot_one
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
quot.mk setoid.r CommRing.colimits.prequotient.one = 1
@[simp]
theorem
CommRing.colimits.quot_neg
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(x : CommRing.colimits.prequotient F) :
@[simp]
theorem
CommRing.colimits.quot_add
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(x y : CommRing.colimits.prequotient F) :
@[simp]
theorem
CommRing.colimits.quot_mul
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(x y : CommRing.colimits.prequotient F) :
The bundled commutative ring giving the colimit of a diagram.
Equations
def
CommRing.colimits.cocone_fun
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(j : J) :
↥(F.obj j) → CommRing.colimits.colimit_type F
The function from a given commutative ring in the diagram to the colimit commutative ring.
Equations
- CommRing.colimits.cocone_fun F j x = quot.mk setoid.r (CommRing.colimits.prequotient.of j x)
def
CommRing.colimits.cocone_morphism
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(j : J) :
F.obj j ⟶ CommRing.colimits.colimit F
The ring homomorphism from a given commutative ring in the diagram to the colimit commutative ring.
Equations
- CommRing.colimits.cocone_morphism F j = {to_fun := CommRing.colimits.cocone_fun F j, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
CommRing.colimits.cocone_naturality
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
{j j' : J}
(f : j ⟶ j') :
@[simp]
theorem
CommRing.colimits.cocone_naturality_components
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(j j' : J)
(f : j ⟶ j')
(x : ↥(F.obj j)) :
⇑(CommRing.colimits.cocone_morphism F j') (⇑(F.map f) x) = ⇑(CommRing.colimits.cocone_morphism F j) x
def
CommRing.colimits.colimit_cocone
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
The cocone over the proposed colimit commutative ring.
Equations
- CommRing.colimits.colimit_cocone F = {X := CommRing.colimits.colimit F, ι := {app := CommRing.colimits.cocone_morphism F, naturality' := _}}
@[simp]
def
CommRing.colimits.desc_fun_lift
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(s : category_theory.limits.cocone F) :
CommRing.colimits.prequotient F → ↥(s.X)
The function from the free commutative ring on the diagram to the cone point of any other cocone.
Equations
- CommRing.colimits.desc_fun_lift F s (x.mul y) = CommRing.colimits.desc_fun_lift F s x * CommRing.colimits.desc_fun_lift F s y
- CommRing.colimits.desc_fun_lift F s (x.add y) = CommRing.colimits.desc_fun_lift F s x + CommRing.colimits.desc_fun_lift F s y
- CommRing.colimits.desc_fun_lift F s x.neg = -CommRing.colimits.desc_fun_lift F s x
- CommRing.colimits.desc_fun_lift F s CommRing.colimits.prequotient.one = 1
- CommRing.colimits.desc_fun_lift F s CommRing.colimits.prequotient.zero = 0
- CommRing.colimits.desc_fun_lift F s (CommRing.colimits.prequotient.of j x) = ⇑(s.ι.app j) x
def
CommRing.colimits.desc_fun
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(s : category_theory.limits.cocone F) :
CommRing.colimits.colimit_type F → ↥(s.X)
The function from the colimit commutative ring to the cone point of any other cocone.
Equations
- CommRing.colimits.desc_fun F s = quot.lift (CommRing.colimits.desc_fun_lift F s) _
def
CommRing.colimits.desc_morphism
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing)
(s : category_theory.limits.cocone F) :
The ring homomorphism from the colimit commutative ring to the cone point of any other cocone.
Equations
- CommRing.colimits.desc_morphism F s = {to_fun := CommRing.colimits.desc_fun F s, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
def
CommRing.colimits.colimit_is_colimit
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ CommRing) :
Evidence that the proposed colimit is the colimit.
Equations
- CommRing.colimits.colimit_is_colimit F = {desc := λ (s : category_theory.limits.cocone F), CommRing.colimits.desc_morphism F s, fac' := _, uniq' := _}
@[instance]
Equations
- CommRing.colimits.has_colimits_CommRing = {has_colimits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_colimit := λ (F : J ⥤ CommRing), {cocone := CommRing.colimits.colimit_cocone F, is_colimit := CommRing.colimits.colimit_is_colimit F}}}