feat(order/bounded_order): define with_bot.map and with_top.map (#…

…14163)

Also define `monotone.with_bot` etc.

src/algebra/order/monoid.lean

@@ -1037,6 +1037,31 @@ coe_lt_top 0
   (0 : with_top α) < a ↔ 0 < a :=
 coe_lt_coe
 
+/-- A version of `with_top.map` for `one_hom`s. -/
+@[to_additive "A version of `with_top.map` for `zero_hom`s", simps { fully_applied := ff }]
+protected def _root_.one_hom.with_top_map {M N : Type*} [has_one M] [has_one N] (f : one_hom M N) :
+  one_hom (with_top M) (with_top N) :=
+{ to_fun := with_top.map f,
+  map_one' := by rw [with_top.map_one, map_one, coe_one] }
+
+/-- A version of `with_top.map` for `add_hom`s. -/
+@[simps { fully_applied := ff }] protected def _root_.add_hom.with_top_map
+  {M N : Type*} [has_add M] [has_add N] (f : add_hom M N) :
+  add_hom (with_top M) (with_top N) :=
+{ to_fun := with_top.map f,
+  map_add' := λ x y, match x, y with
+    ⊤, y := by rw [top_add, map_top, top_add],
+    x, ⊤ := by rw [add_top, map_top, add_top],
+    (x : M), (y : M) := by simp only [← coe_add, map_coe, map_add]
+  end }
+
+/-- A version of `with_top.map` for `add_monoid_hom`s. -/
+@[simps { fully_applied := ff }] protected def _root_.add_monoid_hom.with_top_map
+  {M N : Type*} [add_zero_class M] [add_zero_class N] (f : M →+ N) :
+  with_top M →+ with_top N :=
+{ to_fun := with_top.map f,
+  .. f.to_zero_hom.with_top_map, .. f.to_add_hom.with_top_map }
+
 end with_top
 
 namespace with_bot

src/algebra/order/ring.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
 import algebra.order.group
 import algebra.order.sub
+import algebra.hom.ring
 import data.set.intervals.basic
 
 /-!
@@ -1587,6 +1588,26 @@ instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_top
   end,
   .. with_top.mul_zero_class }
 
+/-- A version of `with_top.map` for `monoid_with_zero_hom`s. -/
+@[simps { fully_applied := ff }] protected def _root_.monoid_with_zero_hom.with_top_map
+  {R S : Type*} [mul_zero_one_class R] [decidable_eq R] [nontrivial R]
+  [mul_zero_one_class S] [decidable_eq S] [nontrivial S] (f : R →*₀ S) (hf : function.injective f) :
+  with_top R →*₀ with_top S :=
+{ to_fun := with_top.map f,
+  map_mul' := λ x y,
+    begin
+      have : ∀ z, map f z = 0 ↔ z = 0,
+        from λ z, (option.map_injective hf).eq_iff' f.to_zero_hom.with_top_map.map_zero,
+      rcases eq_or_ne x 0 with rfl|hx, { simp },
+      rcases eq_or_ne y 0 with rfl|hy, { simp },
+      induction x using with_top.rec_top_coe, { simp [hy, this] },
+      induction y using with_top.rec_top_coe,
+      { have : (f x : with_top S) ≠ 0, by simpa [hf.eq_iff' (map_zero f)] using hx,
+        simp [hx, this] },
+      simp [← coe_mul]
+    end,
+  .. f.to_zero_hom.with_top_map, .. f.to_monoid_hom.to_one_hom.with_top_map }
+
 instance [mul_zero_class α] [no_zero_divisors α] : no_zero_divisors (with_top α) :=
 ⟨λ a b, by cases a; cases b; dsimp [mul_def]; split_ifs;
   simp [*, none_eq_top, some_eq_coe, mul_eq_zero] at *⟩
@@ -1648,6 +1669,15 @@ instance [nontrivial α] : canonically_ordered_comm_semiring (with_top α) :=
   .. with_top.canonically_ordered_add_monoid,
   .. with_top.no_zero_divisors, }
 
+/-- A version of `with_top.map` for `ring_hom`s. -/
+@[simps { fully_applied := ff }] protected def _root_.ring_hom.with_top_map
+  {R S : Type*} [canonically_ordered_comm_semiring R] [decidable_eq R] [nontrivial R]
+  [canonically_ordered_comm_semiring S] [decidable_eq S] [nontrivial S]
+  (f : R →+* S) (hf : function.injective f) :
+  with_top R →+* with_top S :=
+{ to_fun := with_top.map f,
+  .. f.to_monoid_with_zero_hom.with_top_map hf, .. f.to_add_monoid_hom.with_top_map }
+
 end with_top
 
 namespace with_bot

src/logic/embedding.lean

@@ -183,6 +183,11 @@ def option_embedding_equiv (α β) : (option α ↪ β) ≃ Σ f : α ↪ β, 
   left_inv := λ f, ext $ by { rintro (_|_); simp [option.coe_def] },
   right_inv := λ ⟨f, y, hy⟩, by { ext; simp [option.coe_def] } }
 
+/-- A version of `option.map` for `function.embedding`s. -/
+@[simps { fully_applied := ff }]
+def option_map {α β} (f : α ↪ β) : option α ↪ option β :=
+⟨option.map f, option.map_injective f.injective⟩
+
 /-- Embedding of a `subtype`. -/
 def subtype {α} (p : α → Prop) : subtype p ↪ α :=
 ⟨coe, λ _ _, subtype.ext_val⟩

src/order/bounded_order.lean

@@ -521,11 +521,11 @@ option.rec h₁ h₂
 
 @[norm_cast] lemma coe_eq_coe : (a : with_bot α) = b ↔ a = b := option.some_inj
 
--- the `by exact` here forces the type of the equality to be `@eq (with_bot α)`
-@[simp] lemma map_bot (f : α → β) :
-  (by exact option.map f (⊥ : with_bot α)) = (⊥ : with_bot β) := rfl
-lemma map_coe (f : α → β) (a : α) :
-  (by exact option.map f (a : with_bot α)) = (f a : with_bot β) := rfl
+/-- Lift a map `f : α → β` to `with_bot α → with_bot β`. Implemented using `option.map`. -/
+def map (f : α → β) : with_bot α → with_bot β := option.map f
+
+@[simp] lemma map_bot (f : α → β) : map f ⊥ = ⊥ := rfl
+@[simp] lemma map_coe (f : α → β) (a : α) : map f a = f a := rfl
 
 lemma ne_bot_iff_exists {x : with_bot α} : x ≠ ⊥ ↔ ∃ (a : α), ↑a = x := option.ne_none_iff_exists
 
@@ -674,11 +674,11 @@ lemma coe_sup [semilattice_sup α] (a b : α) : ((a ⊔ b : α) : with_bot α) =
 instance [semilattice_inf α] : semilattice_inf (with_bot α) :=
 { inf          := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a ⊓ b)),
   inf_le_left  := λ o₁ o₂ a ha, begin
-    simp at ha, rcases ha with ⟨b, rfl, c, rfl, rfl⟩,
+    simp [map] at ha, rcases ha with ⟨b, rfl, c, rfl, rfl⟩,
     exact ⟨_, rfl, inf_le_left⟩
   end,
   inf_le_right := λ o₁ o₂ a ha, begin
-    simp at ha, rcases ha with ⟨b, rfl, c, rfl, rfl⟩,
+    simp [map] at ha, rcases ha with ⟨b, rfl, c, rfl, rfl⟩,
     exact ⟨_, rfl, inf_le_right⟩
   end,
   le_inf       := λ o₁ o₂ o₃ h₁ h₂ a ha, begin
@@ -808,11 +808,11 @@ option.rec h₁ h₂
 
 @[norm_cast] lemma coe_eq_coe : (a : with_top α) = b ↔ a = b := option.some_inj
 
--- the `by exact` here forces the type of the equality to be `@eq (with_top α)`
-@[simp] lemma map_top (f : α → β) :
-  (by exact option.map f (⊤ : with_top α)) = (⊤ : with_top β) := rfl
-lemma map_coe (f : α → β) (a : α) :
-  (by exact option.map f (a : with_top α)) = (f a : with_top β) := rfl
+/-- Lift a map `f : α → β` to `with_top α → with_top β`. Implemented using `option.map`. -/
+def map (f : α → β) : with_top α → with_top β := option.map f
+
+@[simp] lemma map_top (f : α → β) : map f ⊤ = ⊤ := rfl
+@[simp] lemma map_coe (f : α → β) (a : α) : map f a = f a := rfl
 
 lemma ne_top_iff_exists {x : with_top α} : x ≠ ⊤ ↔ ∃ (a : α), ↑a = x := option.ne_none_iff_exists
 
@@ -939,11 +939,11 @@ lemma coe_inf [semilattice_inf α] (a b : α) : ((a ⊓ b : α) : with_top α) =
 instance [semilattice_sup α] : semilattice_sup (with_top α) :=
 { sup          := λ o₁ o₂, o₁.bind (λ a, o₂.map (λ b, a ⊔ b)),
   le_sup_left  := λ o₁ o₂ a ha, begin
-    simp at ha, rcases ha with ⟨b, rfl, c, rfl, rfl⟩,
+    simp [map] at ha, rcases ha with ⟨b, rfl, c, rfl, rfl⟩,
     exact ⟨_, rfl, le_sup_left⟩
   end,
   le_sup_right := λ o₁ o₂ a ha, begin
-    simp at ha, rcases ha with ⟨b, rfl, c, rfl, rfl⟩,
+    simp [map] at ha, rcases ha with ⟨b, rfl, c, rfl, rfl⟩,
     exact ⟨_, rfl, le_sup_right⟩
   end,
   sup_le       := λ o₁ o₂ o₃ h₁ h₂ a ha, begin
@@ -1031,6 +1031,27 @@ end⟩
 
 end with_top
 
+section mono
+
+variables [preorder α] [preorder β] {f : α → β}
+
+protected lemma monotone.with_bot_map (hf : monotone f) : monotone (with_bot.map f)
+| ⊥       _       h := bot_le
+| (a : α) ⊥       h := (with_bot.not_coe_le_bot _ h).elim
+| (a : α) (b : α) h := with_bot.coe_le_coe.2 (hf (with_bot.coe_le_coe.1 h))
+
+protected lemma monotone.with_top_map (hf : monotone f) : monotone (with_top.map f) :=
+hf.dual.with_bot_map.dual
+
+protected lemma strict_mono.with_bot_map (hf : strict_mono f) : strict_mono (with_bot.map f)
+| ⊥       (a : α) h := with_bot.bot_lt_coe _
+| (a : α) (b : α) h := with_bot.coe_lt_coe.mpr (hf $ with_bot.coe_lt_coe.mp h)
+
+protected lemma strict_mono.with_top_map (hf : strict_mono f) : strict_mono (with_top.map f) :=
+hf.dual.with_bot_map.dual
+
+end mono
+
 /-! ### Subtype, order dual, product lattices -/
 
 namespace subtype

src/order/hom/basic.lean

@@ -363,6 +363,16 @@ def dual_iso (α β : Type*) [preorder α] [preorder β] : (α →o β) ≃o (α
 { to_equiv := order_hom.dual.trans order_dual.to_dual,
   map_rel_iff' := λ f g, iff.rfl }
 
+/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `with_bot α →o with_bot β`. -/
+@[simps { fully_applied := ff }]
+protected def with_bot_map (f : α →o β) : with_bot α →o with_bot β :=
+⟨with_bot.map f, f.mono.with_bot_map⟩
+
+/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `with_top α →o with_top β`. -/
+@[simps { fully_applied := ff }]
+protected def with_top_map (f : α →o β) : with_top α →o with_top β :=
+⟨with_top.map f, f.mono.with_top_map⟩
+
 end order_hom
 
 /-- Embeddings of partial orders that preserve `<` also preserve `≤`. -/
@@ -411,6 +421,20 @@ f.lt_embedding.is_well_order
 protected def dual : αᵒᵈ ↪o βᵒᵈ :=
 ⟨f.to_embedding, λ a b, f.map_rel_iff⟩
 
+/-- A version of `with_bot.map` for order embeddings. -/
+@[simps { fully_applied := ff }]
+protected def with_bot_map (f : α ↪o β) : with_bot α ↪o with_bot β :=
+{ to_fun := with_bot.map f,
+  map_rel_iff' := λ a b, by cases a; cases b; simp [with_bot.none_eq_bot, with_bot.some_eq_coe,
+    with_bot.not_coe_le_bot],
+  .. f.to_embedding.option_map }
+
+/-- A version of `with_top.map` for order embeddings. -/
+@[simps { fully_applied := ff }]
+protected def with_top_map (f : α ↪o β) : with_top α ↪o with_top β :=
+{ to_fun := with_top.map f,
+  .. f.dual.with_bot_map.dual }
+
 /--
 To define an order embedding from a partial order to a preorder it suffices to give a function
 together with a proof that it satisfies `f a ≤ f b ↔ a ≤ b`.
@@ -796,8 +820,7 @@ variables [partial_order α] [partial_order β] [partial_order γ]
 @[simps apply]
 def with_top_congr (e : α ≃o β) : with_top α ≃o with_top β :=
 { to_equiv := e.to_equiv.option_congr,
-  map_rel_iff' := λ x y,
-    by induction x using with_top.rec_top_coe; induction y using with_top.rec_top_coe; simp }
+  .. e.to_order_embedding.with_top_map }
 
 @[simp] lemma with_top_congr_refl : (order_iso.refl α).with_top_congr = order_iso.refl _ :=
 rel_iso.to_equiv_injective equiv.option_congr_refl
@@ -814,8 +837,7 @@ rel_iso.to_equiv_injective $ e₁.to_equiv.option_congr_trans e₂.to_equiv
 def with_bot_congr (e : α ≃o β) :
   with_bot α ≃o with_bot β :=
 { to_equiv := e.to_equiv.option_congr,
-  map_rel_iff' := λ x y,
-    by induction x using with_bot.rec_bot_coe; induction y using with_bot.rec_bot_coe; simp }
+  .. e.to_order_embedding.with_bot_map }
 
 @[simp] lemma with_bot_congr_refl : (order_iso.refl α).with_bot_congr = order_iso.refl _ :=
 rel_iso.to_equiv_injective equiv.option_congr_refl