Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Covariant definition

: Prop

Full source

/-- `Covariant` is useful to formulate succinctly statements about the interactions between an
action of a Type on another one and a relation on the acted-upon Type.

See the `CovariantClass` doc-string for its meaning. -/
def Covariant : Prop :=
  ∀ (m) {n₁ n₂}, r n₁ n₂ → r (μ m n₁) (μ m n₂)

Covariant relation with respect to a binary operation

Informal description

A relation $r$ on a type $N$ is called *covariant* with respect to a binary operation $\mu : M \to N \to N$ if for any element $m \in M$ and any elements $n_1, n_2 \in N$, the relation $r(n_1, n_2)$ implies $r(\mu(m, n_1), \mu(m, n_2))$. In other words, the operation $\mu$ preserves the relation $r$ in its second argument when the first argument is fixed.

Contravariant definition

: Prop

Full source

/-- `Contravariant` is useful to formulate succinctly statements about the interactions between an
action of a Type on another one and a relation on the acted-upon Type.

See the `ContravariantClass` doc-string for its meaning. -/
def Contravariant : Prop :=
  ∀ (m) {n₁ n₂}, r (μ m n₁) (μ m n₂) → r n₁ n₂

Contravariance of a binary operation with respect to a relation

Informal description

Given a type `M` with a binary operation `μ : M → M → M` and a relation `r` on `M`, the property `Contravariant` states that for any element `m ∈ M`, if the relation `r` holds between `μ m n₁` and `μ m n₂` for some `n₁, n₂ ∈ M`, then `r` must also hold between `n₁` and `n₂`. In other words, the operation `μ` is contravariant with respect to the relation `r` in its second argument.

CovariantClass structure

Full source

/-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the
`CovariantClass` says that "the action `μ` preserves the relation `r`."

More precisely, the `CovariantClass` is a class taking two Types `M N`, together with an "action"
`μ : M → N → N` and a relation `r : N → N → Prop`.  Its unique field `elim` is the assertion that
for all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair
`(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)`,
obtained from `(n₁, n₂)` by acting upon it by `m`.

If `m : M` and `h : r n₁ n₂`, then `CovariantClass.elim m h : r (μ m n₁) (μ m n₂)`.
-/
class CovariantClass : Prop where
  /-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair
  `(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)` -/
  protected elim : Covariant M N μ r

Covariant class of an action preserving a relation

Informal description

Given a type `M` acting on a type `N` via an operation `μ : M → N → N` and a relation `r` on `N`, the structure `CovariantClass M N μ r` asserts that for any `m ∈ M` and any `n₁, n₂ ∈ N`, if `r n₁ n₂` holds, then `r (μ m n₁) (μ m n₂)` also holds. In other words, the action `μ` preserves the relation `r` in its second argument.

ContravariantClass structure

Full source

/-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the
`ContravariantClass` says that "if the result of the action `μ` on a pair satisfies the
relation `r`, then the initial pair satisfied the relation `r`."

More precisely, the `ContravariantClass` is a class taking two Types `M N`, together with an
"action" `μ : M → N → N` and a relation `r : N → N → Prop`.  Its unique field `elim` is the
assertion that for all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the
pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation
`r` also holds for the pair `(n₁, n₂)`.

If `m : M` and `h : r (μ m n₁) (μ m n₂)`, then `ContravariantClass.elim m h : r n₁ n₂`.
-/
class ContravariantClass : Prop where
  /-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the
  pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation
  `r` also holds for the pair `(n₁, n₂)`. -/
  protected elim : Contravariant M N μ r

Contravariant Class of an Action with Respect to a Relation

Informal description

Given a type `M` acting on a type `N` via an operation `μ : M → N → N` and a relation `r` on `N`, the `ContravariantClass` structure captures the property that whenever `r(μ m n₁, μ m n₂)` holds for some `m ∈ M` and `n₁, n₂ ∈ N`, then `r(n₁, n₂)` must also hold. In other words, if applying the action preserves the relation in one direction, then the original elements must have satisfied the relation. More formally, for all `m ∈ M` and `n₁, n₂ ∈ N`, if `r(μ m n₁, μ m n₂)` holds, then `r(n₁, n₂)` holds.

MulLeftMono abbrev

[Mul M] [LE M] : Prop

Full source

/-- Typeclass for monotonicity of multiplication on the left,
namely `b₁ ≤ b₂ → a * b₁ ≤ a * b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCommMonoid`. -/
abbrev MulLeftMono [Mul M] [LE M] : Prop :=
  CovariantClass M M (· * ·) (· ≤ ·)

Left Multiplication is Monotone

Informal description

Given a type $M$ with a multiplication operation and a preorder relation $\leq$, the property `MulLeftMono` asserts that for any elements $a, b_1, b_2 \in M$, if $b_1 \leq b_2$, then $a * b_1 \leq a * b_2$. In other words, left multiplication by any fixed element $a$ is monotone with respect to the order relation $\leq$.

MulRightMono abbrev

[Mul M] [LE M] : Prop

Full source

/-- Typeclass for monotonicity of multiplication on the right,
namely `a₁ ≤ a₂ → a₁ * b ≤ a₂ * b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCommMonoid`. -/
abbrev MulRightMono [Mul M] [LE M] : Prop :=
  CovariantClass M M (swap (· * ·)) (· ≤ ·)

Right Multiplication is Monotone

Informal description

Given a type $M$ with a multiplication operation and a partial order $\leq$, the property `MulRightMono` asserts that for any elements $a, b, c \in M$, if $a \leq b$, then $a * c \leq b * c$. In other words, multiplication on the right is monotone with respect to the order relation.

AddLeftMono abbrev

[Add M] [LE M] : Prop

Full source

/-- Typeclass for monotonicity of addition on the left,
namely `b₁ ≤ b₂ → a + b₁ ≤ a + b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedAddCommMonoid`. -/
abbrev AddLeftMono [Add M] [LE M] : Prop :=
  CovariantClass M M (· + ·) (· ≤ ·)

Left-monotonicity of addition with respect to a partial order

Informal description

An additive structure `M` with a partial order `≤` is said to be *left-monotone* if for any elements `a, b₁, b₂ ∈ M`, the implication `b₁ ≤ b₂ → a + b₁ ≤ a + b₂` holds. This means that left addition preserves the order relation.

AddRightMono abbrev

[Add M] [LE M] : Prop

Full source

/-- Typeclass for monotonicity of addition on the right,
namely `a₁ ≤ a₂ → a₁ + b ≤ a₂ + b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedAddCommMonoid`. -/
abbrev AddRightMono [Add M] [LE M] : Prop :=
  CovariantClass M M (swap (· + ·)) (· ≤ ·)

Right Monotonicity of Addition with Respect to Partial Order

Informal description

For a type $M$ equipped with an addition operation and a partial order $\leq$, the property `AddRightMono` asserts that addition is right-monotonic, meaning for any $a_1, a_2, b \in M$, if $a_1 \leq a_2$ then $a_1 + b \leq a_2 + b$.

MulLeftStrictMono abbrev

[Mul M] [LT M] : Prop

Full source

/-- Typeclass for monotonicity of multiplication on the left,
namely `b₁ < b₂ → a * b₁ < a * b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCommGroup`. -/
abbrev MulLeftStrictMono [Mul M] [LT M] : Prop :=
  CovariantClass M M (· * ·) (· < ·)

Strict Left Monotonicity of Multiplication

Informal description

For a type $M$ equipped with a multiplication operation and a strict order relation $<$, the property `MulLeftStrictMono` asserts that left multiplication is strictly monotone, i.e., for any $a, b_1, b_2 \in M$, if $b_1 < b_2$ then $a * b_1 < a * b_2$.

MulRightStrictMono abbrev

[Mul M] [LT M] : Prop

Full source

/-- Typeclass for monotonicity of multiplication on the right,
namely `a₁ < a₂ → a₁ * b < a₂ * b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCommGroup`. -/
abbrev MulRightStrictMono [Mul M] [LT M] : Prop :=
  CovariantClass M M (swap (· * ·)) (· < ·)

Strict Right Monotonicity of Multiplication

Informal description

For a type $M$ equipped with a multiplication operation and a strict order relation $<$, the property `MulRightStrictMono` asserts that multiplication on the right is strictly monotone. That is, for any $a, b, c \in M$, if $a < b$ then $a * c < b * c$.

AddLeftStrictMono abbrev

[Add M] [LT M] : Prop

Full source

/-- Typeclass for monotonicity of addition on the left,
namely `b₁ < b₂ → a + b₁ < a + b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedAddCommGroup`. -/
abbrev AddLeftStrictMono [Add M] [LT M] : Prop :=
  CovariantClass M M (· + ·) (· < ·)

Strict Left Monotonicity of Addition

Informal description

For a type `M` equipped with an addition operation `+` and a strict order relation `<`, the property `AddLeftStrictMono` asserts that for any elements `a, b₁, b₂ ∈ M`, if `b₁ < b₂`, then `a + b₁ < a + b₂`. In other words, addition on the left is strictly monotone with respect to the order.

AddRightStrictMono abbrev

[Add M] [LT M] : Prop

Full source

/-- Typeclass for monotonicity of addition on the right,
namely `a₁ < a₂ → a₁ + b < a₂ + b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedAddCommGroup`. -/
abbrev AddRightStrictMono [Add M] [LT M] : Prop :=
  CovariantClass M M (swap (· + ·)) (· < ·)

Right Strict Monotonicity of Addition

Informal description

Given a type $M$ with an addition operation $+$ and a strict order relation $<$, the property `AddRightStrictMono` asserts that for any $a_1, a_2, b \in M$, if $a_1 < a_2$ then $a_1 + b < a_2 + b$.

MulLeftReflectLT abbrev

[Mul M] [LT M] : Prop

Full source

/-- Typeclass for strict reverse monotonicity of multiplication on the left,
namely `a * b₁ < a * b₂ → b₁ < b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCommGroup`. -/
abbrev MulLeftReflectLT [Mul M] [LT M] : Prop :=
  ContravariantClass M M (· * ·) (· < ·)

Left Multiplication Reflects Strict Order

Informal description

For a type `M` with a multiplication operation `*` and a strict order relation `<`, the property `MulLeftReflectLT` states that for all elements `a, b₁, b₂ ∈ M`, if `a * b₁ < a * b₂`, then `b₁ < b₂`. In other words, multiplication on the left reflects the strict order relation.

MulRightReflectLT abbrev

[Mul M] [LT M] : Prop

Full source

/-- Typeclass for strict reverse monotonicity of multiplication on the right,
namely `a₁ * b < a₂ * b → a₁ < a₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCommGroup`. -/
abbrev MulRightReflectLT [Mul M] [LT M] : Prop :=
  ContravariantClass M M (swap (· * ·)) (· < ·)

Right Multiplication Reflects Strict Order

Informal description

For a type `M` equipped with a multiplication operation `*` and a strict order relation `<`, the property `MulRightReflectLT` states that multiplication on the right reflects the strict order. That is, for any elements `a₁, a₂, b ∈ M`, if `a₁ * b < a₂ * b` holds, then `a₁ < a₂` must also hold.

AddLeftReflectLT abbrev

[Add M] [LT M] : Prop

Full source

/-- Typeclass for strict reverse monotonicity of addition on the left,
namely `a + b₁ < a + b₂ → b₁ < b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedAddCommGroup`. -/
abbrev AddLeftReflectLT [Add M] [LT M] : Prop :=
  ContravariantClass M M (· + ·) (· < ·)

Left Addition Reflects Strict Order

Informal description

For a type `M` with an addition operation `+` and a strict order relation `<`, the property `AddLeftReflectLT` states that for any elements `a, b₁, b₂ ∈ M`, if `a + b₁ < a + b₂`, then `b₁ < b₂`.

AddRightReflectLT abbrev

[Add M] [LT M] : Prop

Full source

/-- Typeclass for strict reverse monotonicity of addition on the right,
namely `a₁ * b < a₂ * b → a₁ < a₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedAddCommGroup`. -/
abbrev AddRightReflectLT [Add M] [LT M] : Prop :=
  ContravariantClass M M (swap (· + ·)) (· < ·)

Right Addition Reflects Strict Inequality

Informal description

For a type `M` equipped with an addition operation `+` and a strict order relation `<`, the property `AddRightReflectLT` states that for all `a₁, a₂, b ∈ M`, if `a₁ + b < a₂ + b` holds, then `a₁ < a₂` must also hold.

MulLeftReflectLE abbrev

[Mul M] [LE M] : Prop

Full source

/-- Typeclass for reverse monotonicity of multiplication on the left,
namely `a * b₁ ≤ a * b₂ → b₁ ≤ b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCancelCommMonoid`. -/
abbrev MulLeftReflectLE [Mul M] [LE M] : Prop :=
  ContravariantClass M M (· * ·) (· ≤ ·)

Left Multiplication Reflects Order Relation

Informal description

A typeclass stating that for a type `M` with a multiplication operation and a less-than-or-equal relation, left multiplication reflects the order: if $a \cdot b_1 \leq a \cdot b_2$ for some $a, b_1, b_2 \in M$, then $b_1 \leq b_2$.

MulRightReflectLE abbrev

[Mul M] [LE M] : Prop

Full source

/-- Typeclass for reverse monotonicity of multiplication on the right,
namely `a₁ * b ≤ a₂ * b → a₁ ≤ a₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCancelCommMonoid`. -/
abbrev MulRightReflectLE [Mul M] [LE M] : Prop :=
  ContravariantClass M M (swap (· * ·)) (· ≤ ·)

Right Multiplication Reflects Order (`≤`)

Informal description

For a type `M` with a multiplication operation `*` and a less-than-or-equal relation `≤`, the property `MulRightReflectLE` states that for all elements `a₁, a₂, b ∈ M`, if `a₁ * b ≤ a₂ * b` holds, then `a₁ ≤ a₂` must also hold. In other words, multiplication on the right reflects the `≤` relation.

AddLeftReflectLE abbrev

[Add M] [LE M] : Prop

Full source

/-- Typeclass for reverse monotonicity of addition on the left,
namely `a + b₁ ≤ a + b₂ → b₁ ≤ b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCancelAddCommMonoid`. -/
abbrev AddLeftReflectLE [Add M] [LE M] : Prop :=
  ContravariantClass M M (· + ·) (· ≤ ·)

Left Cancellation Property for Addition with Respect to Order

Informal description

For an additive operation `+` on a type `M` equipped with a less-than-or-equal relation `≤`, the property `AddLeftReflectLE` states that for any elements `a, b₁, b₂ ∈ M`, if `a + b₁ ≤ a + b₂`, then `b₁ ≤ b₂`.

AddRightReflectLE abbrev

[Add M] [LE M] : Prop

Full source

/-- Typeclass for reverse monotonicity of addition on the right,
namely `a₁ + b ≤ a₂ + b → a₁ ≤ a₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`OrderedCancelAddCommMonoid`. -/
abbrev AddRightReflectLE [Add M] [LE M] : Prop :=
  ContravariantClass M M (swap (· + ·)) (· ≤ ·)

Right Addition Reflects Order via Less-Than-Or-Equal Relation

Informal description

Given an additive operation `+` and a less-than-or-equal relation `≤` on a type `M`, the property `AddRightReflectLE` states that for all elements `a₁, a₂, b ∈ M`, if `a₁ + b ≤ a₂ + b` holds, then `a₁ ≤ a₂` must also hold.

rel_iff_cov theorem

[CovariantClass M N μ r] [ContravariantClass M N μ r] (m : M) {a b : N} : r (μ m a) (μ m b) ↔ r a b

Full source

theorem rel_iff_cov [CovariantClass M N μ r] [ContravariantClass M N μ r] (m : M) {a b : N} :
    r (μ m a) (μ m b) ↔ r a b :=
  ⟨ContravariantClass.elim _, CovariantClass.elim _⟩

Covariant and Contravariant Operation Preserves Relation Equivalence

Informal description

Let $M$ and $N$ be types with an operation $\mu : M \to N \to N$ and a relation $r$ on $N$. If $\mu$ is both covariant and contravariant with respect to $r$ (i.e., for any $m \in M$, the operation $\mu(m, \cdot)$ preserves and reflects $r$), then for any $m \in M$ and $a, b \in N$, we have $r(\mu(m, a), \mu(m, b))$ if and only if $r(a, b)$.

Covariant.flip theorem

(h : Covariant M N μ r) : Covariant M N μ (flip r)

Full source

theorem Covariant.flip (h : Covariant M N μ r) : Covariant M N μ (flip r) :=
  fun a _ _ ↦ h a

Covariance of Flipped Relation

Informal description

If a relation $r$ on $N$ is covariant with respect to a binary operation $\mu : M \to N \to N$, then the flipped relation $\text{flip}(r)$ (where $\text{flip}(r)(x,y) := r(y,x)$) is also covariant with respect to $\mu$.

Contravariant.flip theorem

(h : Contravariant M N μ r) : Contravariant M N μ (flip r)

Full source

theorem Contravariant.flip (h : Contravariant M N μ r) : Contravariant M N μ (flip r) :=
  fun a _ _ ↦ h a

Contravariance with Respect to Flipped Relation

Informal description

Given a type $M$ with a binary operation $\mu : M \to M \to M$ and a relation $r$ on $M$, if $\mu$ is contravariant with respect to $r$ (i.e., $r(\mu\,m\,a, \mu\,m\,b)$ implies $r(a, b)$ for any $m \in M$), then $\mu$ is also contravariant with respect to the flipped relation $\text{flip}\,r$ (i.e., $r(b, a)$ implies $r(\mu\,m\,b, \mu\,m\,a)$ for any $m \in M$).

act_rel_act_of_rel theorem

(m : M) {a b : N} (ab : r a b) : r (μ m a) (μ m b)

Full source

theorem act_rel_act_of_rel (m : M) {a b : N} (ab : r a b) : r (μ m a) (μ m b) :=
  CovariantClass.elim _ ab

Preservation of Relation under Action

Informal description

Given a type $M$ acting on a type $N$ via an operation $\mu : M \to N \to N$ and a relation $r$ on $N$, if $r(a, b)$ holds for some $a, b \in N$, then for any $m \in M$, the relation $r(\mu(m, a), \mu(m, b))$ also holds.

Group.covariant_iff_contravariant theorem

[Group N] : Covariant N N (· * ·) r ↔ Contravariant N N (· * ·) r

Full source

@[to_additive]
theorem Group.covariant_iff_contravariant [Group N] :
    CovariantCovariant N N (· * ·) r ↔ Contravariant N N (· * ·) r := by
  refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
  · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
    exact h a⁻¹ bc
  · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
    exact h a⁻¹ bc

Equivalence of Covariance and Contravariance for Group Multiplication with Respect to a Relation

Informal description

For a group $N$ with a relation $r$ on $N$, the binary operation $(\cdot)$ is covariant with respect to $r$ if and only if it is contravariant with respect to $r$. In other words, for all $a, b, c \in N$, the implication $r(a, b) \implies r(c \cdot a, c \cdot b)$ holds if and only if the implication $r(c \cdot a, c \cdot b) \implies r(a, b)$ holds.

Group.covconv instance

[Group N] [CovariantClass N N (· * ·) r] : ContravariantClass N N (· * ·) r

Full source

@[to_additive]
instance (priority := 100) Group.covconv [Group N] [CovariantClass N N (· * ·) r] :
    ContravariantClass N N (· * ·) r :=
  ⟨Group.covariant_iff_contravariant.mp CovariantClass.elim⟩

Covariance Implies Contravariance for Group Multiplication

Informal description

For any group $N$ with a relation $r$ on $N$, if multiplication is covariant with respect to $r$ (i.e., $r(a, b)$ implies $r(c \cdot a, c \cdot b)$ for all $a, b, c \in N$), then multiplication is also contravariant with respect to $r$ (i.e., $r(c \cdot a, c \cdot b)$ implies $r(a, b)$ for all $a, b, c \in N$).

Group.mulLeftReflectLE_of_mulLeftMono theorem

[Group N] [LE N] [MulLeftMono N] : MulLeftReflectLE N

Full source

@[to_additive]
theorem Group.mulLeftReflectLE_of_mulLeftMono [Group N] [LE N]
    [MulLeftMono N] : MulLeftReflectLE N :=
  inferInstance

Monotonicity of Left Multiplication Implies Order Reflection in Groups

Informal description

Let $N$ be a group equipped with a partial order $\leq$ such that left multiplication is monotone (i.e., for all $a, b_1, b_2 \in N$, if $b_1 \leq b_2$ then $a \cdot b_1 \leq a \cdot b_2$). Then left multiplication reflects the order relation (i.e., for all $a, b_1, b_2 \in N$, if $a \cdot b_1 \leq a \cdot b_2$ then $b_1 \leq b_2$).

Group.mulLeftReflectLT_of_mulLeftStrictMono theorem

[Group N] [LT N] [MulLeftStrictMono N] : MulLeftReflectLT N

Full source

@[to_additive]
theorem Group.mulLeftReflectLT_of_mulLeftStrictMono [Group N] [LT N]
    [MulLeftStrictMono N] : MulLeftReflectLT N :=
  inferInstance

Reflection of Strict Order under Left Multiplication in Groups with Strictly Monotone Multiplication

Informal description

For any group $N$ with a strict order relation $<$ and strictly monotone left multiplication (i.e., $b_1 < b_2$ implies $a * b_1 < a * b_2$ for all $a, b_1, b_2 \in N$), left multiplication reflects the strict order (i.e., $a * b_1 < a * b_2$ implies $b_1 < b_2$ for all $a, b_1, b_2 \in N$).

Group.covariant_swap_iff_contravariant_swap theorem

[Group N] : Covariant N N (swap (· * ·)) r ↔ Contravariant N N (swap (· * ·)) r

Full source

@[to_additive]
theorem Group.covariant_swap_iff_contravariant_swap [Group N] :
    CovariantCovariant N N (swap (· * ·)) r ↔ Contravariant N N (swap (· * ·)) r := by
  refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
  · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
    exact h a⁻¹ bc
  · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
    exact h a⁻¹ bc

Equivalence of Covariance and Contravariance for Swapped Multiplication in Groups

Informal description

Let $N$ be a group with a relation $r$. The operation of multiplication in $N$ is covariant with respect to $r$ when the arguments are swapped (i.e., $\mu(y, x) = x \cdot y$) if and only if it is contravariant with respect to $r$ when the arguments are swapped. In other words, for all $x, y, z \in N$, the implication $r(x \cdot y, x \cdot z) \to r(y, z)$ holds if and only if the implication $r(y, z) \to r(x \cdot y, x \cdot z)$ holds.

Group.covconv_swap instance

[Group N] [CovariantClass N N (swap (· * ·)) r] : ContravariantClass N N (swap (· * ·)) r

Full source

@[to_additive]
instance (priority := 100) Group.covconv_swap [Group N] [CovariantClass N N (swap (· * ·)) r] :
    ContravariantClass N N (swap (· * ·)) r :=
  ⟨Group.covariant_swap_iff_contravariant_swap.mp CovariantClass.elim⟩

Covariance Implies Contravariance for Swapped Multiplication in Groups

Informal description

For any group $N$ with a relation $r$, if the swapped multiplication operation (i.e., $x \cdot y$ becomes $y \cdot x$) is covariant with respect to $r$, then it is also contravariant with respect to $r$.

Group.mulRightReflectLE_of_mulRightMono theorem

[Group N] [LE N] [MulRightMono N] : MulRightReflectLE N

Full source

@[to_additive]
theorem Group.mulRightReflectLE_of_mulRightMono [Group N] [LE N]
    [MulRightMono N] : MulRightReflectLE N :=
  inferInstance

Monotonicity of Right Multiplication Implies Order Reflection in Groups

Informal description

For any group $N$ with a partial order $\leq$ and right multiplication that is monotone (i.e., $a \leq b$ implies $a \cdot c \leq b \cdot c$ for all $a, b, c \in N$), it follows that right multiplication reflects the order (i.e., $a \cdot c \leq b \cdot c$ implies $a \leq b$ for all $a, b, c \in N$).

Group.mulRightReflectLT_of_mulRightStrictMono theorem

[Group N] [LT N] [MulRightStrictMono N] : MulRightReflectLT N

Full source

@[to_additive]
theorem Group.mulRightReflectLT_of_mulRightStrictMono [Group N] [LT N]
    [MulRightStrictMono N] : MulRightReflectLT N :=
  inferInstance

Right Multiplication Reflects Strict Order in Strictly Right Monotone Groups

Informal description

For any group $N$ equipped with a strict order relation $<$ and the property that right multiplication is strictly monotone (i.e., $a < b$ implies $a \cdot c < b \cdot c$ for all $c \in N$), it follows that right multiplication reflects the strict order (i.e., $a \cdot c < b \cdot c$ implies $a < b$ for all $c \in N$).

act_rel_of_rel_of_act_rel theorem

(ab : r a b) (rl : r (μ m b) c) : r (μ m a) c

Full source

theorem act_rel_of_rel_of_act_rel (ab : r a b) (rl : r (μ m b) c) : r (μ m a) c :=
  _root_.trans (act_rel_act_of_rel m ab) rl

Transitivity of Action-Preserved Relation: $\mu(m, a) \prec c$ given $a \prec b$ and $\mu(m, b) \prec c$

Informal description

Given a type $M$ acting on a type $N$ via an operation $\mu : M \to N \to N$ and a transitive relation $r$ on $N$, if $r(a, b)$ holds for some $a, b \in N$ and $r(\mu(m, b), c)$ holds for some $m \in M$ and $c \in N$, then $r(\mu(m, a), c)$ also holds.

rel_act_of_rel_of_rel_act theorem

(ab : r a b) (rr : r c (μ m a)) : r c (μ m b)

Full source

theorem rel_act_of_rel_of_rel_act (ab : r a b) (rr : r c (μ m a)) : r c (μ m b) :=
  _root_.trans rr (act_rel_act_of_rel _ ab)

Transitivity of Action-Preserved Relation: $c \prec \mu(m, b)$ given $a \prec b$ and $c \prec \mu(m, a)$

Informal description

Given a transitive relation $r$ on a type $N$ and an action $\mu : M \to N \to N$, if $r(a, b)$ holds for some $a, b \in N$ and $r(c, \mu(m, a))$ holds for some $c \in N$ and $m \in M$, then $r(c, \mu(m, b))$ also holds.

act_rel_act_of_rel_of_rel theorem

(ab : r a b) (cd : r c d) : r (mu a c) (mu b d)

Full source

theorem act_rel_act_of_rel_of_rel (ab : r a b) (cd : r c d) : r (mu a c) (mu b d) :=
  _root_.trans (@act_rel_act_of_rel _ _ (swap mu) r _ c _ _ ab) (act_rel_act_of_rel b cd)

Preservation of Relation under Binary Operation: $a \prec b \land c \prec d \implies \mu(a,c) \prec \mu(b,d)$

Informal description

Given a binary operation $\mu : M \to N \to N$ and a transitive relation $r$ on $N$, if $r(a, b)$ and $r(c, d)$ hold for some $a, b, c, d \in N$, then $r(\mu(a, c), \mu(b, d))$ also holds.

rel_of_act_rel_act theorem

(m : M) {a b : N} (ab : r (μ m a) (μ m b)) : r a b

Full source

theorem rel_of_act_rel_act (m : M) {a b : N} (ab : r (μ m a) (μ m b)) : r a b :=
  ContravariantClass.elim _ ab

Contravariance of Relation under Action: $r(\mu(m,a), \mu(m,b)) \implies r(a,b)$

Informal description

For any element $m \in M$ and elements $a, b \in N$, if the relation $r$ holds between $\mu(m, a)$ and $\mu(m, b)$, then $r$ also holds between $a$ and $b$.

act_rel_of_act_rel_of_rel_act_rel theorem

(ab : r (μ m a) b) (rl : r (μ m b) (μ m c)) : r (μ m a) c

Full source

theorem act_rel_of_act_rel_of_rel_act_rel (ab : r (μ m a) b) (rl : r (μ m b) (μ m c)) :
    r (μ m a) c :=
  _root_.trans ab (rel_of_act_rel_act m rl)

Transitivity of Action-Relation Interaction: $r(\mu(m,a), b) \land r(\mu(m,b), \mu(m,c)) \implies r(\mu(m,a), c)$

Informal description

Let $M$ and $N$ be types with a binary operation $\mu : M \to N \to N$ and a transitive relation $r$ on $N$. For any $m \in M$ and $a, b, c \in N$, if $r(\mu(m, a), b)$ holds and $r(\mu(m, b), \mu(m, c))$ holds, then $r(\mu(m, a), c)$ also holds.

rel_act_of_act_rel_act_of_rel_act theorem

(ab : r (μ m a) (μ m b)) (rr : r b (μ m c)) : r a (μ m c)

Full source

theorem rel_act_of_act_rel_act_of_rel_act (ab : r (μ m a) (μ m b)) (rr : r b (μ m c)) :
    r a (μ m c) :=
  _root_.trans (rel_of_act_rel_act m ab) rr

Transitive Chaining of Action-Relation Implications: $r(\mu(m,a), \mu(m,b)) \land r(b, \mu(m,c)) \implies r(a, \mu(m,c))$

Informal description

Let $M$ and $N$ be types with a binary operation $\mu : M \to N \to N$ and a transitive relation $r$ on $N$. For any $m \in M$ and $a, b, c \in N$, if $r(\mu(m, a), \mu(m, b))$ holds and $r(b, \mu(m, c))$ holds, then $r(a, \mu(m, c))$ also holds.

Covariant.monotone_of_const theorem

[CovariantClass M N μ (· ≤ ·)] (m : M) : Monotone (μ m)

Full source

/-- The partial application of a constant to a covariant operator is monotone. -/
theorem Covariant.monotone_of_const [CovariantClass M N μ (· ≤ ·)] (m : M) : Monotone (μ m) :=
  fun _ _ ↦ CovariantClass.elim m

Monotonicity of Partial Application in Covariant Operations

Informal description

Let $M$ and $N$ be types with a binary operation $\mu : M \to N \to N$ and a preorder relation $\leq$ on $N$. If the operation $\mu$ is covariant with respect to $\leq$ (i.e., for any $m \in M$, the function $\mu(m, \cdot) : N \to N$ preserves the order $\leq$), then for any fixed $m \in M$, the partial application $\mu(m, \cdot)$ is a monotone function from $N$ to $N$.

Monotone.covariant_of_const theorem

[CovariantClass M N μ (· ≤ ·)] (hf : Monotone f) (m : M) : Monotone (f <| μ m ·)

Full source

/-- A monotone function remains monotone when composed with the partial application
of a covariant operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (m + n))`. -/
theorem Monotone.covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Monotone f) (m : M) :
    Monotone (f <| μ m ·) :=
  hf.comp (Covariant.monotone_of_const m)

Monotonicity of Composition with Covariant Operation

Informal description

Let $M$ and $N$ be types with a binary operation $\mu : M \to N \to N$ and a preorder relation $\leq$ on $N$. If $\mu$ is covariant with respect to $\leq$ (i.e., for any $m \in M$, the function $\mu(m, \cdot) : N \to N$ is monotone), then for any monotone function $f : N \to P$ (where $P$ is a preorder) and any fixed $m \in M$, the composition $f \circ \mu(m, \cdot)$ is monotone.

Monotone.covariant_of_const' theorem

{μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)] (hf : Monotone f) (m : N) : Monotone (f <| μ · m)

Full source

/-- Same as `Monotone.covariant_of_const`, but with the constant on the other side of
the operator.  E.g., `∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (n + m))`. -/
theorem Monotone.covariant_of_const' {μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)]
    (hf : Monotone f) (m : N) : Monotone (f <| μ · m) :=
  Monotone.covariant_of_const (μ := swap μ) hf m

Monotonicity of Composition with Covariant Operation in First Argument

Informal description

Let $N$ be a type with a binary operation $\mu : N \to N \to N$ and a preorder relation $\leq$ on $N$. Suppose that for any $n \in N$, the function $\mu(\cdot, n) : N \to N$ is monotone (i.e., the operation $\mu$ is covariant in its first argument with respect to $\leq$). Then for any monotone function $f : N \to P$ (where $P$ is a preorder) and any fixed $m \in N$, the composition $f \circ \mu(\cdot, m)$ is monotone.

Antitone.covariant_of_const theorem

[CovariantClass M N μ (· ≤ ·)] (hf : Antitone f) (m : M) : Antitone (f <| μ m ·)

Full source

/-- Dual of `Monotone.covariant_of_const` -/
theorem Antitone.covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Antitone f) (m : M) :
    Antitone (f <| μ m ·) :=
  hf.comp_monotone <| Covariant.monotone_of_const m

Antitone Composition with Covariant Operation

Informal description

Let $M$ and $N$ be types with a binary operation $\mu : M \to N \to N$ and a preorder relation $\leq$ on $N$. If $\mu$ is covariant with respect to $\leq$ (i.e., for any $m \in M$, the function $\mu(m, \cdot) : N \to N$ is monotone), then for any antitone function $f : N \to P$ (where $P$ is a preorder) and any fixed $m \in M$, the composition $f \circ \mu(m, \cdot)$ is antitone.

Antitone.covariant_of_const' theorem

{μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)] (hf : Antitone f) (m : N) : Antitone (f <| μ · m)

Full source

/-- Dual of `Monotone.covariant_of_const'` -/
theorem Antitone.covariant_of_const' {μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)]
    (hf : Antitone f) (m : N) : Antitone (f <| μ · m) :=
  Antitone.covariant_of_const (μ := swap μ) hf m

Antitone Composition with Covariant Operation (Swapped Arguments)

Informal description

Let $N$ be a type with a binary operation $\mu : N \to N \to N$ and a preorder relation $\leq$ on $N$. Suppose that $\mu$ is covariant with respect to $\leq$ when the arguments are swapped (i.e., for any $n \in N$, the function $\mu(\cdot, n) : N \to N$ is monotone). Then for any antitone function $f : N \to P$ (where $P$ is a preorder) and any fixed $m \in N$, the composition $f \circ \mu(\cdot, m)$ is antitone.

covariant_le_of_covariant_lt theorem

[PartialOrder N] : Covariant M N μ (· < ·) → Covariant M N μ (· ≤ ·)

Full source

theorem covariant_le_of_covariant_lt [PartialOrder N] :
    Covariant M N μ (· < ·) → Covariant M N μ (· ≤ ·) := by
  intro h a b c bc
  rcases bc.eq_or_lt with (rfl | bc)
  · exact le_rfl
  · exact (h _ bc).le

Covariance of $\leq$ from covariance of $<$ under a binary operation

Informal description

Let $N$ be a partially ordered set and $\mu : M \to N \to N$ be a binary operation. If $\mu$ is covariant with respect to the strict order relation $<$ (i.e., for any $m \in M$, the function $\mu(m, \cdot) : N \to N$ preserves $<$), then $\mu$ is also covariant with respect to the non-strict order relation $\leq$.

covariantClass_le_of_lt theorem

[PartialOrder N] [CovariantClass M N μ (· < ·)] : CovariantClass M N μ (· ≤ ·)

Full source

theorem covariantClass_le_of_lt [PartialOrder N] [CovariantClass M N μ (· < ·)] :
    CovariantClass M N μ (· ≤ ·) := ⟨covariant_le_of_covariant_lt _ _ _ CovariantClass.elim⟩

Covariance of $\leq$ from covariance of $<$ under a binary operation

Informal description

Let $N$ be a partially ordered set with a binary operation $\mu : M \to N \to N$. If $\mu$ is covariant with respect to the strict order relation $<$ (i.e., for any $m \in M$, the function $\mu(m, \cdot) : N \to N$ preserves $<$), then $\mu$ is also covariant with respect to the non-strict order relation $\leq$.

mulLeftMono_of_mulLeftStrictMono theorem

(M) [Mul M] [PartialOrder M] [MulLeftStrictMono M] : MulLeftMono M

Full source

@[to_additive]
theorem mulLeftMono_of_mulLeftStrictMono (M) [Mul M] [PartialOrder M] [MulLeftStrictMono M] :
    MulLeftMono M := covariantClass_le_of_lt _ _ _

Monotonicity of Left Multiplication from Strict Monotonicity

Informal description

Let $M$ be a type equipped with a multiplication operation and a partial order $\leq$. If left multiplication is strictly monotone (i.e., for any $a, b_1, b_2 \in M$, $b_1 < b_2$ implies $a * b_1 < a * b_2$), then left multiplication is also monotone (i.e., $b_1 \leq b_2$ implies $a * b_1 \leq a * b_2$).

mulRightMono_of_mulRightStrictMono theorem

(M) [Mul M] [PartialOrder M] [MulRightStrictMono M] : MulRightMono M

Full source

@[to_additive]
theorem mulRightMono_of_mulRightStrictMono (M) [Mul M] [PartialOrder M] [MulRightStrictMono M] :
    MulRightMono M := covariantClass_le_of_lt _ _ _

Monotonicity of Right Multiplication from Strict Monotonicity

Informal description

Let $M$ be a type equipped with a multiplication operation and a partial order $\leq$. If multiplication on the right is strictly monotone (i.e., for any $a, b, c \in M$, $a < b$ implies $a * c < b * c$), then multiplication on the right is also monotone (i.e., $a \leq b$ implies $a * c \leq b * c$).

contravariant_le_iff_contravariant_lt_and_eq theorem

 [PartialOrder N] : Contravariant M N μ (· ≤ ·) ↔ Contravariant M N μ (· < ·) ∧ Contravariant M N μ (· = ·)

Full source

theorem contravariant_le_iff_contravariant_lt_and_eq [PartialOrder N] :
    ContravariantContravariant M N μ (· ≤ ·) ↔ Contravariant M N μ (· < ·) ∧ Contravariant M N μ (· = ·) := by
  refine ⟨fun h ↦ ⟨fun a b c bc ↦ ?_, fun a b c bc ↦ ?_⟩, fun h ↦ fun a b c bc ↦ ?_⟩
  · exact (h a bc.le).lt_of_ne (by rintro rfl; exact lt_irrefl _ bc)
  · exact (h a bc.le).antisymm (h a bc.ge)
  · exact bc.lt_or_eq.elim (fun bc ↦ (h.1 a bc).le) (fun bc ↦ (h.2 a bc).le)

Contravariance with respect to $\leq$ is equivalent to contravariance with respect to both $<$ and $=$

Informal description

For a type $N$ with a partial order $\leq$, the operation $\mu : M \to N \to N$ is contravariant with respect to $\leq$ if and only if it is contravariant with respect to both the strict order $<$ and equality $=$. In other words, for all $m \in M$ and $n_1, n_2 \in N$, the following are equivalent: 1. $\mu\, m\, n_1 \leq \mu\, m\, n_2$ implies $n_1 \leq n_2$; 2. $\mu\, m\, n_1 < \mu\, m\, n_2$ implies $n_1 < n_2$, and $\mu\, m\, n_1 = \mu\, m\, n_2$ implies $n_1 = n_2$.

contravariant_lt_of_contravariant_le theorem

[PartialOrder N] : Contravariant M N μ (· ≤ ·) → Contravariant M N μ (· < ·)

Full source

theorem contravariant_lt_of_contravariant_le [PartialOrder N] :
    Contravariant M N μ (· ≤ ·) → Contravariant M N μ (· < ·) :=
  And.leftAnd.left ∘ (contravariant_le_iff_contravariant_lt_and_eq M N μ).mp

Contravariance with respect to $\leq$ implies contravariance with respect to $<$

Informal description

Let $N$ be a partially ordered set and $\mu : M \to N \to N$ be a binary operation. If $\mu$ is contravariant with respect to the non-strict order $\leq$ (i.e., $\mu\, m\, n_1 \leq \mu\, m\, n_2$ implies $n_1 \leq n_2$ for all $m \in M$), then $\mu$ is also contravariant with respect to the strict order $<$ (i.e., $\mu\, m\, n_1 < \mu\, m\, n_2$ implies $n_1 < n_2$ for all $m \in M$).

covariant_le_iff_contravariant_lt theorem

[LinearOrder N] : Covariant M N μ (· ≤ ·) ↔ Contravariant M N μ (· < ·)

Full source

theorem covariant_le_iff_contravariant_lt [LinearOrder N] :
    CovariantCovariant M N μ (· ≤ ·) ↔ Contravariant M N μ (· < ·) :=
  ⟨fun h _ _ _ bc ↦ not_le.mp fun k ↦ bc.not_le (h _ k),
   fun h _ _ _ bc ↦ not_lt.mp fun k ↦ bc.not_lt (h _ k)⟩

Equivalence of Covariance with $\leq$ and Contravariance with $<$ in Linear Orders

Informal description

For a linearly ordered type $N$ and a binary operation $\mu : M \to N \to N$, the following are equivalent: 1. The operation $\mu$ is covariant with respect to the non-strict order $\leq$ (i.e., $n_1 \leq n_2$ implies $\mu\, m\, n_1 \leq \mu\, m\, n_2$ for all $m \in M$); 2. The operation $\mu$ is contravariant with respect to the strict order $<$ (i.e., $\mu\, m\, n_1 < \mu\, m\, n_2$ implies $n_1 < n_2$ for all $m \in M$).

covariant_lt_iff_contravariant_le theorem

[LinearOrder N] : Covariant M N μ (· < ·) ↔ Contravariant M N μ (· ≤ ·)

Full source

theorem covariant_lt_iff_contravariant_le [LinearOrder N] :
    CovariantCovariant M N μ (· < ·) ↔ Contravariant M N μ (· ≤ ·) :=
  ⟨fun h _ _ _ bc ↦ not_lt.mp fun k ↦ bc.not_lt (h _ k),
   fun h _ _ _ bc ↦ not_le.mp fun k ↦ bc.not_le (h _ k)⟩

Equivalence between covariance with respect to $<$ and contravariance with respect to $\leq$ in linear orders

Informal description

Let $N$ be a linearly ordered set and $\mu : M \to N \to N$ be a binary operation. Then the following are equivalent: 1. The operation $\mu$ is covariant with respect to the strict order $<$ (i.e., for any $m \in M$, if $n_1 < n_2$ then $\mu(m, n_1) < \mu(m, n_2)$) 2. The operation $\mu$ is contravariant with respect to the non-strict order $\leq$ (i.e., for any $m \in M$, if $\mu(m, n_1) \leq \mu(m, n_2)$ then $n_1 \leq n_2$)

covariant_flip_iff theorem

[h : Std.Commutative mu] : Covariant N N (flip mu) r ↔ Covariant N N mu r

Full source

theorem covariant_flip_iff [h : Std.Commutative mu] :
    CovariantCovariant N N (flip mu) r ↔ Covariant N N mu r := by unfold flip; simp_rw [h.comm]

Equivalence of Covariance Under Flipped Operation for Commutative Operations

Informal description

Let $N$ be a type with a binary operation $\mu : N \to N \to N$ and a relation $r$ on $N$. If $\mu$ is commutative, then the following are equivalent: 1. The relation $r$ is covariant with respect to the flipped operation $\text{flip}(\mu)(a,b) = \mu(b,a)$ 2. The relation $r$ is covariant with respect to $\mu$ In other words, for a commutative operation $\mu$, covariance under the flipped operation is equivalent to covariance under $\mu$ itself.

contravariant_flip_iff theorem

[h : Std.Commutative mu] : Contravariant N N (flip mu) r ↔ Contravariant N N mu r

Full source

theorem contravariant_flip_iff [h : Std.Commutative mu] :
    ContravariantContravariant N N (flip mu) r ↔ Contravariant N N mu r := by unfold flip; simp_rw [h.comm]

Equivalence of Contravariance Properties for Commutative Operations

Informal description

Let $N$ be a type with a binary operation $\mu : N \to N \to N$ and a relation $r$ on $N$. If $\mu$ is commutative (i.e., $\mu(a,b) = \mu(b,a)$ for all $a,b \in N$), then the following are equivalent: 1. The operation $\mu$ is contravariant with respect to $r$ when the arguments are flipped (i.e., for any $m \in N$, if $r(\mu(n_1, m), \mu(n_2, m))$ holds, then $r(n_1, n_2)$ holds) 2. The operation $\mu$ is contravariant with respect to $r$ (i.e., for any $m \in N$, if $r(\mu(m, n_1), \mu(m, n_2))$ holds, then $r(n_1, n_2)$ holds)

contravariant_lt_of_covariant_le instance

[LinearOrder N] [CovariantClass N N mu (· ≤ ·)] : ContravariantClass N N mu (· < ·)

Full source

instance contravariant_lt_of_covariant_le [LinearOrder N]
    [CovariantClass N N mu (· ≤ ·)] : ContravariantClass N N mu (· < ·) where
  elim := (covariant_le_iff_contravariant_lt N N mu).mp CovariantClass.elim

Contravariance of $<$ from Covariance of $\leq$ in Linear Orders

Informal description

For a linearly ordered type $N$ with a binary operation $\mu : N \to N \to N$, if $\mu$ is covariant with respect to the non-strict order $\leq$ (i.e., $n_1 \leq n_2$ implies $\mu\, m\, n_1 \leq \mu\, m\, n_2$ for all $m \in N$), then $\mu$ is also contravariant with respect to the strict order $<$ (i.e., $\mu\, m\, n_1 < \mu\, m\, n_2$ implies $n_1 < n_2$ for all $m \in N$).

mulLeftReflectLT_of_mulLeftMono theorem

[Mul N] [LinearOrder N] [MulLeftMono N] : MulLeftReflectLT N

Full source

@[to_additive]
theorem mulLeftReflectLT_of_mulLeftMono [Mul N] [LinearOrder N] [MulLeftMono N] :
    MulLeftReflectLT N :=
  inferInstance

Monotonicity of Left Multiplication Implies Reflection of Strict Order in Linear Orders

Informal description

For any linearly ordered type $N$ with a multiplication operation, if left multiplication is monotone with respect to the non-strict order $\leq$ (i.e., $b_1 \leq b_2$ implies $a * b_1 \leq a * b_2$ for all $a, b_1, b_2 \in N$), then left multiplication reflects the strict order $<$ (i.e., $a * b_1 < a * b_2$ implies $b_1 < b_2$ for all $a, b_1, b_2 \in N$).

mulRightReflectLT_of_mulRightMono theorem

[Mul N] [LinearOrder N] [MulRightMono N] : MulRightReflectLT N

Full source

@[to_additive]
theorem mulRightReflectLT_of_mulRightMono [Mul N] [LinearOrder N] [MulRightMono N] :
    MulRightReflectLT N :=
  inferInstance

Right multiplication reflects strict order when it is monotone in linear orders

Informal description

For a linearly ordered type $N$ with a multiplication operation, if right multiplication is monotone (i.e., $a \leq b$ implies $a \cdot c \leq b \cdot c$ for all $c \in N$), then right multiplication reflects the strict order (i.e., $a \cdot c < b \cdot c$ implies $a < b$ for all $c \in N$).

covariant_lt_of_contravariant_le instance

[LinearOrder N] [ContravariantClass N N mu (· ≤ ·)] : CovariantClass N N mu (· < ·)

Full source

instance covariant_lt_of_contravariant_le [LinearOrder N]
    [ContravariantClass N N mu (· ≤ ·)] : CovariantClass N N mu (· < ·) where
  elim := (covariant_lt_iff_contravariant_le N N mu).mpr ContravariantClass.elim

Contravariance with respect to $\leq$ implies covariance with respect to $<$ in linear orders

Informal description

For any linearly ordered set $N$ with a binary operation $\mu : N \to N \to N$, if $\mu$ is contravariant with respect to the non-strict order $\leq$ (i.e., $\mu(a, x) \leq \mu(a, y)$ implies $x \leq y$ for all $a, x, y \in N$), then $\mu$ is covariant with respect to the strict order $<$ (i.e., $x < y$ implies $\mu(a, x) < \mu(a, y)$ for all $a, x, y \in N$).

mulLeftStrictMono_of_mulLeftReflectLE theorem

[Mul N] [LinearOrder N] [MulLeftReflectLE N] : MulLeftStrictMono N

Full source

@[to_additive]
theorem mulLeftStrictMono_of_mulLeftReflectLE [Mul N] [LinearOrder N] [MulLeftReflectLE N] :
    MulLeftStrictMono N :=
  inferInstance

Left multiplication is strictly monotone if it reflects the non-strict order in a linear order

Informal description

For any linearly ordered type $N$ with a multiplication operation, if left multiplication reflects the non-strict order $\leq$ (i.e., $a \cdot b_1 \leq a \cdot b_2$ implies $b_1 \leq b_2$ for all $a, b_1, b_2 \in N$), then left multiplication is strictly monotone with respect to the strict order $<$ (i.e., $b_1 < b_2$ implies $a \cdot b_1 < a \cdot b_2$ for all $a, b_1, b_2 \in N$).

mulRightStrictMono_of_mulRightReflectLE theorem

[Mul N] [LinearOrder N] [MulRightReflectLE N] : MulRightStrictMono N

Full source

@[to_additive]
theorem mulRightStrictMono_of_mulRightReflectLE [Mul N] [LinearOrder N] [MulRightReflectLE N] :
    MulRightStrictMono N :=
  inferInstance

Right multiplication is strictly monotone if it reflects order in linearly ordered semigroups

Informal description

For any linearly ordered set $N$ with a multiplication operation $*$, if multiplication on the right reflects the non-strict order $\leq$ (i.e., for all $a, b, c \in N$, $a * c \leq b * c$ implies $a \leq b$), then multiplication on the right is strictly monotone with respect to $<$ (i.e., for all $a, b, c \in N$, $a < b$ implies $a * c < b * c$).

covariant_swap_mul_of_covariant_mul instance

[CommSemigroup N] [CovariantClass N N (· * ·) r] : CovariantClass N N (swap (· * ·)) r

Full source

@[to_additive]
instance covariant_swap_mul_of_covariant_mul [CommSemigroup N]
    [CovariantClass N N (· * ·) r] : CovariantClass N N (swap (· * ·)) r where
  elim := (covariant_flip_iff N r (· * ·)).mpr CovariantClass.elim

Covariance under Swapped Multiplication in Commutative Semigroups

Informal description

For any commutative semigroup $N$ with a relation $r$, if multiplication $(\cdot * \cdot)$ preserves $r$ in its second argument (i.e., $r$ is covariant with respect to multiplication), then the swapped multiplication $\operatorname{swap}(\cdot * \cdot)$ also preserves $r$ in its second argument.

mulRightMono_of_mulLeftMono theorem

[CommSemigroup N] [LE N] [MulLeftMono N] : MulRightMono N

Full source

@[to_additive]
theorem mulRightMono_of_mulLeftMono [CommSemigroup N] [LE N] [MulLeftMono N] :
    MulRightMono N :=
  inferInstance

Monotonicity of Right Multiplication from Left Multiplication in Commutative Semigroups

Informal description

Let $N$ be a commutative semigroup with a preorder relation $\leq$. If left multiplication is monotone (i.e., for all $a, b_1, b_2 \in N$, $b_1 \leq b_2$ implies $a * b_1 \leq a * b_2$), then right multiplication is also monotone (i.e., for all $a_1, a_2, b \in N$, $a_1 \leq a_2$ implies $a_1 * b \leq a_2 * b$).

mulRightStrictMono_of_mulLeftStrictMono theorem

[CommSemigroup N] [LT N] [MulLeftStrictMono N] : MulRightStrictMono N

Full source

@[to_additive]
theorem mulRightStrictMono_of_mulLeftStrictMono [CommSemigroup N] [LT N] [MulLeftStrictMono N] :
    MulRightStrictMono N :=
  inferInstance

Strict Monotonicity of Right Multiplication from Left in Commutative Semigroups

Informal description

Let $N$ be a commutative semigroup equipped with a strict order relation $<$. If left multiplication is strictly monotone (i.e., for all $a, b_1, b_2 \in N$, $b_1 < b_2$ implies $a * b_1 < a * b_2$), then right multiplication is also strictly monotone (i.e., for all $a_1, a_2, b \in N$, $a_1 < a_2$ implies $a_1 * b < a_2 * b$).

contravariant_swap_mul_of_contravariant_mul instance

[CommSemigroup N] [ContravariantClass N N (· * ·) r] : ContravariantClass N N (swap (· * ·)) r

Full source

@[to_additive]
instance contravariant_swap_mul_of_contravariant_mul [CommSemigroup N]
    [ContravariantClass N N (· * ·) r] : ContravariantClass N N (swap (· * ·)) r where
  elim := (contravariant_flip_iff N r (· * ·)).mpr ContravariantClass.elim

Contravariance of Swapped Multiplication in Commutative Semigroups

Informal description

For any commutative semigroup $N$ with a relation $r$, if multiplication is contravariant with respect to $r$ (i.e., $a * b \mathrel{r} a * c$ implies $b \mathrel{r} c$), then the swapped multiplication (i.e., $b * a$) is also contravariant with respect to $r$.

mulRightReflectLE_of_mulLeftReflectLE theorem

[CommSemigroup N] [LE N] [MulLeftReflectLE N] : MulRightReflectLE N

Full source

@[to_additive]
theorem mulRightReflectLE_of_mulLeftReflectLE [CommSemigroup N] [LE N] [MulLeftReflectLE N] :
    MulRightReflectLE N :=
  inferInstance

Right Multiplication Reflects Order in Commutative Semigroups if Left Does

Informal description

Let $N$ be a commutative semigroup equipped with a partial order $\leq$. If left multiplication reflects the order (i.e., for all $a, b_1, b_2 \in N$, $a * b_1 \leq a * b_2$ implies $b_1 \leq b_2$), then right multiplication also reflects the order (i.e., for all $a_1, a_2, b \in N$, $a_1 * b \leq a_2 * b$ implies $a_1 \leq a_2$).

mulRightReflectLT_of_mulLeftReflectLT theorem

[CommSemigroup N] [LT N] [MulLeftReflectLT N] : MulRightReflectLT N

Full source

@[to_additive]
theorem mulRightReflectLT_of_mulLeftReflectLT [CommSemigroup N] [LT N] [MulLeftReflectLT N] :
    MulRightReflectLT N :=
  inferInstance

Right multiplication reflects strict order in commutative semigroups when left multiplication does

Informal description

Let $N$ be a commutative semigroup with a strict order relation $<$. If left multiplication reflects the strict order (i.e., for all $a, b_1, b_2 \in N$, $a * b_1 < a * b_2$ implies $b_1 < b_2$), then right multiplication also reflects the strict order (i.e., for all $a_1, a_2, b \in N$, $a_1 * b < a_2 * b$ implies $a_1 < a_2$).

covariant_lt_of_covariant_le_of_contravariant_eq theorem

 [ContravariantClass M N μ (· = ·)] [PartialOrder N] [CovariantClass M N μ (· ≤ ·)] : CovariantClass M N μ (· < ·)

Full source

theorem covariant_lt_of_covariant_le_of_contravariant_eq [ContravariantClass M N μ (· = ·)]
    [PartialOrder N] [CovariantClass M N μ (· ≤ ·)] : CovariantClass M N μ (· < ·) where
  elim a _ _ bc := (CovariantClass.elim a bc.le).lt_of_ne (bc.ne ∘ ContravariantClass.elim _)

Covariance of strict order under covariance of non-strict order and contravariance of equality

Informal description

Let $M$ and $N$ be types with a binary operation $\mu : M \to N \to N$ and a partial order $\leq$ on $N$. If $\mu$ is contravariant with respect to equality (i.e., $\mu(m, n_1) = \mu(m, n_2)$ implies $n_1 = n_2$ for all $m \in M$) and covariant with respect to $\leq$ (i.e., $n_1 \leq n_2$ implies $\mu(m, n_1) \leq \mu(m, n_2)$ for all $m \in M$), then $\mu$ is also covariant with respect to the strict order $<$ on $N$.

contravariant_le_of_contravariant_eq_and_lt theorem

 [PartialOrder N] [ContravariantClass M N μ (· = ·)] [ContravariantClass M N μ (· < ·)] :
  ContravariantClass M N μ (· ≤ ·)

Full source

theorem contravariant_le_of_contravariant_eq_and_lt [PartialOrder N]
    [ContravariantClass M N μ (· = ·)] [ContravariantClass M N μ (· < ·)] :
    ContravariantClass M N μ (· ≤ ·) where
  elim := (contravariant_le_iff_contravariant_lt_and_eq M N μ).mpr
    ⟨ContravariantClass.elim, ContravariantClass.elim⟩

Contravariance of $\leq$ from contravariance of $=$ and $<$

Informal description

Let $N$ be a partially ordered set and $M$ be a type with a binary operation $\mu : M \to N \to N$. If $\mu$ is contravariant with respect to both equality $=$ and the strict order $<$ on $N$, then $\mu$ is also contravariant with respect to the non-strict order $\leq$ on $N$. In other words, for all $m \in M$ and $n_1, n_2 \in N$, if $\mu(m, n_1) \leq \mu(m, n_2)$ implies $n_1 \leq n_2$ whenever $\mu$ preserves both equality and strict order in the contravariant sense.

IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono instance

[Mul N] [IsLeftCancelMul N] [PartialOrder N] [MulLeftMono N] : MulLeftStrictMono N

Full source

@[to_additive]
instance IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono [Mul N] [IsLeftCancelMul N]
    [PartialOrder N] [MulLeftMono N] :
    MulLeftStrictMono N where
  elim a _ _ bc := (CovariantClass.elim a bc.le).lt_of_ne ((mul_ne_mul_right a).mpr bc.ne)

Strict Monotonicity from Monotonicity in Left Cancellative Structures

Informal description

For any left cancellative multiplicative structure $N$ with a partial order, if left multiplication is monotone with respect to the order, then it is also strictly monotone.

IsRightCancelMul.mulRightStrictMono_of_mulRightMono instance

[Mul N] [IsRightCancelMul N] [PartialOrder N] [MulRightMono N] : MulRightStrictMono N

Full source

@[to_additive]
instance IsRightCancelMul.mulRightStrictMono_of_mulRightMono
    [Mul N] [IsRightCancelMul N] [PartialOrder N] [MulRightMono N] :
    MulRightStrictMono N where
  elim a _ _ bc := (CovariantClass.elim a bc.le).lt_of_ne ((mul_ne_mul_left a).mpr bc.ne)

Strict Right Monotonicity from Monotonicity in Right Cancellative Structures

Informal description

For any type $N$ with a multiplication operation that is right cancellative and a partial order $\leq$, if multiplication on the right is monotone (i.e., $a \leq b$ implies $a * c \leq b * c$ for all $a, b, c \in N$), then multiplication on the right is strictly monotone (i.e., $a < b$ implies $a * c < b * c$ for all $a, b, c \in N$).

IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT instance

[Mul N] [IsLeftCancelMul N] [PartialOrder N] [MulLeftReflectLT N] : MulLeftReflectLE N

Full source

@[to_additive]
instance IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT [Mul N] [IsLeftCancelMul N]
    [PartialOrder N] [MulLeftReflectLT N] :
    MulLeftReflectLE N where
  elim := (contravariant_le_iff_contravariant_lt_and_eq N N _).mpr
    ⟨ContravariantClass.elim, fun _ ↦ mul_left_cancel⟩

Reflection of Non-Strict Order from Strict Order in Left Cancellative Structures

Informal description

For any left cancellative multiplicative structure $N$ with a partial order, if left multiplication reflects the strict order (i.e., $a \cdot b_1 < a \cdot b_2$ implies $b_1 < b_2$ for all $a, b_1, b_2 \in N$), then left multiplication also reflects the non-strict order (i.e., $a \cdot b_1 \leq a \cdot b_2$ implies $b_1 \leq b_2$ for all $a, b_1, b_2 \in N$).

IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT instance

[Mul N] [IsRightCancelMul N] [PartialOrder N] [MulRightReflectLT N] : MulRightReflectLE N

Full source

@[to_additive]
instance IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT
    [Mul N] [IsRightCancelMul N] [PartialOrder N] [MulRightReflectLT N] :
    MulRightReflectLE N where
  elim := (contravariant_le_iff_contravariant_lt_and_eq N N _).mpr
    ⟨ContravariantClass.elim, fun _ ↦ mul_right_cancel⟩

Reflection of Non-strict Order from Strict Order in Right Cancellative Structures

Informal description

For any type $N$ with a right cancellative multiplication operation and a partial order $\leq$, if multiplication on the right reflects the strict order $<$ (i.e., $a * c < b * c$ implies $a < b$ for all $a, b, c \in N$), then it also reflects the non-strict order $\leq$ (i.e., $a * c \leq b * c$ implies $a \leq b$ for all $a, b, c \in N$).

Formalization notes