doc-next-gen

Mathlib.Algebra.Order.Ring.InjSurj

Module docstring

{"# Pulling back ordered rings along injective maps "}

Function.Injective.isOrderedRing theorem
[IsOrderedRing R] (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) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : letI _ : Semiring S := hf.semiring f zero one add mul nsmul npow natCast letI _ : PartialOrder S := PartialOrder.lift f hf IsOrderedRing S
Full source 
/-- Pullback an `IsOrderedRing` under an injective map. -/
protected lemma isOrderedRing [IsOrderedRing R] (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)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) :
    letI _ : Semiring S := hf.semiring f zero one add mul nsmul npow natCast
    letI _ : PartialOrder S := PartialOrder.lift f hf
    IsOrderedRing S :=
  letI _ : Semiring S := hf.semiring f zero one add mul nsmul npow natCast
  letI _ : PartialOrder S := PartialOrder.lift f hf
  { __ := hf.isOrderedAddMonoid f zero add (swap nsmul)
    zero_le_one := show f 0 ≤ f 1 by simp only [zero, one, zero_le_one]
    mul_le_mul_of_nonneg_left a b c h hc := show f (c * a) ≤ f (c * b) by
      rw [mul, mul]; refine mul_le_mul_of_nonneg_left h ?_; rwa [← zero]
    mul_le_mul_of_nonneg_right a b c h hc := show f (a * c) ≤ f (b * c) by
      rw [mul, mul]; refine mul_le_mul_of_nonneg_right h ?_; rwa [← zero] }
Pullback of Ordered Semiring Structure Along Injective Homomorphism
Informal description
Let $R$ be an ordered semiring and $f : R \to S$ be an injective function. Suppose $f$ preserves the following operations and constants: - $f(0) = 0$ - $f(1) = 1$ - $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ - $f(x^n) = f(x)^n$ for all $x \in R$ and $n \in \mathbb{N}$ - $f(n) = n$ for all $n \in \mathbb{N}$ Then $S$ can be equipped with a semiring structure and a partial order induced by $f$, making $S$ an ordered semiring.
Function.Injective.isStrictOrderedRing theorem
[IsStrictOrderedRing R] (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) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (natCast : ∀ n : ℕ, f n = n) : letI _ : Semiring S := hf.semiring f zero one add mul nsmul npow natCast letI _ : PartialOrder S := PartialOrder.lift f hf IsStrictOrderedRing S
Full source 
/-- Pullback a `IsStrictOrderedRing` under an injective map. -/
protected lemma isStrictOrderedRing [IsStrictOrderedRing R] (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)
    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (natCast : ∀ n : ℕ, f n = n) :
    letI _ : Semiring S := hf.semiring f zero one add mul nsmul npow natCast
    letI _ : PartialOrder S := PartialOrder.lift f hf
    IsStrictOrderedRing S :=
  letI _ : Semiring S := hf.semiring f zero one add mul nsmul npow natCast
  letI _ : PartialOrder S := PartialOrder.lift f hf
  { __ := hf.isOrderedCancelAddMonoid f zero add (swap nsmul)
    __ := domain_nontrivial f zero one
    __ := hf.isOrderedRing f zero one add mul nsmul npow natCast
    mul_lt_mul_of_pos_left a b c h hc := show f (c * a) < f (c * b) by
      simpa only [mul, zero] using mul_lt_mul_of_pos_left ‹f a < f b› (by rwa [← zero])
    mul_lt_mul_of_pos_right a b c h hc := show f (a * c) < f (b * c) by
      simpa only [mul, zero] using mul_lt_mul_of_pos_right ‹f a < f b› (by rwa [← zero]) }
Pullback of Strict Ordered Semiring Structure Along Injective Homomorphism
Informal description
Let $R$ be a strict ordered semiring and $f : R \to S$ be an injective function. Suppose $f$ preserves the following operations and constants: - $f(0) = 0$ - $f(1) = 1$ - $f(x + y) = f(x) + f(y)$ for all $x, y \in R$ - $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in R$ - $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{N}$ and $x \in R$ - $f(x^n) = f(x)^n$ for all $x \in R$ and $n \in \mathbb{N}$ - $f(n) = n$ for all $n \in \mathbb{N}$ Then $S$ can be equipped with a semiring structure and a partial order induced by $f$, making $S$ a strict ordered semiring.