Revision 65a1391a0106c9204fe45bc73a039f056558cb83 authored by Yaël Dillies on 30 October 2023, 15:07:49 UTC, committed by Yaël Dillies on 30 October 2023, 15:07:49 UTC
Left commutativity and cardinality of `list.filter`/`multiset.filter`/`finset.filter`. Interaction of `count`/`countp` and `attach`.
1 parent 3365b20
map_floor.lean
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import algebra.order.hom.ring
import data.polynomial.reverse
/-!
# Floors and ceils aren't preserved under ordered ring homomorphisms
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
Intuitively, if `f : α → β` is an ordered ring homomorphism, then floors and ceils should be
preserved by `f` because:
* `f` preserves the naturals/integers in `α` and `β` because it's a ring hom.
* `f` preserves what's between `n` and `n + 1` because it's monotone.
However, there is a catch. Potentially something whose floor was `n` could
get mapped to `n + 1`, and this has floor `n + 1`, not `n`. Note that this is at most an off by one
error.
This pathology disappears if you require `f` to be strictly monotone or `α` to be archimedean.
## The counterexample
Consider `ℤ[ε]` (`int_with_epsilons`), the integers with infinitesimals adjoined. This is a linearly
ordered commutative floor ring (`int_with_epsilons.linear_ordered_comm_ring`,
`int_with_epsilons.floor_ring`).
The map `f : ℤ[ε] → ℤ` that forgets about the epsilons (`int_with_epsilons.forget_epsilons`) is an
ordered ring homomorphism.
But it does not preserve floors (nor ceils) as `⌊-ε⌋ = -1` while `⌊f (-ε)⌋ = ⌊0⌋ = 0`
(`int_with_epsilons.forget_epsilons_floor_lt`, `int_with_epsilons.lt_forget_epsilons_ceil`).
-/
namespace counterexample
noncomputable theory
open function int polynomial
open_locale polynomial
/-- The integers with infinitesimals adjoined. -/
@[derive [comm_ring, nontrivial, inhabited]] def int_with_epsilon := ℤ[X]
local notation `ℤ[ε]` := int_with_epsilon
local notation `ε` := (X : ℤ[ε])
namespace int_with_epsilon
instance : linear_order ℤ[ε] := linear_order.lift' (to_lex ∘ coeff) coeff_injective
instance : ordered_add_comm_group ℤ[ε] :=
by refine (to_lex.injective.comp coeff_injective).ordered_add_comm_group _ _ _ _ _ _ _;
refl <|> intros; ext; simp [←nsmul_eq_mul, ←zsmul_eq_mul]
lemma pos_iff {p : ℤ[ε]} : 0 < p ↔ 0 < p.trailing_coeff :=
begin
rw trailing_coeff,
refine ⟨_, λ h,
⟨p.nat_trailing_degree, λ m hm, (coeff_eq_zero_of_lt_nat_trailing_degree hm).symm, h⟩⟩,
rintro ⟨n, hn⟩,
convert hn.2,
exact (nat_trailing_degree_le_of_ne_zero hn.2.ne').antisymm
(le_nat_trailing_degree (by { rintro rfl, cases hn.2.false }) $ λ m hm, (hn.1 _ hm).symm),
end
instance : linear_ordered_comm_ring ℤ[ε] :=
{ zero_le_one := or.inr ⟨0, by simp⟩,
mul_pos := λ p q, by { simp_rw [pos_iff, trailing_coeff_mul], exact mul_pos },
..int_with_epsilon.linear_order, ..int_with_epsilon.comm_ring,
..int_with_epsilon.ordered_add_comm_group, ..int_with_epsilon.nontrivial }
instance : floor_ring ℤ[ε] :=
floor_ring.of_floor _ (λ p, if (p.coeff 0 : ℤ[ε]) ≤ p then p.coeff 0 else p.coeff 0 - 1) $ λ p q,
begin
simp_rw [←not_lt, not_iff_not],
split,
{ split_ifs,
{ rintro ⟨_ | n, hn⟩,
{ refine (sub_one_lt _).trans _,
simpa using hn },
{ dsimp at hn,
simp [hn.1 _ n.zero_lt_succ] } },
{ exact λ h', cast_lt.1 ((not_lt.1 h).trans_lt h') } },
{ split_ifs,
{ exact λ h', h.trans_le (cast_le.2 $ sub_one_lt_iff.1 h') },
{ exact λ h', ⟨0, by simpa using h'⟩ } }
end
/-- The ordered ring homomorphisms from `ℤ[ε]` to `ℤ` that "forgets" the `ε`s. -/
def forget_epsilons : ℤ[ε] →+*o ℤ :=
{ to_fun := λ p, coeff p 0,
map_zero' := coeff_zero _,
map_one' := coeff_one_zero,
map_add' := λ _ _, coeff_add _ _ _,
map_mul' := mul_coeff_zero,
monotone' := monotone_iff_forall_lt.2 begin
rintro p q ⟨n, hn⟩,
cases n,
{ exact hn.2.le },
{ exact (hn.1 _ n.zero_lt_succ).le }
end }
@[simp] lemma forget_epsilons_apply (p : ℤ[ε]) : forget_epsilons p = coeff p 0 := rfl
/-- The floor of `n - ε` is `n - 1` but its image under `forget_epsilons` is `n`, whose floor is
itself. -/
lemma forget_epsilons_floor_lt (n : ℤ) :
forget_epsilons ⌊(n - ε : ℤ[ε])⌋ < ⌊forget_epsilons (n - ε)⌋ :=
begin
suffices : ⌊(n - ε : ℤ[ε])⌋ = n - 1,
{ simp [this] },
have : (0 : ℤ[ε]) < ε := ⟨1, by simp⟩,
exact (if_neg $ by simp [this]).trans (by simp),
end
/-- The ceil of `n + ε` is `n + 1` but its image under `forget_epsilons` is `n`, whose ceil is
itself. -/
lemma lt_forget_epsilons_ceil (n : ℤ) :
⌈forget_epsilons (n + ε)⌉ < forget_epsilons ⌈(n + ε : ℤ[ε])⌉ :=
begin
rw [←neg_lt_neg_iff, ←map_neg, ←cast_neg, ←floor_neg, ←floor_neg, ←map_neg, neg_add', ←cast_neg],
exact forget_epsilons_floor_lt _,
end
end int_with_epsilon
end counterexample
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...