English
Let α be a ring with a linear order that is strictly ordered, and let floor: α → ℤ satisfy that Int.cast and floor form a Galois connection. Then there exists a FloorRing structure on α in which floor is the given floor function, and the ceiling is defined by ceil(a) = − floor(−a); moreover the natural adjunction relations with the integer embedding hold.
Русский
Пусть α — кольцо с линейным порядком, являющееся строго упорядкованным, и пусть floor: α → ℤ удовлетворяет свойству, что отображения Int.cast и floor образуют галуа-сопоставление. Тогда существует структура FloorRing на α, для которой floor совпадает с заданной функцией floor, а ceiling задаётся как ceil(a) = − floor(−a); при этом выполняются соответствующие связи сопряжённости с внедрением целых в α.
LaTeX
$$$\exists\text{ FloorRing }\alpha\text{ such that }\text{floor}=\text{floor},\; \text{ceil}(a)=-\text{floor}(-a)\text{ and }\text{gc\_coe\_floor}\text{ holds with }\mathbb{Z}\hookrightarrow\alpha.$$$
Lean4
/-- A `FloorRing` constructor from the `floor` function alone. -/
def ofFloor (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (floor : α → ℤ)
(gc_coe_floor : GaloisConnection (↑) floor) : FloorRing α :=
{ floor
ceil := fun a => -floor (-a)
gc_coe_floor
gc_ceil_coe := fun a z => by rw [neg_le, ← gc_coe_floor, Int.cast_neg, neg_le_neg_iff] }
