English
Let α be a Ring with LinearOrder and IsStrictOrderedRing, and let ceil: α → ℤ be such that gc_ceil_coe holds with the natural embedding. Then there exists a FloorRing α whose ceil is the given ceil function and whose floor is defined by floor(a) = − ceil(−a); the necessary adjunctions are satisfied.
Русский
Пусть α — кольцо с линейным порядком и строгим упорядоченным кольцом, и пусть ceil: α → ℤ удовлетворяет условию gc_ceil_coe совместно с внедрением. Тогда существует FloorRing α, у которого функция ceil заданная, а floor(a) = − ceil(−a); выполняются необходимые условия сопряжённости.
LaTeX
$$$\exists\text{ FloorRing }\alpha\text{ such that }\text{ceil}=\text{ceil},\; \text{floor}(a)=-\text{ceil}(-a)\text{ and }\text{gc\_ceil\_coe}\text{ holds with }\mathbb{Z}\hookrightarrow\alpha.$$$
Lean4
/-- A `FloorRing` constructor from the `ceil` function alone. -/
def ofCeil (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (ceil : α → ℤ)
(gc_ceil_coe : GaloisConnection ceil (↑)) : FloorRing α :=
{ floor := fun a => -ceil (-a)
ceil
gc_coe_floor := fun a z => by rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]
gc_ceil_coe }
