From 744e79c1fe89480f28a8d9df029e15f27ee1def4 Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 4 Mar 2021 21:18:02 +0000 Subject: [PATCH] feat(algebra/ordered_*, */sub{monoid,group,ring,semiring,field,algebra}): pullback of ordered algebraic structures under an injective map (#6489) Prove that the following 14 order typeclasses can be pulled back via an injective map (`function.injective.*`), and use them to attach 30 new instances to sub-objects: * `ordered_comm_monoid` (and the implied `ordered_add_comm_monoid`) * `submonoid.to_ordered_comm_monoid` * `submodule.to_ordered_add_comm_monoid` * `ordered_comm_group` (and the implied `ordered_add_comm_group`) * `subgroup.to_ordered_comm_group` * `submodule.to_ordered_add_comm_group` * `ordered_cancel_comm_monoid` (and the implied `ordered_cancel_add_comm_monoid`) * `submonoid.to_ordered_cancel_comm_monoid` * `submodule.to_ordered_cancel_add_comm_monoid` * `linear_ordered_cancel_comm_monoid` (and the implied `linear_ordered_cancel_add_comm_monoid`) * `submonoid.to_linear_ordered_cancel_comm_monoid` * `submodule.to_linear_ordered_cancel_add_comm_monoid` * `linear_ordered_comm_monoid_with_zero` * (no suitable subobject exists for monoid_with_zero) * `linear_ordered_comm_group` (and the implied `linear_ordered_add_comm_group`) * `subgroup.to_linear_ordered_comm_group` * `submodule.to_linear_ordered_add_comm_group` * `ordered_semiring` * `subsemiring.to_ordered_semiring` * `subalgebra.to_ordered_semiring` * `ordered_comm_semiring` * `subsemiring.to_ordered_comm_semiring` * `subalgebra.to_ordered_comm_semiring` * `ordered_ring` * `subring.to_ordered_ring` * `subalgebra.to_ordered_ring` * `ordered_comm_ring` * `subring.to_ordered_comm_ring` * `subalgebra.to_ordered_comm_ring` * `linear_ordered_semiring` * `subring.to_linear_ordered_semiring` * `subalgebra.to_linear_ordered_semiring` * `linear_ordered_ring` * `subring.to_linear_ordered_ring` * `subalgebra.to_linear_ordered_ring` * `linear_ordered_comm_ring` * `subring.to_linear_ordered_comm_ring` * `subalgebra.to_linear_ordered_comm_ring` * `linear_ordered_field` * `subfield.to_linear_ordered_field` Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rings.20from.20subtype Co-authored-by: Eric Wieser --- src/algebra/algebra/subalgebra.lean | 24 ++++++ .../linear_ordered_comm_group_with_zero.lean | 12 +++ src/algebra/module/submodule.lean | 44 ++++++++++ src/algebra/ordered_field.lean | 12 +++ src/algebra/ordered_group.lean | 27 ++++++ src/algebra/ordered_monoid.lean | 40 +++++++++ src/algebra/ordered_ring.lean | 85 +++++++++++++++++++ src/field_theory/subfield.lean | 6 ++ src/group_theory/subgroup.lean | 13 +++ src/group_theory/submonoid/operations.lean | 22 +++++ src/ring_theory/subring.lean | 21 +++++ src/ring_theory/subsemiring.lean | 16 ++++ 12 files changed, 322 insertions(+) diff --git a/src/algebra/algebra/subalgebra.lean b/src/algebra/algebra/subalgebra.lean index 70b8102381a03..003130d4176a3 100644 --- a/src/algebra/algebra/subalgebra.lean +++ b/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 := diff --git a/src/algebra/linear_ordered_comm_group_with_zero.lean b/src/algebra/linear_ordered_comm_group_with_zero.lean index 16010c8c4a2c0..1049a41dbebde 100644 --- a/src/algebra/linear_ordered_comm_group_with_zero.lean +++ b/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, diff --git a/src/algebra/module/submodule.lean b/src/algebra/module/submodule.lean index e963afbeb2f71..82f4c8c707202 100644 --- a/src/algebra/module/submodule.lean +++ b/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 diff --git a/src/algebra/ordered_field.lean b/src/algebra/ordered_field.lean index ecc1f67bf4c31..b27827e30df0b 100644 --- a/src/algebra/ordered_field.lean +++ b/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] diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean index 863ac48bcc6b8..26b37f4f5ef0a 100644 --- a/src/algebra/ordered_group.lean +++ b/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 := diff --git a/src/algebra/ordered_monoid.lean b/src/algebra/ordered_monoid.lean index de6ead14e17fc..9ee661bc2550b 100644 --- a/src/algebra/ordered_monoid.lean +++ 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 diff --git a/src/algebra/ordered_ring.lean b/src/algebra/ordered_ring.lean index 8de14353aef37..654041d206035 100644 --- a/src/algebra/ordered_ring.lean +++ b/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 {β : 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 {β : 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 {β : 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 diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean index 35bcae9fd6b82..e9f99c84ee183 100644 --- a/src/field_theory/subfield.lean +++ b/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 diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean index f8446416cf211..44ff3281a3e9e 100644 --- a/src/group_theory/subgroup.lean +++ b/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⟩ diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean index 5b6093b82fec5..0b9d1eacd1349 100644 --- a/src/group_theory/submonoid/operations.lean +++ b/src/group_theory/submonoid/operations.lean @@ -332,6 +332,28 @@ an `add_comm_monoid`."] instance to_comm_monoid {M} [comm_monoid M] (S : submonoid M) : comm_monoid S := S.coe_injective.comm_monoid coe rfl (λ _ _, rfl) +/-- A submonoid of a `ordered_comm_monoid` is a `ordered_comm_monoid`. -/ +@[to_additive "An `add_submonoid` of an `ordered_add_comm_monoid` is +an `ordered_add_comm_monoid`."] +instance to_ordered_comm_monoid {M} [ordered_comm_monoid M] (S : submonoid M) : + ordered_comm_monoid S := +S.coe_injective.ordered_comm_monoid coe rfl (λ _ _, rfl) + +/-- A submonoid of an `ordered_cancel_comm_monoid` is an `ordered_cancel_comm_monoid`. -/ +@[to_additive "An `add_submonoid` of an `ordered_cancel_add_comm_monoid` is +an `ordered_cancel_add_comm_monoid`."] +instance to_ordered_cancel_comm_monoid {M} [ordered_cancel_comm_monoid M] (S : submonoid M) : + ordered_cancel_comm_monoid S := +S.coe_injective.ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) + +/-- A submonoid of a `linear_ordered_cancel_comm_monoid` is a `linear_ordered_cancel_comm_monoid`. +-/ +@[to_additive "An `add_submonoid` of a `linear_ordered_cancel_add_comm_monoid` is +a `linear_ordered_cancel_add_comm_monoid`."] +instance to_linear_ordered_cancel_comm_monoid {M} [linear_ordered_cancel_comm_monoid M] + (S : submonoid M) : linear_ordered_cancel_comm_monoid S := +S.coe_injective.linear_ordered_cancel_comm_monoid coe rfl (λ _ _, rfl) + /-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/ @[to_additive "The natural monoid hom from an `add_submonoid` of `add_monoid` `M` to `M`."] def subtype : S →* M := ⟨coe, rfl, λ _ _, rfl⟩ diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean index eeeab989aeab2..b87c731d52a57 100644 --- a/src/ring_theory/subring.lean +++ b/src/ring_theory/subring.lean @@ -254,6 +254,27 @@ s.to_subsemiring.no_zero_divisors instance {R} [integral_domain R] (s : subring R) : integral_domain s := { .. s.nontrivial, .. s.no_zero_divisors, .. s.to_comm_ring } +/-- A subring of an `ordered_ring` is an `ordered_ring`. -/ +instance to_ordered_ring {R} [ordered_ring R] (s : subring R) : ordered_ring s := +subtype.coe_injective.ordered_ring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) + +/-- A subring of an `ordered_comm_ring` is an `ordered_comm_ring`. -/ +instance to_ordered_comm_ring {R} [ordered_comm_ring R] (s : subring R) : ordered_comm_ring s := +subtype.coe_injective.ordered_comm_ring coe rfl rfl + (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) + +/-- A subring of a `linear_ordered_ring` is a `linear_ordered_ring`. -/ +instance to_linear_ordered_ring {R} [linear_ordered_ring R] (s : subring R) : + linear_ordered_ring s := +subtype.coe_injective.linear_ordered_ring coe rfl rfl + (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) + +/-- A subring of a `linear_ordered_comm_ring` is a `linear_ordered_comm_ring`. -/ +instance to_linear_ordered_comm_ring {R} [linear_ordered_comm_ring R] (s : subring R) : + linear_ordered_comm_ring s := +subtype.coe_injective.linear_ordered_comm_ring coe rfl rfl + (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) + /-- The natural ring hom from a subring of ring `R` to `R`. -/ def subtype (s : subring R) : s →+* R := { to_fun := coe, diff --git a/src/ring_theory/subsemiring.lean b/src/ring_theory/subsemiring.lean index 1480140f08ed5..2820b7c220d3b 100644 --- a/src/ring_theory/subsemiring.lean +++ b/src/ring_theory/subsemiring.lean @@ -180,6 +180,22 @@ def subtype : s →+* R := @[simp] theorem coe_subtype : ⇑s.subtype = coe := rfl +/-- A subsemiring of an `ordered_semiring` is an `ordered_semiring`. -/ +instance to_ordered_semiring {R} [ordered_semiring R] (s : subsemiring R) : ordered_semiring s := +subtype.coe_injective.ordered_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) + +/-- A subsemiring of an `ordered_comm_semiring` is an `ordered_comm_semiring`. -/ +instance to_ordered_comm_semiring {R} [ordered_comm_semiring R] (s : subsemiring R) : + ordered_comm_semiring s := +subtype.coe_injective.ordered_comm_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) + +/-- A subsemiring of a `linear_ordered_semiring` is a `linear_ordered_semiring`. -/ +instance to_linear_ordered_semiring {R} [linear_ordered_semiring R] (s : subsemiring R) : + linear_ordered_semiring s := +subtype.coe_injective.linear_ordered_semiring coe rfl rfl (λ _ _, rfl) (λ _ _, rfl) + +/-! Note: currently, there is no `linear_ordered_comm_semiring`. -/ + instance : partial_order (subsemiring R) := { le := λ s t, ∀ ⦃x⦄, x ∈ s → x ∈ t, .. partial_order.lift (coe : subsemiring R → set R) ext' }