Documentation

Mathlib.Algebra.Order.Hom.Basic

Algebraic order homomorphism classes #

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

Typeclasses #

Basic typeclasses

Group norms

Ring norms

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 #

class NonnegHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Zero β] [inst : LE β] extends FunLike :
Type (max(maxu_1u_2)u_3)
  • the image of any element is non negative.

    map_nonneg : ∀ (f : F) (a : α), 0 f a

NonnegHomClass F α β states that F is a type of nonnegative morphisms.

Instances
    class SubadditiveHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Add α] [inst : Add β] [inst : LE β] extends FunLike :
    Type (max(maxu_1u_2)u_3)
    • 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

    SubadditiveHomClass F α β states that F is a type of subadditive morphisms.

    Instances
      class SubmultiplicativeHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Mul α] [inst : Mul β] [inst : LE β] extends FunLike :
      Type (max(maxu_1u_2)u_3)
      • 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

      SubmultiplicativeHomClass F α β states that F is a type of submultiplicative morphisms.

      Instances
        class MulLEAddHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Mul α] [inst : Add β] [inst : LE β] extends FunLike :
        Type (max(maxu_1u_2)u_3)
        • 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

        MulLEAddHomClass F α β states that F is a type of subadditive morphisms.

        Instances
          class NonarchimedeanHomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Add α] [inst : LinearOrder β] extends FunLike :
          Type (max(maxu_1u_2)u_3)
          • 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)

          NonarchimedeanHomClass F α β states that F is a type of non-archimedean morphisms.

          Instances
            theorem le_map_add_map_sub {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : AddCommSemigroup β] [inst : LE β] [inst : SubadditiveHomClass F α β] (f : F) (a : α) (b : α) :
            f a f b + f (a - b)
            theorem le_map_mul_map_div {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : CommSemigroup β] [inst : LE β] [inst : SubmultiplicativeHomClass F α β] (f : F) (a : α) (b : α) :
            f a f b * f (a / b)
            theorem le_map_add_map_div {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : AddCommSemigroup β] [inst : LE β] [inst : MulLEAddHomClass F α β] (f : F) (a : α) (b : α) :
            f a f b + f (a / b)
            theorem le_map_sub_add_map_sub {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : AddCommSemigroup β] [inst : LE β] [inst : SubadditiveHomClass F α β] (f : F) (a : α) (b : α) (c : α) :
            f (a - c) f (a - b) + f (b - c)
            theorem le_map_div_mul_map_div {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : CommSemigroup β] [inst : LE β] [inst : SubmultiplicativeHomClass F α β] (f : F) (a : α) (b : α) (c : α) :
            f (a / c) f (a / b) * f (b / c)
            theorem le_map_div_add_map_div {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : AddCommSemigroup β] [inst : LE β] [inst : MulLEAddHomClass F α β] (f : F) (a : α) (b : α) (c : α) :
            f (a / c) f (a / b) + f (b / c)

            Group (semi)norms #

            class AddGroupSeminormClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : AddGroup α] [inst : OrderedAddCommMonoid β] extends SubadditiveHomClass :
            Type (max(maxu_1u_2)u_3)
            • 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

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

            You should extend this class when you extend AddGroupSeminorm.

            Instances
              class GroupSeminormClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Group α] [inst : OrderedAddCommMonoid β] extends MulLEAddHomClass :
              Type (max(maxu_1u_2)u_3)
              • 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

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

              You should extend this class when you extend GroupSeminorm.

              Instances
                class AddGroupNormClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : AddGroup α] [inst : OrderedAddCommMonoid β] extends AddGroupSeminormClass :
                Type (max(maxu_1u_2)u_3)
                • The argument is zero if its image under the map is zero.

                  eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, f a = 0a = 0

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

                You should extend this class when you extend AddGroupNorm.

                Instances
                  class GroupNormClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : Group α] [inst : OrderedAddCommMonoid β] extends GroupSeminormClass :
                  Type (max(maxu_1u_2)u_3)
                  • The argument is one if its image under the map is zero.

                    eq_one_of_map_eq_zero : ∀ (f : F) {a : α}, f a = 0a = 1

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

                  You should extend this class when you extend GroupNorm.

                  Instances
                    instance AddGroupSeminormClass.toAddLEAddHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
                    {inst : AddGroup α} → {inst_1 : OrderedAddCommMonoid β} → [self : AddGroupSeminormClass F α β] → SubadditiveHomClass F α β
                    Equations
                    • AddGroupSeminormClass.toAddLEAddHomClass = self.1
                    instance AddGroupSeminormClass.toZeroHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
                    {x : AddGroup α} → {x_1 : OrderedAddCommMonoid β} → [inst : AddGroupSeminormClass F α β] → ZeroHomClass F α β
                    Equations
                    • AddGroupSeminormClass.toZeroHomClass = let src := inst; ZeroHomClass.mk (_ : ∀ (f : F), f 0 = 0)
                    theorem map_sub_le_add {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : OrderedAddCommMonoid β] [inst : AddGroupSeminormClass F α β] (f : F) (x : α) (y : α) :
                    f (x - y) f x + f y
                    theorem map_div_le_add {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : OrderedAddCommMonoid β] [inst : GroupSeminormClass F α β] (f : F) (x : α) (y : α) :
                    f (x / y) f x + f y
                    theorem map_sub_rev {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : OrderedAddCommMonoid β] [inst : AddGroupSeminormClass F α β] (f : F) (x : α) (y : α) :
                    f (x - y) = f (y - x)
                    theorem map_div_rev {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : OrderedAddCommMonoid β] [inst : GroupSeminormClass F α β] (f : F) (x : α) (y : α) :
                    f (x / y) = f (y / x)
                    theorem le_map_add_map_sub' {F : Type u_2} {α : Type u_3} {β : Type u_1} [inst : AddGroup α] [inst : OrderedAddCommMonoid β] [inst : AddGroupSeminormClass F α β] (f : F) (x : α) (y : α) :
                    f x f y + f (y - x)
                    theorem le_map_add_map_div' {F : Type u_2} {α : Type u_3} {β : Type u_1} [inst : Group α] [inst : OrderedAddCommMonoid β] [inst : GroupSeminormClass F α β] (f : F) (x : α) (y : α) :
                    f x f y + f (y / x)
                    theorem abs_sub_map_le_sub {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : LinearOrderedAddCommGroup β] [inst : AddGroupSeminormClass F α β] (f : F) (x : α) (y : α) :
                    abs (f x - f y) f (x - y)
                    theorem abs_sub_map_le_div {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : LinearOrderedAddCommGroup β] [inst : GroupSeminormClass F α β] (f : F) (x : α) (y : α) :
                    abs (f x - f y) f (x / y)
                    instance AddGroupSeminormClass.toNonnegHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
                    {x : AddGroup α} → {x_1 : LinearOrderedAddCommMonoid β} → [inst : AddGroupSeminormClass F α β] → NonnegHomClass F α β
                    Equations
                    • AddGroupSeminormClass.toNonnegHomClass = let src := inst; NonnegHomClass.mk (_ : ∀ (f : F) (a : α), 0 f a)
                    def AddGroupSeminormClass.toNonnegHomClass.proof_1 {F : Type u_2} {α : Type u_3} {β : Type u_1} :
                    ∀ {x : AddGroup α} {x_1 : LinearOrderedAddCommMonoid β} [inst : AddGroupSeminormClass F α β] (f : F) (a : α), 0 f a
                    Equations
                    • (_ : 0 f a) = (_ : 0 f a)
                    instance GroupSeminormClass.toNonnegHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
                    {x : Group α} → {x_1 : LinearOrderedAddCommMonoid β} → [inst : GroupSeminormClass F α β] → NonnegHomClass F α β
                    Equations
                    • GroupSeminormClass.toNonnegHomClass = let src := inst; NonnegHomClass.mk (_ : ∀ (f : F) (a : α), 0 f a)
                    @[simp]
                    theorem map_eq_zero_iff_eq_zero {F : Type u_2} {α : Type u_3} {β : Type u_1} [inst : AddGroup α] [inst : OrderedAddCommMonoid β] [inst : AddGroupNormClass F α β] (f : F) {x : α} :
                    f x = 0 x = 0
                    @[simp]
                    theorem map_eq_zero_iff_eq_one {F : Type u_2} {α : Type u_3} {β : Type u_1} [inst : Group α] [inst : OrderedAddCommMonoid β] [inst : GroupNormClass F α β] (f : F) {x : α} :
                    f x = 0 x = 1
                    theorem map_ne_zero_iff_ne_zero {F : Type u_2} {α : Type u_3} {β : Type u_1} [inst : AddGroup α] [inst : OrderedAddCommMonoid β] [inst : AddGroupNormClass F α β] (f : F) {x : α} :
                    f x 0 x 0
                    theorem map_ne_zero_iff_ne_one {F : Type u_2} {α : Type u_3} {β : Type u_1} [inst : Group α] [inst : OrderedAddCommMonoid β] [inst : GroupNormClass F α β] (f : F) {x : α} :
                    f x 0 x 1
                    theorem map_pos_of_ne_zero {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : LinearOrderedAddCommMonoid β] [inst : AddGroupNormClass F α β] (f : F) {x : α} (hx : x 0) :
                    0 < f x
                    theorem map_pos_of_ne_one {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : LinearOrderedAddCommMonoid β] [inst : GroupNormClass F α β] (f : F) {x : α} (hx : x 1) :
                    0 < f x

                    Ring (semi)norms #

                    class RingSeminormClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : NonUnitalNonAssocRing α] [inst : OrderedSemiring β] extends AddGroupSeminormClass :
                    Type (max(maxu_1u_2)u_3)
                    • 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

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

                    You should extend this class when you extend RingSeminorm.

                    Instances
                      class RingNormClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : NonUnitalNonAssocRing α] [inst : OrderedSemiring β] extends RingSeminormClass :
                      Type (max(maxu_1u_2)u_3)
                      • The argument is zero if its image under the map is zero.

                        eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, f a = 0a = 0

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

                      You should extend this class when you extend RingNorm.

                      Instances
                        class MulRingSeminormClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : NonAssocRing α] [inst : OrderedSemiring β] extends AddGroupSeminormClass :
                        Type (max(maxu_1u_2)u_3)
                        • The proposition that the function preserves multiplication

                          map_mul : ∀ (f : F) (x y : α), f (x * y) = f x * f y
                        • The proposition that the function preserves 1

                          map_one : ∀ (f : F), f 1 = 1

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

                        You should extend this class when you extend MulRingSeminorm.

                        Instances
                          class MulRingNormClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [inst : NonAssocRing α] [inst : OrderedSemiring β] extends MulRingSeminormClass :
                          Type (max(maxu_1u_2)u_3)
                          • The argument is zero if its image under the map is zero.

                            eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, f a = 0a = 0

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

                          You should extend this class when you extend MulRingNorm.

                          Instances
                            instance RingSeminormClass.toNonnegHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
                            {x : NonUnitalNonAssocRing α} → {x_1 : LinearOrderedSemiring β} → [inst : RingSeminormClass F α β] → NonnegHomClass F α β
                            Equations
                            • RingSeminormClass.toNonnegHomClass = AddGroupSeminormClass.toNonnegHomClass
                            instance MulRingSeminormClass.toRingSeminormClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
                            {x : NonAssocRing α} → {x_1 : OrderedSemiring β} → [inst : MulRingSeminormClass F α β] → RingSeminormClass F α β
                            Equations
                            • MulRingSeminormClass.toRingSeminormClass = let src := inst; RingSeminormClass.mk (_ : ∀ (f : F) (a b : α), f (a * b) f a * f b)
                            instance MulRingNormClass.toRingNormClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
                            {x : NonAssocRing α} → {x_1 : OrderedSemiring β} → [inst : MulRingNormClass F α β] → RingNormClass F α β
                            Equations
                            • MulRingNormClass.toRingNormClass = let src := inst; let src_1 := MulRingSeminormClass.toRingSeminormClass; RingNormClass.mk (_ : ∀ (f : F) {a : α}, f a = 0a = 0)