Mathlib.Algebra.Order.Hom.Basic

Module docstring

{"# Algebraic order homomorphism classes

This file defines hom classes for common properties at the intersection of order theory and algebra.

Typeclasses

Basic typeclasses * NonnegHomClass: Homs are nonnegative: ∀ f a, 0 ≤ f a * SubadditiveHomClass: Homs are subadditive: ∀ f a b, f (a + b) ≤ f a + f b * SubmultiplicativeHomClass: Homs are submultiplicative: ∀ f a b, f (a * b) ≤ f a * f b * MulLEAddHomClass: ∀ f a b, f (a * b) ≤ f a + f b * NonarchimedeanHomClass: ∀ a b, f (a + b) ≤ max (f a) (f b)

Group norms * AddGroupSeminormClass: Homs are nonnegative, subadditive, even and preserve zero. * GroupSeminormClass: Homs are nonnegative, respect f (a * b) ≤ f a + f b, f a⁻¹ = f a and preserve zero. * AddGroupNormClass: Homs are seminorms such that f x = 0 → x = 0 for all x. * GroupNormClass: Homs are seminorms such that f x = 0 → x = 1 for all x.

Ring norms * RingSeminormClass: Homs are submultiplicative group norms. * RingNormClass: Homs are ring seminorms that are also additive group norms. * MulRingSeminormClass: Homs are ring seminorms that are multiplicative. * MulRingNormClass: Homs are ring norms that are multiplicative.

Notes

Typeclasses for seminorms are defined here while types of seminorms are defined in Analysis.Normed.Group.Seminorm and Analysis.Normed.Ring.Seminorm because absolute values are multiplicative ring norms but outside of this use we only consider real-valued seminorms.

TODO

Finitary versions of the current lemmas. ","### Basics ","### Group (semi)norms ","### Ring (semi)norms "}

NonnegHomClass structure

(F : Type*) (α β : outParam Type*) [Zero β] [LE β] [FunLike F α β]

Full source

/-- `NonnegHomClass F α β` states that `F` is a type of nonnegative morphisms. -/
class NonnegHomClass (F : Type*) (α β : outParam Type*) [Zero β] [LE β] [FunLike F α β] : Prop where
  /-- the image of any element is non negative. -/
  apply_nonneg (f : F) : ∀ a, 0 ≤ f a

Nonnegative Homomorphism Class

Informal description

The class `NonnegHomClass F α β` states that for any type `F` with a function-like structure from `α` to `β`, where `β` has a zero element and a partial order, every element `f : F` is nonnegative, i.e., satisfies `0 ≤ f a` for all `a : α`.

SubadditiveHomClass structure

(F : Type*) (α β : outParam Type*) [Add α] [Add β] [LE β] [FunLike F α β]

Full source

/-- `SubadditiveHomClass F α β` states that `F` is a type of subadditive morphisms. -/
class SubadditiveHomClass (F : Type*) (α β : outParam Type*)
    [Add α] [Add β] [LE β] [FunLike F α β] : Prop where
  /-- the image of a sum is less or equal than the sum of the images. -/
  map_add_le_add (f : F) : ∀ a b, f (a + b) ≤ f a + f b

Subadditive Homomorphism Class

Informal description

The structure `SubadditiveHomClass F α β` represents a class of subadditive morphisms, where for any `f : F`, the map `f : α → β` satisfies the subadditivity condition: for all `a, b ∈ α`, we have `f (a + b) ≤ f a + f b`.

SubmultiplicativeHomClass structure

(F : Type*) (α β : outParam (Type*)) [Mul α] [Mul β] [LE β] [FunLike F α β]

Full source

/-- `SubmultiplicativeHomClass F α β` states that `F` is a type of submultiplicative morphisms. -/
@[to_additive SubadditiveHomClass]
class SubmultiplicativeHomClass (F : Type*) (α β : outParam (Type*)) [Mul α] [Mul β] [LE β]
    [FunLike F α β] : Prop where
  /-- the image of a product is less or equal than the product of the images. -/
  map_mul_le_mul (f : F) : ∀ a b, f (a * b) ≤ f a * f b

Submultiplicative Homomorphism Class

Informal description

The structure `SubmultiplicativeHomClass F α β` represents a class of submultiplicative morphisms, where for any `f : F`, the map `f : α → β` satisfies the submultiplicativity condition: for all `a, b ∈ α$, we have `f (a * b) ≤ f a * f b`. Here, `α` and `β` are types equipped with multiplication operations, and `β` is also equipped with a partial order.

MulLEAddHomClass structure

(F : Type*) (α β : outParam Type*) [Mul α] [Add β] [LE β] [FunLike F α β]

Full source

/-- `MulLEAddHomClass F α β` states that `F` is a type of subadditive morphisms. -/
@[to_additive SubadditiveHomClass]
class MulLEAddHomClass (F : Type*) (α β : outParam Type*) [Mul α] [Add β] [LE β] [FunLike F α β] :
    Prop where
  /-- the image of a product is less or equal than the sum of the images. -/
  map_mul_le_add (f : F) : ∀ a b, f (a * b) ≤ f a + f b

Submultiplicative-to-additive homomorphism class

Informal description

The structure `MulLEAddHomClass F α β` represents a class of morphisms where for any `f : F`, the map `f : α → β` satisfies the property that for all `a, b ∈ α`, we have `f (a * b) ≤ f a + f b`. Here, `α` is equipped with a multiplication operation and `β` is equipped with an addition operation and a partial order.

NonarchimedeanHomClass structure

(F : Type*) (α β : outParam Type*) [Add α] [LinearOrder β] [FunLike F α β]

Full source

/-- `NonarchimedeanHomClass F α β` states that `F` is a type of non-archimedean morphisms. -/
class NonarchimedeanHomClass (F : Type*) (α β : outParam Type*)
    [Add α] [LinearOrder β] [FunLike F α β] : Prop where
  /-- the image of a sum is less or equal than the maximum of the images. -/
  map_add_le_max (f : F) : ∀ a b, f (a + b) ≤ max (f a) (f b)

Non-archimedean homomorphism class

Informal description

The structure `NonarchimedeanHomClass F α β` represents a class of non-archimedean morphisms, where for any `f : F`, the map `f : α → β` satisfies the property that for all `a, b ∈ α`, we have `f (a + b) ≤ max (f a, f b)`. Here, `α` is equipped with an addition operation and `β` is a linearly ordered type.

le_map_mul_map_div theorem

[Group α] [CommMagma β] [LE β] [SubmultiplicativeHomClass F α β] (f : F) (a b : α) : f a ≤ f b * f (a / b)

Full source

@[to_additive]
theorem le_map_mul_map_div [Group α] [CommMagma β] [LE β] [SubmultiplicativeHomClass F α β]
    (f : F) (a b : α) : f a ≤ f b * f (a / b) := by
  simpa only [mul_comm, div_mul_cancel] using map_mul_le_mul f (a / b) b

Submultiplicative Homomorphism Inequality: $f(a) \leq f(b) \cdot f(a/b)$

Informal description

Let $\alpha$ be a group and $\beta$ be a commutative magma equipped with a partial order $\leq$. For any submultiplicative homomorphism $f \colon \alpha \to \beta$ (i.e., satisfying $f(a * b) \leq f(a) * f(b)$ for all $a, b \in \alpha$) and for any elements $a, b \in \alpha$, we have the inequality: \[ f(a) \leq f(b) * f(a / b). \]

le_map_add_map_div theorem

[Group α] [AddCommMagma β] [LE β] [MulLEAddHomClass F α β] (f : F) (a b : α) : f a ≤ f b + f (a / b)

Full source

@[to_additive existing]
theorem le_map_add_map_div [Group α] [AddCommMagma β] [LE β] [MulLEAddHomClass F α β] (f : F)
    (a b : α) : f a ≤ f b + f (a / b) := by
  simpa only [add_comm, div_mul_cancel] using map_mul_le_add f (a / b) b

Inequality for submultiplicative-to-additive homomorphisms: $f(a) \leq f(b) + f(a / b)$

Informal description

Let $\alpha$ be a group and $\beta$ be an additive commutative magma with a partial order $\leq$. For any function $f \colon \alpha \to \beta$ in the class `MulLEAddHomClass` (i.e., satisfying $f(a * b) \leq f(a) + f(b)$ for all $a, b \in \alpha$), and for any elements $a, b \in \alpha$, we have the inequality: \[ f(a) \leq f(b) + f(a / b). \]

le_map_div_mul_map_div theorem

 [Group α] [Mul β] [LE β] [SubmultiplicativeHomClass F α β] (f : F) (a b c : α) : f (a / c) ≤ f (a / b) * f (b / c)

Full source

@[to_additive]
theorem le_map_div_mul_map_div [Group α] [Mul β] [LE β] [SubmultiplicativeHomClass F α β]
    (f : F) (a b c : α) : f (a / c) ≤ f (a / b) * f (b / c) := by
  simpa only [div_mul_div_cancel] using map_mul_le_mul f (a / b) (b / c)

Submultiplicative Homomorphism Inequality for Group Division: $f(a/c) \leq f(a/b) \cdot f(b/c)$

Informal description

Let $\alpha$ be a group and $\beta$ be a multiplicative magma equipped with a partial order $\leq$. For any submultiplicative homomorphism $f \colon \alpha \to \beta$ (i.e., satisfying $f(a * b) \leq f(a) * f(b)$ for all $a, b \in \alpha$) and for any elements $a, b, c \in \alpha$, we have the inequality: \[ f(a / c) \leq f(a / b) \cdot f(b / c). \]

le_map_div_add_map_div theorem

[Group α] [Add β] [LE β] [MulLEAddHomClass F α β] (f : F) (a b c : α) : f (a / c) ≤ f (a / b) + f (b / c)

Full source

@[to_additive existing]
theorem le_map_div_add_map_div [Group α] [Add β] [LE β] [MulLEAddHomClass F α β]
    (f : F) (a b c : α) : f (a / c) ≤ f (a / b) + f (b / c) := by
    simpa only [div_mul_div_cancel] using map_mul_le_add f (a / b) (b / c)

Triangle Inequality for Group Division under Submultiplicative-to-Additive Homomorphisms

Informal description

Let $\alpha$ be a group and $\beta$ be an additive magma with a partial order $\leq$. For any function $f \colon \alpha \to \beta$ in the class `MulLEAddHomClass` (i.e., satisfying $f(a * b) \leq f(a) + f(b)$ for all $a, b \in \alpha$), and for any elements $a, b, c \in \alpha$, we have the inequality: \[ f(a / c) \leq f(a / b) + f(b / c). \]

Mathlib.Meta.Positivity.evalMap definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
@[positivity DFunLike.coe _ _]
def evalMap : PositivityExt where eval {_ β} _ _ e := do
  let .app (.app _ f) a ← whnfR e
    | throwError "not ↑f · where f is of NonnegHomClass"
  let pa ← mkAppOptM ``apply_nonneg #[none, none, β, none, none, none, none, f, a]
  pure (.nonnegative pa)

Positivity extension for nonnegative homomorphisms

Informal description

The tactic extension for positivity that proves expressions of the form `f a` are nonnegative when `f` is a function from a class of nonnegative homomorphisms (i.e., functions satisfying `∀ f a, 0 ≤ f a`).

AddGroupSeminormClass structure

(F : Type*) (α β : outParam Type*)
    [AddGroup α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] : Prop
  extends SubadditiveHomClass F α β

Full source

/-- `AddGroupSeminormClass F α` states that `F` is a type of `β`-valued seminorms on the additive
group `α`.

You should extend this class when you extend `AddGroupSeminorm`. -/
class AddGroupSeminormClass (F : Type*) (α β : outParam Type*)
    [AddGroup α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] : Prop
  extends SubadditiveHomClass F α β where
  /-- The image of zero is zero. -/
  map_zero (f : F) : f 0 = 0
  /-- The map is invariant under negation of its argument. -/
  map_neg_eq_map (f : F) (a : α) : f (-a) = f a

Additive Group Seminorm Class

Informal description

The class `AddGroupSeminormClass F α β` states that `F` is a type of `β`-valued seminorms on the additive group `α`. A seminorm of this type is a function that is nonnegative, subadditive (i.e., satisfies the triangle inequality), even (i.e., satisfies $f(-a) = f(a)$), and preserves zero (i.e., $f(0) = 0$).

GroupSeminormClass structure

(F : Type*) (α β : outParam Type*)
    [Group α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] : Prop
  extends MulLEAddHomClass F α β

Full source

/-- `GroupSeminormClass F α` states that `F` is a type of `β`-valued seminorms on the group `α`.

You should extend this class when you extend `GroupSeminorm`. -/
@[to_additive]
class GroupSeminormClass (F : Type*) (α β : outParam Type*)
    [Group α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] : Prop
  extends MulLEAddHomClass F α β where
  /-- The image of one is zero. -/
  map_one_eq_zero (f : F) : f 1 = 0
  /-- The map is invariant under inversion of its argument. -/
  map_inv_eq_map (f : F) (a : α) : f a⁻¹ = f a

Group Seminorm Class

Informal description

The structure `GroupSeminormClass F α β` represents a class of $\beta$-valued seminorms on the group $\alpha$, where $\beta$ is an additively written commutative monoid with a partial order. A function $f \colon \alpha \to \beta$ in this class satisfies the following properties: 1. (Nonnegativity) $0 \leq f(a)$ for all $a \in \alpha$, 2. (Subadditivity) $f(a \cdot b) \leq f(a) + f(b)$ for all $a, b \in \alpha$, 3. (Inversion invariance) $f(a^{-1}) = f(a)$ for all $a \in \alpha$, 4. (Preservation of identity) $f(1) = 0$. This class extends `MulLEAddHomClass` and is used to define group seminorms.

AddGroupNormClass structure

(F : Type*) (α β : outParam Type*)
    [AddGroup α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] : Prop
  extends AddGroupSeminormClass F α β

Full source

/-- `AddGroupNormClass F α` states that `F` is a type of `β`-valued norms on the additive group
`α`.

You should extend this class when you extend `AddGroupNorm`. -/
class AddGroupNormClass (F : Type*) (α β : outParam Type*)
    [AddGroup α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] : Prop
  extends AddGroupSeminormClass F α β where
  /-- The argument is zero if its image under the map is zero. -/
  eq_zero_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 0

Additive Group Norm Class

Informal description

The structure `AddGroupNormClass F α β` represents a class of $\beta$-valued norms on the additive group $\alpha$, where $\beta$ is an additively written commutative monoid with a partial order. A function $f \colon \alpha \to \beta$ in this class satisfies the following properties: 1. (Nonnegativity) $0 \leq f(a)$ for all $a \in \alpha$, 2. (Subadditivity) $f(a + b) \leq f(a) + f(b)$ for all $a, b \in \alpha$, 3. (Evenness) $f(-a) = f(a)$ for all $a \in \alpha$, 4. (Positivity) $f(a) = 0$ implies $a = 0$ for all $a \in \alpha$. This class extends `AddGroupSeminormClass` and is used to define additive group norms.

GroupNormClass structure

(F : Type*) (α β : outParam Type*)
    [Group α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] : Prop
  extends GroupSeminormClass F α β

Full source

/-- `GroupNormClass F α` states that `F` is a type of `β`-valued norms on the group `α`.

You should extend this class when you extend `GroupNorm`. -/
@[to_additive]
class GroupNormClass (F : Type*) (α β : outParam Type*)
    [Group α] [AddCommMonoid β] [PartialOrder β] [FunLike F α β] : Prop
  extends GroupSeminormClass F α β where
  /-- The argument is one if its image under the map is zero. -/
  eq_one_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 1

Group Norm Class

Informal description

The structure `GroupNormClass F α β` represents a class of $\beta$-valued norms on the group $\alpha$, where $\beta$ is an additively written commutative monoid with a partial order. A function $f \colon \alpha \to \beta$ in this class satisfies the following properties: 1. (Nonnegativity) $0 \leq f(a)$ for all $a \in \alpha$, 2. (Subadditivity) $f(a \cdot b) \leq f(a) + f(b)$ for all $a, b \in \alpha$, 3. (Inversion invariance) $f(a^{-1}) = f(a)$ for all $a \in \alpha$, 4. (Positivity) $f(a) = 0$ implies $a = 1$ for all $a \in \alpha$. This class extends `GroupSeminormClass` and is used to define group norms.

AddGroupSeminormClass.toZeroHomClass instance

[AddGroup α] [AddCommMonoid β] [PartialOrder β] [AddGroupSeminormClass F α β] : ZeroHomClass F α β

Full source

instance (priority := 100) AddGroupSeminormClass.toZeroHomClass [AddGroup α]
    [AddCommMonoid β] [PartialOrder β] [AddGroupSeminormClass F α β] : ZeroHomClass F α β :=
  { ‹AddGroupSeminormClass F α β› with }

Additive Group Seminorms Preserve Zero

Informal description

For any additive group $\alpha$ and additive commutative monoid $\beta$ with a partial order, every additive group seminorm $f \colon \alpha \to \beta$ preserves zero, i.e., $f(0) = 0$.

map_div_le_add theorem

: f (x / y) ≤ f x + f y

Full source

@[to_additive]
theorem map_div_le_add : f (x / y) ≤ f x + f y := by
  rw [div_eq_mul_inv, ← map_inv_eq_map f y]
  exact map_mul_le_add _ _ _

Subadditivity of Group Seminorm under Division

Informal description

For any group seminorm $f$ on a group $\alpha$ and any elements $x, y \in \alpha$, the seminorm satisfies the inequality $f(x / y) \leq f(x) + f(y)$.

map_div_rev theorem

: f (x / y) = f (y / x)

Full source

@[to_additive]
theorem map_div_rev : f (x / y) = f (y / x) := by rw [← inv_div, map_inv_eq_map]

Symmetric Property of Group Seminorm under Division

Informal description

For any group seminorm $f$ on a group $\alpha$ and any elements $x, y \in \alpha$, the seminorm satisfies $f(x / y) = f(y / x)$.

le_map_add_map_div' theorem

: f x ≤ f y + f (y / x)

Full source

@[to_additive]
theorem le_map_add_map_div' : f x ≤ f y + f (y / x) := by
  simpa only [add_comm, map_div_rev, div_mul_cancel] using map_mul_le_add f (x / y) y

Triangle Inequality for Group Seminorm with Division

Informal description

For any group seminorm $f$ on a group $\alpha$ and any elements $x, y \in \alpha$, the seminorm satisfies the inequality $f(x) \leq f(y) + f(y / x)$.

abs_sub_map_le_div theorem

 [Group α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupSeminormClass F α β] (f : F) (x y : α) :
  |f x - f y| ≤ f (x / y)

Full source

@[to_additive]
theorem abs_sub_map_le_div [Group α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β]
    [GroupSeminormClass F α β]
    (f : F) (x y : α) : |f x - f y| ≤ f (x / y) := by
  rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']
  exact ⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩

Lipschitz-type Inequality for Group Seminorms: $|f(x) - f(y)| \leq f(x / y)$

Informal description

Let $\alpha$ be a group and $\beta$ be an additively written commutative group with a linear order that makes it an ordered additive monoid. For any group seminorm $f \colon \alpha \to \beta$ (i.e., a function satisfying $f(1) = 0$, $f(a^{-1}) = f(a)$, and $f(ab) \leq f(a) + f(b)$ for all $a, b \in \alpha$) and any elements $x, y \in \alpha$, the following inequality holds: \[ |f(x) - f(y)| \leq f(x / y). \]

GroupSeminormClass.toNonnegHomClass instance

 [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupSeminormClass F α β] : NonnegHomClass F α β

Full source

@[to_additive]
instance (priority := 100) GroupSeminormClass.toNonnegHomClass [Group α]
    [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupSeminormClass F α β] :
    NonnegHomClass F α β :=
  { ‹GroupSeminormClass F α β› with
    apply_nonneg := fun f a =>
      (nsmul_nonneg_iff two_ne_zero).1 <| by
        rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]
        exact map_div_le_add _ _ _ }

Group Seminorms are Nonnegative Homomorphisms

Informal description

For any group $\alpha$, additive commutative monoid $\beta$ with a linear order and ordered additive monoid structure, and any type $F$ that is a group seminorm class from $\alpha$ to $\beta$, the elements of $F$ are nonnegative homomorphisms. That is, for any $f \in F$ and $a \in \alpha$, we have $0 \leq f(a)$.

map_eq_zero_iff_eq_one theorem

: f x = 0 ↔ x = 1

Full source

@[to_additive]
theorem map_eq_zero_iff_eq_one : f x = 0 ↔ x = 1 :=
  ⟨eq_one_of_map_eq_zero _, by
    rintro rfl
    exact map_one_eq_zero _⟩

Characterization of Group Norm Vanishing at Identity

Informal description

For a group norm $f$ on a group $\alpha$ with values in an ordered additive commutative monoid $\beta$, the norm $f(x)$ equals zero if and only if $x$ is the identity element of $\alpha$, i.e., $f(x) = 0 \leftrightarrow x = 1$.

map_ne_zero_iff_ne_one theorem

: f x ≠ 0 ↔ x ≠ 1

Full source

@[to_additive]
theorem map_ne_zero_iff_ne_one : f x ≠ 0f x ≠ 0 ↔ x ≠ 1 :=
  (map_eq_zero_iff_eq_one _).not

Nonzero Norm Characterization for Non-Identity Elements

Informal description

For a group norm $f$ on a group $\alpha$ with values in an ordered additive commutative monoid $\beta$, the norm $f(x)$ is nonzero if and only if $x$ is not the identity element of $\alpha$, i.e., $f(x) \neq 0 \leftrightarrow x \neq 1$.

map_pos_of_ne_one theorem

 [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [GroupNormClass F α β] (f : F) {x : α}
  (hx : x ≠ 1) : 0 < f x

Full source

@[to_additive]
theorem map_pos_of_ne_one [Group α] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β]
    [GroupNormClass F α β] (f : F)
    {x : α} (hx : x ≠ 1) : 0 < f x :=
  (apply_nonneg _ _).lt_of_ne <| ((map_ne_zero_iff_ne_one _).2 hx).symm

Positivity of Group Norm for Non-Identity Elements

Informal description

Let $\alpha$ be a group and $\beta$ be a linearly ordered additive commutative monoid. For any group norm $f \colon \alpha \to \beta$ in the group norm class $F$ and any element $x \in \alpha$ such that $x \neq 1$, the norm $f(x)$ is strictly positive, i.e., $0 < f(x)$.

RingSeminormClass structure

(F : Type*) (α β : outParam Type*)
    [NonUnitalNonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
  extends AddGroupSeminormClass F α β, SubmultiplicativeHomClass F α β

Full source

/-- `RingSeminormClass F α` states that `F` is a type of `β`-valued seminorms on the ring `α`.

You should extend this class when you extend `RingSeminorm`. -/
class RingSeminormClass (F : Type*) (α β : outParam Type*)
    [NonUnitalNonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
  extends AddGroupSeminormClass F α β, SubmultiplicativeHomClass F α β

Ring Seminorm Class

Informal description

The class `RingSeminormClass F α β` states that `F` is a type of `β`-valued seminorms on the ring `α`. A seminorm `f : F` satisfies the following properties: 1. Nonnegativity: $0 \leq f(a)$ for all $a \in \alpha$. 2. Subadditivity: $f(a + b) \leq f(a) + f(b)$ for all $a, b \in \alpha$. 3. Submultiplicativity: $f(a * b) \leq f(a) * f(b)$ for all $a, b \in \alpha$. 4. Evenness: $f(-a) = f(a)$ for all $a \in \alpha$. 5. Preserves zero: $f(0) = 0$. This class extends `AddGroupSeminormClass` and `SubmultiplicativeHomClass` to combine both additive and multiplicative properties of seminorms on rings.

RingNormClass structure

(F : Type*) (α β : outParam Type*)
    [NonUnitalNonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
  extends RingSeminormClass F α β, AddGroupNormClass F α β

Full source

/-- `RingNormClass F α` states that `F` is a type of `β`-valued norms on the ring `α`.

You should extend this class when you extend `RingNorm`. -/
class RingNormClass (F : Type*) (α β : outParam Type*)
    [NonUnitalNonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
  extends RingSeminormClass F α β, AddGroupNormClass F α β

Ring Norm Class

Informal description

The class `RingNormClass F α β` represents a type of functions `F` from a non-unital non-associative ring `α` to a semiring `β` with a partial order, where each function `f : F` is a ring norm satisfying the following properties: 1. Nonnegativity: $0 \leq f(a)$ for all $a \in \alpha$ 2. Subadditivity: $f(a + b) \leq f(a) + f(b)$ for all $a, b \in \alpha$ 3. Submultiplicativity: $f(a * b) \leq f(a) * f(b)$ for all $a, b \in \alpha$ 4. Evenness: $f(-a) = f(a)$ for all $a \in \alpha$ 5. Preservation of zero: $f(0) = 0$ 6. Definiteness: $f(x) = 0$ implies $x = 0$ for all $x \in \alpha$ This class extends both `RingSeminormClass` and `AddGroupNormClass`, combining their properties to describe norms on rings.

MulRingSeminormClass structure

(F : Type*) (α β : outParam Type*)
    [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
  extends AddGroupSeminormClass F α β, MonoidWithZeroHomClass F α β

Full source

/-- `MulRingSeminormClass F α` states that `F` is a type of `β`-valued multiplicative seminorms
on the ring `α`.

You should extend this class when you extend `MulRingSeminorm`. -/
class MulRingSeminormClass (F : Type*) (α β : outParam Type*)
    [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
  extends AddGroupSeminormClass F α β, MonoidWithZeroHomClass F α β

Multiplicative Ring Seminorm Class

Informal description

The structure `MulRingSeminormClass F α β` represents a class of multiplicative ring seminorms, where `F` is a type of functions from a non-associative ring `α$ to a semiring $\beta$ with a partial order. A function `f : F` is a multiplicative ring seminorm if it satisfies the following properties: 1. Nonnegativity: $0 \leq f(a)$ for all $a \in \alpha$ 2. Subadditivity: $f(a + b) \leq f(a) + f(b)$ for all $a, b \in \alpha$ 3. Multiplicativity: $f(a * b) = f(a) * f(b)$ for all $a, b \in \alpha$ 4. Evenness: $f(-a) = f(a)$ for all $a \in \alpha$ 5. Preservation of zero: $f(0) = 0$ This class extends both `AddGroupSeminormClass` and `MonoidWithZeroHomClass`, combining their properties to describe multiplicative seminorms on rings.

MulRingNormClass structure

(F : Type*) (α β : outParam Type*)
    [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
  extends MulRingSeminormClass F α β, AddGroupNormClass F α β

Full source

/-- `MulRingNormClass F α` states that `F` is a type of `β`-valued multiplicative norms on the
ring `α`.

You should extend this class when you extend `MulRingNorm`. -/
class MulRingNormClass (F : Type*) (α β : outParam Type*)
    [NonAssocRing α] [Semiring β] [PartialOrder β] [FunLike F α β] : Prop
  extends MulRingSeminormClass F α β, AddGroupNormClass F α β

Multiplicative Ring Norm Class

Informal description

The structure `MulRingNormClass F α β` represents a class of multiplicative ring norms, where `F` is a type of functions from a non-associative ring `α` to a semiring `β` with a partial order. A function `f : F` is a multiplicative ring norm if it satisfies the following properties: 1. It is a multiplicative ring seminorm (preserves multiplication and is submultiplicative) 2. It is an additive group norm (nonnegative, subadditive, and satisfies `f x = 0` only when `x = 0`)

RingSeminormClass.toNonnegHomClass instance

 [NonUnitalNonAssocRing α] [Semiring β] [LinearOrder β] [IsOrderedAddMonoid β] [RingSeminormClass F α β] :
  NonnegHomClass F α β

Full source

instance (priority := 100) RingSeminormClass.toNonnegHomClass [NonUnitalNonAssocRing α]
    [Semiring β] [LinearOrder β] [IsOrderedAddMonoid β] [RingSeminormClass F α β] :
    NonnegHomClass F α β :=
  AddGroupSeminormClass.toNonnegHomClass

Ring Seminorms are Nonnegative

Informal description

For any non-unital non-associative ring $\alpha$, semiring $\beta$ with a linear order and ordered additive monoid structure, and type $F$ of functions from $\alpha$ to $\beta$ that forms a ring seminorm class, every function $f \in F$ is nonnegative, i.e., satisfies $0 \leq f(a)$ for all $a \in \alpha$.

MulRingSeminormClass.toRingSeminormClass instance

[NonAssocRing α] [Semiring β] [PartialOrder β] [MulRingSeminormClass F α β] : RingSeminormClass F α β

Full source

instance (priority := 100) MulRingSeminormClass.toRingSeminormClass [NonAssocRing α]
    [Semiring β] [PartialOrder β] [MulRingSeminormClass F α β] : RingSeminormClass F α β :=
  { ‹MulRingSeminormClass F α β› with map_mul_le_mul := fun _ _ _ => (map_mul _ _ _).le }

Multiplicative Ring Seminorms are Ring Seminorms

Informal description

For any non-associative ring $\alpha$, semiring $\beta$ with a partial order, and type $F$ of functions from $\alpha$ to $\beta$ that forms a multiplicative ring seminorm class, $F$ also forms a ring seminorm class. This means that every multiplicative ring seminorm is also a ring seminorm, inheriting the properties of nonnegativity, subadditivity, submultiplicativity, evenness, and preservation of zero.

MulRingNormClass.toRingNormClass instance

[NonAssocRing α] [Semiring β] [PartialOrder β] [MulRingNormClass F α β] : RingNormClass F α β

Full source

instance (priority := 100) MulRingNormClass.toRingNormClass [NonAssocRing α]
    [Semiring β] [PartialOrder β] [MulRingNormClass F α β] : RingNormClass F α β :=
  { ‹MulRingNormClass F α β›, MulRingSeminormClass.toRingSeminormClass with }

Multiplicative Ring Norms are Ring Norms

Informal description

For any non-associative ring $\alpha$, semiring $\beta$ with a partial order, and type $F$ of functions from $\alpha$ to $\beta$ that forms a multiplicative ring norm class, $F$ also forms a ring norm class. This means that every multiplicative ring norm is also a ring norm, inheriting the properties of nonnegativity, subadditivity, submultiplicativity, evenness, preservation of zero, and definiteness.