English
Let α be a field equipped with a linear order and a strict ordered-ring structure, β a ring, and abv: β → α an absolute value. Consider CauSeq β abv, the Cauchy sequences in β with respect to abv, and Cauchy abv, its completion. There is a canonical map mk: CauSeq β abv → Cauchy abv sending a Cauchy sequence to its image in the completion. The construction embeds β into the completion via ofRat x := mk(const abv x). The completion carries natural ring operations, scalar actions, and functorial properties induced by evaluating these operations termwise on representatives of the Cauchy sequences. In particular, the distinguished elements 0 and 1 arise from the zero and unit in β via ofRat, and all algebraic operations on the completion are defined so that mk respects these operations.
Русский
Пусть α — поле с линейным порядком и строгой упорядоченной структурой кольца, β — кольцо, abv: β → α — абсолютная величина. Пусть CauSeq β abv обозначает последовательности Коши в β по отношению к abv, а Cauchy abv — их завершение. Существует каноническое отображение mk: CauSeq β abv → Cauchy abv, отправляющее последовательность в её образ в завершении. От β в завершение имеется вложение через ofRat x := mk(const abv x). В завершении задаются естественные арифметические операции, действие скаляров и прочие конструктивные свойства, полученные покомпонентной реализацией операций над представительствами последовательностей. В частности 0 и 1 в завершении получаются из нулевого и единичного элементов β через ofRat, и все операции согласованы с mk.
LaTeX
$$$\operatorname{mk}: \mathrm{CauSeq}(\beta,abv) \to \mathrm{Cauchy}(abv)$$$
Lean4
/-- The map from Cauchy sequences into the Cauchy completion. -/
def mk : CauSeq _ abv → Cauchy abv :=
Quotient.mk''
