[Merged by Bors] - feat(algebra/ordered_*, */sub{monoid,group,ring,semiring,field,algebra}): pullback of ordered algebraic structures under an injective map

src/algebra/algebra/subalgebra.lean

@@ -166,6 +166,30 @@ instance to_comm_ring {R A}
   [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) :
   comm_ring S := S.to_subring.to_comm_ring
 
+instance to_ordered_semiring {R A}
+  [comm_semiring R] [ordered_semiring A] [algebra R A] (S : subalgebra R A) :
+  ordered_semiring S := S.to_subsemiring.to_ordered_semiring
+instance to_ordered_comm_semiring {R A}
+  [comm_semiring R] [ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
+  ordered_comm_semiring S := subsemiring.to_ordered_comm_semiring S
+instance to_ordered_ring {R A}
+  [comm_ring R] [ordered_ring A] [algebra R A] (S : subalgebra R A) :
+  ordered_ring S := S.to_subring.to_ordered_ring
+instance to_ordered_comm_ring {R A}
+  [comm_ring R] [ordered_comm_ring A] [algebra R A] (S : subalgebra R A) :
+  ordered_comm_ring S := S.to_subring.to_ordered_comm_ring
+
+instance to_linear_ordered_semiring {R A}
+  [comm_semiring R] [linear_ordered_semiring A] [algebra R A] (S : subalgebra R A) :
+  linear_ordered_semiring S := S.to_subsemiring.to_linear_ordered_semiring
+/-! There is no `linear_ordered_comm_semiring`. -/
+instance to_linear_ordered_ring {R A}
+  [comm_ring R] [linear_ordered_ring A] [algebra R A] (S : subalgebra R A) :
+  linear_ordered_ring S := S.to_subring.to_linear_ordered_ring
+instance to_linear_ordered_comm_ring {R A}
+  [comm_ring R] [linear_ordered_comm_ring A] [algebra R A] (S : subalgebra R A) :
+  linear_ordered_comm_ring S := S.to_subring.to_linear_ordered_comm_ring
+
 end
 
 instance algebra : algebra R S :=

src/algebra/linear_ordered_comm_group_with_zero.lean

@@ -42,6 +42,18 @@ variables [linear_ordered_comm_monoid_with_zero α]
 The following facts are true more generally in a (linearly) ordered commutative monoid.
 -/
 
+/-- Pullback a `linear_ordered_comm_monoid_with_zero` under an injective map. -/
+def function.injective.linear_ordered_comm_monoid_with_zero {β : Type*}
+  [has_zero β] [has_one β] [has_mul β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (mul : ∀ x y, f (x * y) = f x * f y) :
+  linear_ordered_comm_monoid_with_zero β :=
+{ zero_le_one := show f 0 ≤ f 1, by simp only [zero, one,
+    linear_ordered_comm_monoid_with_zero.zero_le_one],
+  ..linear_order.lift f hf,
+  ..hf.ordered_comm_monoid f one mul,
+  ..hf.comm_monoid_with_zero f zero one mul }
+
 lemma one_le_pow_of_one_le' {n : ℕ} (H : 1 ≤ x) : 1 ≤ x^n :=
 begin
   induction n with n ih,

src/algebra/module/submodule.lean

@@ -199,6 +199,50 @@ instance : add_comm_group p :=
 
 end add_comm_group
 
+section ordered_monoid
+
+variables [semiring R]
+
+/-- A submodule of an `ordered_add_comm_monoid` is an `ordered_add_comm_monoid`. -/
+instance to_ordered_add_comm_monoid
+  {M} [ordered_add_comm_monoid M] [semimodule R M] (S : submodule R M) :
+  ordered_add_comm_monoid S :=
+subtype.coe_injective.ordered_add_comm_monoid coe rfl (λ _ _, rfl)
+
+/-- A submodule of an `ordered_cancel_add_comm_monoid` is an `ordered_cancel_add_comm_monoid`. -/
+instance to_ordered_cancel_add_comm_monoid
+  {M} [ordered_cancel_add_comm_monoid M] [semimodule R M] (S : submodule R M) :
+  ordered_cancel_add_comm_monoid S :=
+subtype.coe_injective.ordered_cancel_add_comm_monoid coe rfl (λ _ _, rfl)
+
+/-- A submodule of a `linear_ordered_cancel_add_comm_monoid` is a
+`linear_ordered_cancel_add_comm_monoid`. -/
+instance to_linear_ordered_cancel_add_comm_monoid
+  {M} [linear_ordered_cancel_add_comm_monoid M] [semimodule R M] (S : submodule R M) :
+  linear_ordered_cancel_add_comm_monoid S :=
+subtype.coe_injective.linear_ordered_cancel_add_comm_monoid coe rfl (λ _ _, rfl)
+
+end ordered_monoid
+
+section ordered_group
+
+variables [ring R]
+
+/-- A submodule of an `ordered_add_comm_group` is an `ordered_add_comm_group`. -/
+instance to_ordered_add_comm_group
+  {M} [ordered_add_comm_group M] [semimodule R M] (S : submodule R M) :
+  ordered_add_comm_group S :=
+subtype.coe_injective.ordered_add_comm_group coe rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
+
+/-- A submodule of a `linear_ordered_add_comm_group` is a
+`linear_ordered_add_comm_group`. -/
+instance to_linear_ordered_add_comm_group
+  {M} [linear_ordered_add_comm_group M] [semimodule R M] (S : submodule R M) :
+  linear_ordered_add_comm_group S :=
+subtype.coe_injective.linear_ordered_add_comm_group coe rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
+
+end ordered_group
+
 end submodule
 
 namespace submodule

src/algebra/ordered_field.lean

@@ -553,6 +553,18 @@ end
 ### Miscellaneous lemmas
 -/
 
+/-- Pullback a `linear_ordered_field` under an injective map. -/
+def function.injective.linear_ordered_field {β : Type*}
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_inv β] [has_div β]
+  [nontrivial β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
+  (inv : ∀ x, f (x⁻¹) = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y) :
+  linear_ordered_field β :=
+{ ..hf.linear_ordered_ring f zero one add mul neg sub,
+  ..hf.field f zero one add mul neg sub inv div}
+
 lemma mul_sub_mul_div_mul_neg_iff (hc : c ≠ 0) (hd : d ≠ 0) :
   (a * d - b * c) / (c * d) < 0 ↔ a / c < b / d :=
 by rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_lt_zero]

src/algebra/ordered_group.lean

@@ -407,6 +407,20 @@ by simp [div_eq_mul_inv]
 @[simp, to_additive] lemma div_lt_self_iff (a : α) {b : α} : a / b < a ↔ 1 < b :=
 by simp [div_eq_mul_inv]
 
+/-- Pullback an `ordered_comm_group` under an injective map. -/
+@[to_additive function.injective.ordered_add_comm_group
+"Pullback an `ordered_add_comm_group` under an injective map."]
+def function.injective.ordered_comm_group {β : Type*}
+  [has_one β] [has_mul β] [has_inv β] [has_div β]
+  (f : β → α) (hf : function.injective f) (one : f 1 = 1)
+  (mul : ∀ x y, f (x * y) = f x * f y)
+  (inv : ∀ x, f (x⁻¹) = (f x)⁻¹)
+  (div : ∀ x y, f (x / y) = f x / f y) :
+  ordered_comm_group β :=
+{ ..partial_order.lift f hf,
+  ..hf.ordered_comm_monoid f one mul,
+  ..hf.comm_group_div f one mul inv div }
+
 end ordered_comm_group
 
 section ordered_add_comm_group
@@ -570,6 +584,19 @@ instance linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid :
   mul_right_cancel := λ x y z, mul_right_cancel,
   ..‹linear_ordered_comm_group α› }
 
+/-- Pullback a `linear_ordered_comm_group` under an injective map. -/
+@[to_additive function.injective.linear_ordered_add_comm_group
+"Pullback a `linear_ordered_add_comm_group` under an injective map."]
+def function.injective.linear_ordered_comm_group {β : Type*}
+  [has_one β] [has_mul β] [has_inv β] [has_div β]
+  (f : β → α) (hf : function.injective f) (one : f 1 = 1)
+  (mul : ∀ x y, f (x * y) = f x * f y)
+  (inv : ∀ x, f (x⁻¹) = (f x)⁻¹)
+  (div : ∀ x y, f (x / y) = f x / f y)  :
+  linear_ordered_comm_group β :=
+{ ..linear_order.lift f hf,
+  ..hf.ordered_comm_group f one mul inv div }
+
 @[to_additive linear_ordered_add_comm_group.add_lt_add_left]
 lemma linear_ordered_comm_group.mul_lt_mul_left'
   (a b : α) (h : a < b) (c : α) : c * a < c * b :=

src/algebra/ordered_monoid.lean

@@ -264,6 +264,21 @@ iff.intro
    and.intro ‹a = 1› ‹b = 1›)
   (assume ⟨ha', hb'⟩, by rw [ha', hb', mul_one])
 
+/-- Pullback an `ordered_comm_monoid` under an injective map. -/
+@[to_additive function.injective.ordered_add_comm_monoid
+"Pullback an `ordered_add_comm_monoid` under an injective map."]
+def function.injective.ordered_comm_monoid {β : Type*}
+  [has_one β] [has_mul β]
+  (f : β → α) (hf : function.injective f) (one : f 1 = 1)
+  (mul : ∀ x y, f (x * y) = f x * f y) :
+  ordered_comm_monoid β :=
+{ mul_le_mul_left := λ a b ab c,
+    show f (c * a) ≤ f (c * b), by simp [mul, mul_le_mul_left' ab],
+  lt_of_mul_lt_mul_left :=
+    λ a b c bc, @lt_of_mul_lt_mul_left' _ _ (f a) _ _ (by rwa [← mul, ← mul]),
+  ..partial_order.lift f hf,
+  ..hf.comm_monoid f one mul }
+
 section mono
 
 variables {β : Type*} [preorder β] {f g : β → α}
@@ -964,6 +979,20 @@ by split; apply le_antisymm; try {assumption};
    rw ← hab; simp [ha, hb],
 λ ⟨ha', hb'⟩, by rw [ha', hb', mul_one]⟩
 
+/-- Pullback an `ordered_cancel_comm_monoid` under an injective map. -/
+@[to_additive function.injective.ordered_cancel_add_comm_monoid
+"Pullback an `ordered_cancel_add_comm_monoid` under an injective map."]
+def function.injective.ordered_cancel_comm_monoid {β : Type*}
+  [has_one β] [has_mul β]
+  (f : β → α) (hf : function.injective f) (one : f 1 = 1)
+  (mul : ∀ x y, f (x * y) = f x * f y) :
+  ordered_cancel_comm_monoid β :=
+{ le_of_mul_le_mul_left := λ a b c (ab : f (a * b) ≤ f (a * c)),
+    (by { rw [mul, mul] at ab, exact le_of_mul_le_mul_left' ab }),
+  ..hf.left_cancel_semigroup f mul,
+  ..hf.right_cancel_semigroup f mul,
+  ..hf.ordered_comm_monoid f one mul }
+
 section mono
 
 variables {β : Type*} [preorder β] {f g : β → α}
@@ -1089,6 +1118,17 @@ min_le_iff.2 $ or.inr $ le_mul_of_one_le_left' ha
 lemma max_le_mul_of_one_le {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : max a b ≤ a * b :=
 max_le_iff.2 ⟨le_mul_of_one_le_right' hb, le_mul_of_one_le_left' ha⟩
 
+/-- Pullback a `linear_ordered_cancel_comm_monoid` under an injective map. -/
+@[to_additive function.injective.linear_ordered_cancel_add_comm_monoid
+"Pullback a `linear_ordered_cancel_add_comm_monoid` under an injective map."]
+def function.injective.linear_ordered_cancel_comm_monoid {β : Type*}
+  [has_one β] [has_mul β]
+  (f : β → α) (hf : function.injective f) (one : f 1 = 1)
+  (mul : ∀ x y, f (x * y) = f x * f y) :
+  linear_ordered_cancel_comm_monoid β :=
+{ ..linear_order.lift f hf,
+  ..hf.ordered_cancel_comm_monoid f one mul }
+
 end linear_ordered_cancel_comm_monoid
 
 namespace order_dual

src/algebra/ordered_ring.lean

@@ -148,6 +148,28 @@ lemma one_le_mul_of_one_le_of_one_le {a b : α} (a1 : 1 ≤ a) (b1 : 1 ≤ b) :
   (1 : α) ≤ a * b :=
 (mul_one (1 : α)).symm.le.trans (mul_le_mul a1 b1 zero_le_one (zero_le_one.trans a1))
 
+/-- Pullback an `ordered_semiring` under an injective map. -/
+def function.injective.ordered_semiring {β : Type*}
+  [has_zero β] [has_one β] [has_add β] [has_mul β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) :
+  ordered_semiring β :=
+{ zero_le_one := show f 0 ≤ f 1, by  simp only [zero, one, zero_le_one],
+  mul_lt_mul_of_pos_left := λ  a b c ab c0, show f (c * a) < f (c * b),
+    begin
+      rw [mul, mul],
+      refine mul_lt_mul_of_pos_left ab _,
+      rwa ← zero,
+    end,
+  mul_lt_mul_of_pos_right := λ a b c ab c0, show f (a * c) < f (b * c),
+    begin
+      rw [mul, mul],
+      refine mul_lt_mul_of_pos_right ab _,
+      rwa ← zero,
+    end,
+  ..hf.ordered_cancel_add_comm_monoid f zero add,
+  ..hf.semiring f zero one add mul }
+
 section
 variable [nontrivial α]
 
@@ -216,6 +238,15 @@ multiplication with a positive number and addition are monotone. -/
 @[protect_proj]
 class ordered_comm_semiring (α : Type u) extends ordered_semiring α, comm_semiring α
 
+/-- Pullback an `ordered_comm_semiring` under an injective map. -/
+def function.injective.ordered_comm_semiring [ordered_comm_semiring α] {β : Type*}
+  [has_zero β] [has_one β] [has_add β] [has_mul β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) :
+  ordered_comm_semiring β :=
+{ ..hf.comm_semiring f zero one add mul,
+  ..hf.ordered_semiring f zero one add mul }
+
 end ordered_comm_semiring
 
 /--
@@ -444,6 +475,16 @@ instance linear_ordered_semiring.to_no_top_order {α : Type*} [linear_ordered_se
   no_top_order α :=
 ⟨assume a, ⟨a + 1, lt_add_of_pos_right _ zero_lt_one⟩⟩
 
+/-- Pullback a `linear_ordered_semiring` under an injective map. -/
+def function.injective.linear_ordered_semiring [linear_ordered_semiring α] {β : Type*}
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [nontrivial β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y) :
+  linear_ordered_semiring β :=
+{ ..linear_order.lift f hf,
+  ..‹nontrivial β›,
+  ..hf.ordered_semiring f zero one add mul }
+
 end linear_ordered_semiring
 
 section mono
@@ -605,6 +646,17 @@ lemma mul_pos_of_neg_of_neg {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b :=
 have 0 * b < a * b, from mul_lt_mul_of_neg_right ha hb,
 by rwa zero_mul at this
 
+/-- Pullback an `ordered_ring` under an injective map. -/
+def function.injective.ordered_ring {β : Type*}
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (- x) = - f x) (sub : ∀ x y, f (x - y) = f x - f y) :
+  ordered_ring β :=
+{ mul_pos := λ a b a0 b0, show f 0 < f (a * b), by { rw [zero, mul], apply mul_pos; rwa ← zero },
+  ..hf.ordered_semiring f zero one add mul,
+  ..hf.ring_sub f zero one add mul neg sub }
+
 end ordered_ring
 
 section ordered_comm_ring
@@ -614,6 +666,17 @@ multiplication with a positive number and addition are monotone. -/
 @[protect_proj]
 class ordered_comm_ring (α : Type u) extends ordered_ring α, ordered_comm_semiring α, comm_ring α
 
+/-- Pullback an `ordered_comm_ring` under an injective map. -/
+def function.injective.ordered_comm_ring [ordered_comm_ring α] {β : Type*}
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (- x) = - f x) (sub : ∀ x y, f (x - y) = f x - f y) :
+  ordered_comm_ring β :=
+{ ..hf.ordered_comm_semiring f zero one add mul,
+  ..hf.ordered_ring f zero one add mul neg sub,
+  ..hf.comm_ring_sub f zero one add mul neg sub }
+
 end ordered_comm_ring
 
 /-- A `linear_ordered_ring α` is a ring `α` with a linear order such that
@@ -807,6 +870,17 @@ end
 lemma abs_le_one_iff_mul_self_le_one : abs a ≤ 1 ↔ a * a ≤ 1 :=
 by simpa only [abs_one, one_mul] using @abs_le_iff_mul_self_le α _ a 1
 
+/-- Pullback a `linear_ordered_ring` under an injective map. -/
+def function.injective.linear_ordered_ring [linear_ordered_ring α] {β : Type*}
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [nontrivial β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) :
+  linear_ordered_ring β :=
+{ ..linear_order.lift f hf,
+  ..‹nontrivial β›,
+  ..hf.ordered_ring f zero one add mul neg sub }
+
 end linear_ordered_ring
 
 /-- A `linear_ordered_comm_ring α` is a commutative ring `α` with a linear order
@@ -872,6 +946,17 @@ begin
   simp [left_distrib, right_distrib, add_assoc, add_comm, add_left_comm, mul_comm, sub_eq_add_neg],
 end
 
+/-- Pullback a `linear_ordered_comm_ring` under an injective map. -/
+def function.injective.linear_ordered_comm_ring [linear_ordered_comm_ring α] {β : Type*}
+  [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [nontrivial β]
+  (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1)
+  (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+  (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) :
+  linear_ordered_comm_ring β :=
+{ ..linear_order.lift f hf,
+  ..‹nontrivial β›,
+  ..hf.ordered_comm_ring f zero one add mul neg sub }
+
 end linear_ordered_comm_ring
 
 /-- Extend `nonneg_add_comm_group` to support ordered rings

src/field_theory/subfield.lean

@@ -199,6 +199,12 @@ instance to_field : field s :=
 subtype.coe_injective.field coe
   rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
 
+/-- A subfield of a `linear_ordered_field` is a `linear_ordered_field`. -/
+instance to_linear_ordered_field {K} [linear_ordered_field K] (s : subfield K) :
+  linear_ordered_field s :=
+subtype.coe_injective.linear_ordered_field coe
+  rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
+
 @[simp, norm_cast] lemma coe_add (x y : s) : (↑(x + y) : K) = ↑x + ↑y := rfl
 @[simp, norm_cast] lemma coe_sub (x y : s) : (↑(x - y) : K) = ↑x - ↑y := rfl
 @[simp, norm_cast] lemma coe_neg (x : s) : (↑(-x) : K) = -↑x := rfl

src/group_theory/subgroup.lean

@@ -306,6 +306,19 @@ subtype.coe_injective.group_div _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
 instance to_comm_group {G : Type*} [comm_group G] (H : subgroup G) : comm_group H :=
 subtype.coe_injective.comm_group_div _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
 
+/-- A subgroup of an `ordered_comm_group` is an `ordered_comm_group`. -/
+@[to_additive "An `add_subgroup` of an `add_ordered_comm_group` is an `add_ordered_comm_group`."]
+instance to_ordered_comm_group {G : Type*} [ordered_comm_group G] (H : subgroup G) :
+  ordered_comm_group H :=
+subtype.coe_injective.ordered_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
+
+/-- A subgroup of a `linear_ordered_comm_group` is a `linear_ordered_comm_group`. -/
+@[to_additive "An `add_subgroup` of a `linear_ordered_add_comm_group` is a
+  `linear_ordered_add_comm_group`."]
+instance to_linear_ordered_comm_group {G : Type*} [linear_ordered_comm_group G]
+  (H : subgroup G) : linear_ordered_comm_group H :=
+subtype.coe_injective.linear_ordered_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
+
 /-- The natural group hom from a subgroup of group `G` to `G`. -/
 @[to_additive "The natural group hom from an `add_subgroup` of `add_group` `G` to `G`."]
 def subtype : H →* G := ⟨coe, rfl, λ _ _, rfl⟩