Documentation

Mathlib.Analysis.Normed.Group.Hom

Normed groups homomorphisms #

This file gathers definitions and elementary constructions about bounded group homomorphisms between normed (abelian) groups (abbreviated to "normed group homs").

The main lemmas relate the boundedness condition to continuity and Lipschitzness.

The main construction is to endow the type of normed group homs between two given normed groups with a group structure and a norm, giving rise to a normed group structure. We provide several simple constructions for normed group homs, like kernel, range and equalizer.

Some easy other constructions are related to subgroups of normed groups.

Since a lot of elementary properties don't require ‖x‖ = 0 → x = 0 we start setting up the theory of SeminormedAddGroupHom and we specialize to NormedAddGroupHom when needed.

structure NormedAddGroupHom (V : Type u_1) (W : Type u_2) [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] :
Type (max u_1 u_2)

A morphism of seminormed abelian groups is a bounded group homomorphism.

Instances For
    def AddMonoidHom.mkNormedAddGroupHom {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f : V →+ W) (C : ) (h : ∀ (v : V), f v C * v) :

    Associate to a group homomorphism a bounded group homomorphism under a norm control condition.

    See AddMonoidHom.mkNormedAddGroupHom' for a version that uses ℝ≥0 for the bound.

    Equations
    Instances For
      def AddMonoidHom.mkNormedAddGroupHom' {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] (f : V →+ W) (C : NNReal) (hC : ∀ (x : V), f x‖₊ C * x‖₊) :

      Associate to a group homomorphism a bounded group homomorphism under a norm control condition.

      See AddMonoidHom.mkNormedAddGroupHom for a version that uses for the bound.

      Equations
      Instances For
        theorem exists_pos_bound_of_bound {V : Type u_1} {W : Type u_2} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] {f : VW} (M : ) (h : ∀ (x : V), f x M * x) :
        ∃ (N : ), 0 < N ∀ (x : V), f x N * x
        def NormedAddGroupHom.ofLipschitz {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {K : NNReal} (h : LipschitzWith K f) :

        A Lipschitz continuous additive homomorphism is a normed additive group homomorphism.

        Equations
        Instances For
          instance NormedAddGroupHom.funLike {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
          FunLike (NormedAddGroupHom V₁ V₂) V₁ V₂
          Equations
          • NormedAddGroupHom.funLike = { coe := NormedAddGroupHom.toFun, coe_injective' := }
          Equations
          • =
          theorem NormedAddGroupHom.coe_inj {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₁ V₂} (H : f = g) :
          f = g
          theorem NormedAddGroupHom.coe_injective {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
          Function.Injective NormedAddGroupHom.toFun
          theorem NormedAddGroupHom.coe_inj_iff {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₁ V₂} :
          f = g f = g
          theorem NormedAddGroupHom.ext {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₁ V₂} (H : ∀ (x : V₁), f x = g x) :
          f = g
          theorem NormedAddGroupHom.ext_iff {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₁ V₂} :
          f = g ∀ (x : V₁), f x = g x
          @[simp]
          theorem NormedAddGroupHom.toFun_eq_coe {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :
          f.toFun = f
          theorem NormedAddGroupHom.coe_mk {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ) (h₃ : ∀ (v : V₁), f v h₂ * v) :
          { toFun := f, map_add' := h₁, bound' := } = f
          @[simp]
          theorem NormedAddGroupHom.coe_mkNormedAddGroupHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) (C : ) (hC : ∀ (v : V₁), f v C * v) :
          @[simp]
          theorem NormedAddGroupHom.coe_mkNormedAddGroupHom' {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) (C : NNReal) (hC : ∀ (x : V₁), f x‖₊ C * x‖₊) :
          def NormedAddGroupHom.toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :
          V₁ →+ V₂

          The group homomorphism underlying a bounded group homomorphism.

          Equations
          Instances For
            theorem NormedAddGroupHom.toAddMonoidHom_injective {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
            Function.Injective NormedAddGroupHom.toAddMonoidHom
            @[simp]
            theorem NormedAddGroupHom.mk_toAddMonoidHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ∃ (C : ), ∀ (v : V₁), f v C * v) :
            NormedAddGroupHom.toAddMonoidHom { toFun := f, map_add' := h₁, bound' := h₂ } = AddMonoidHom.mk' f h₁
            theorem NormedAddGroupHom.bound {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :
            ∃ (C : ), 0 < C ∀ (x : V₁), f x C * x
            theorem NormedAddGroupHom.antilipschitz_of_norm_ge {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {K : NNReal} (h : ∀ (x : V₁), x K * f x) :
            def NormedAddGroupHom.SurjectiveOnWith {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (K : AddSubgroup V₂) (C : ) :

            A normed group hom is surjective on the subgroup K with constant C if every element x of K has a preimage whose norm is bounded above by C*‖x‖. This is a more abstract version of f having a right inverse defined on K with operator norm at most C.

            Equations
            Instances For
              theorem NormedAddGroupHom.SurjectiveOnWith.surjOn {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : } (h : NormedAddGroupHom.SurjectiveOnWith f K C) :
              Set.SurjOn (f) Set.univ K

              The operator norm #

              def NormedAddGroupHom.opNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :

              The operator norm of a seminormed group homomorphism is the inf of all its bounds.

              Equations
              Instances For
                instance NormedAddGroupHom.hasOpNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
                Equations
                • NormedAddGroupHom.hasOpNorm = { norm := NormedAddGroupHom.opNorm }
                theorem NormedAddGroupHom.norm_def {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :
                f = sInf {c : | 0 c ∀ (x : V₁), f x c * x}
                theorem NormedAddGroupHom.bounds_nonempty {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} :
                ∃ (c : ), c {c : | 0 c ∀ (x : V₁), f x c * x}
                theorem NormedAddGroupHom.bounds_bddBelow {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} :
                BddBelow {c : | 0 c ∀ (x : V₁), f x c * x}
                theorem NormedAddGroupHom.le_opNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (x : V₁) :

                The fundamental property of the operator norm: ‖f x‖ ≤ ‖f‖ * ‖x‖.

                theorem NormedAddGroupHom.le_opNorm_of_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {c : } {x : V₁} (h : x c) :
                theorem NormedAddGroupHom.le_of_opNorm_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {c : } (h : f c) (x : V₁) :
                theorem NormedAddGroupHom.lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :
                LipschitzWith { val := f, property := } f

                continuous linear maps are Lipschitz continuous.

                theorem NormedAddGroupHom.continuous {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :
                theorem NormedAddGroupHom.ratio_le_opNorm {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (x : V₁) :
                theorem NormedAddGroupHom.opNorm_le_bound {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {M : } (hMp : 0 M) (hM : ∀ (x : V₁), f x M * x) :

                If one controls the norm of every f x, then one controls the norm of f.

                theorem NormedAddGroupHom.opNorm_eq_of_bounds {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) {M : } (M_nonneg : 0 M) (h_above : ∀ (x : V₁), f x M * x) (h_below : N0, (∀ (x : V₁), f x N * x)M N) :
                theorem NormedAddGroupHom.opNorm_le_of_lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} {K : NNReal} (hf : LipschitzWith K f) :
                f K
                theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {C : } (hC : 0 C) (h : ∀ (x : V₁), f x C * x) :

                If a bounded group homomorphism map is constructed from a group homomorphism via the constructor AddMonoidHom.mkNormedAddGroupHom, then its norm is bounded by the bound given to the constructor if it is nonnegative.

                theorem NormedAddGroupHom.ofLipschitz_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {K : NNReal} (h : LipschitzWith K f) :

                If a bounded group homomorphism map is constructed from a group homomorphism via the constructor NormedAddGroupHom.ofLipschitz, then its norm is bounded by the bound given to the constructor.

                theorem NormedAddGroupHom.mkNormedAddGroupHom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {C : } (h : ∀ (x : V₁), f x C * x) :

                If a bounded group homomorphism map is constructed from a group homomorphism via the constructor AddMonoidHom.mkNormedAddGroupHom, then its norm is bounded by the bound given to the constructor or zero if this bound is negative.

                theorem AddMonoidHom.mkNormedAddGroupHom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {C : } (hC : 0 C) (h : ∀ (x : V₁), f x C * x) :

                Alias of NormedAddGroupHom.mkNormedAddGroupHom_norm_le.


                If a bounded group homomorphism map is constructed from a group homomorphism via the constructor AddMonoidHom.mkNormedAddGroupHom, then its norm is bounded by the bound given to the constructor if it is nonnegative.

                theorem AddMonoidHom.mkNormedAddGroupHom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : V₁ →+ V₂) {C : } (h : ∀ (x : V₁), f x C * x) :

                Alias of NormedAddGroupHom.mkNormedAddGroupHom_norm_le'.


                If a bounded group homomorphism map is constructed from a group homomorphism via the constructor AddMonoidHom.mkNormedAddGroupHom, then its norm is bounded by the bound given to the constructor or zero if this bound is negative.

                Addition of normed group homs #

                instance NormedAddGroupHom.add {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :

                Addition of normed group homs.

                Equations
                • One or more equations did not get rendered due to their size.
                theorem NormedAddGroupHom.opNorm_add_le {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₁ V₂) :

                The operator norm satisfies the triangle inequality.

                @[simp]
                theorem NormedAddGroupHom.coe_add {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₁ V₂) :
                (f + g) = f + g
                @[simp]
                theorem NormedAddGroupHom.add_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₁ V₂) (v : V₁) :
                (f + g) v = f v + g v

                The zero normed group hom #

                instance NormedAddGroupHom.zero {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
                Equations
                Equations
                • NormedAddGroupHom.inhabited = { default := 0 }

                The norm of the 0 operator is 0.

                theorem NormedAddGroupHom.opNorm_zero_iff {V₁ : Type u_5} {V₂ : Type u_6} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} :
                f = 0 f = 0

                For normed groups, an operator is zero iff its norm vanishes.

                @[simp]
                theorem NormedAddGroupHom.coe_zero {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
                0 = 0
                @[simp]
                theorem NormedAddGroupHom.zero_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (v : V₁) :
                0 v = 0

                The identity normed group hom #

                @[simp]

                The identity as a continuous normed group hom.

                Equations
                Instances For

                  The norm of the identity is at most 1. It is in fact 1, except when the norm of every element vanishes, where it is 0. (Since we are working with seminorms this can happen even if the space is non-trivial.) It means that one can not do better than an inequality in general.

                  If there is an element with norm different from 0, then the norm of the identity equals 1. (Since we are working with seminorms supposing that the space is non-trivial is not enough.)

                  If a normed space is non-trivial, then the norm of the identity equals 1.

                  The negation of a normed group hom #

                  instance NormedAddGroupHom.neg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :

                  Opposite of a normed group hom.

                  Equations
                  @[simp]
                  theorem NormedAddGroupHom.coe_neg {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :
                  (-f) = -f
                  @[simp]
                  theorem NormedAddGroupHom.neg_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₁) :
                  (-f) v = -f v

                  Subtraction of normed group homs #

                  instance NormedAddGroupHom.sub {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :

                  Subtraction of normed group homs.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[simp]
                  theorem NormedAddGroupHom.coe_sub {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₁ V₂) :
                  (f - g) = f - g
                  @[simp]
                  theorem NormedAddGroupHom.sub_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₁ V₂) (v : V₁) :
                  (f - g) v = f v - g v

                  Scalar actions on normed group homs #

                  instance NormedAddGroupHom.smul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [BoundedSMul R V₂] :
                  SMul R (NormedAddGroupHom V₁ V₂)
                  Equations
                  • NormedAddGroupHom.smul = { smul := fun (r : R) (f : NormedAddGroupHom V₁ V₂) => { toFun := r f, map_add' := , bound' := } }
                  @[simp]
                  theorem NormedAddGroupHom.coe_smul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [BoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂) :
                  (r f) = r f
                  @[simp]
                  theorem NormedAddGroupHom.smul_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [BoundedSMul R V₂] (r : R) (f : NormedAddGroupHom V₁ V₂) (v : V₁) :
                  (r f) v = r f v
                  instance NormedAddGroupHom.smulCommClass {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} {R' : Type u_6} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [BoundedSMul R V₂] [MonoidWithZero R'] [DistribMulAction R' V₂] [PseudoMetricSpace R'] [BoundedSMul R' V₂] [SMulCommClass R R' V₂] :
                  Equations
                  • =
                  instance NormedAddGroupHom.isScalarTower {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} {R' : Type u_6} [MonoidWithZero R] [DistribMulAction R V₂] [PseudoMetricSpace R] [BoundedSMul R V₂] [MonoidWithZero R'] [DistribMulAction R' V₂] [PseudoMetricSpace R'] [BoundedSMul R' V₂] [SMul R R'] [IsScalarTower R R' V₂] :
                  Equations
                  • =
                  instance NormedAddGroupHom.nsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
                  Equations
                  • NormedAddGroupHom.nsmul = { smul := fun (n : ) (f : NormedAddGroupHom V₁ V₂) => { toFun := n f, map_add' := , bound' := } }
                  @[simp]
                  theorem NormedAddGroupHom.coe_nsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : ) (f : NormedAddGroupHom V₁ V₂) :
                  (r f) = r f
                  @[simp]
                  theorem NormedAddGroupHom.nsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : ) (f : NormedAddGroupHom V₁ V₂) (v : V₁) :
                  (r f) v = r f v
                  instance NormedAddGroupHom.zsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
                  Equations
                  • NormedAddGroupHom.zsmul = { smul := fun (z : ) (f : NormedAddGroupHom V₁ V₂) => { toFun := z f, map_add' := , bound' := } }
                  @[simp]
                  theorem NormedAddGroupHom.coe_zsmul {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : ) (f : NormedAddGroupHom V₁ V₂) :
                  (r f) = r f
                  @[simp]
                  theorem NormedAddGroupHom.zsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (r : ) (f : NormedAddGroupHom V₁ V₂) (v : V₁) :
                  (r f) v = r f v

                  Normed group structure on normed group homs #

                  Homs between two given normed groups form a commutative additive group.

                  Equations

                  Normed group homomorphisms themselves form a seminormed group with respect to the operator norm.

                  Equations

                  Normed group homomorphisms themselves form a normed group with respect to the operator norm.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[simp]
                  theorem NormedAddGroupHom.coeAddHom_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
                  ∀ (a : NormedAddGroupHom V₁ V₂) (a_1 : V₁), NormedAddGroupHom.coeAddHom a a_1 = a a_1
                  def NormedAddGroupHom.coeAddHom {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] :
                  NormedAddGroupHom V₁ V₂ →+ V₁V₂

                  Coercion of a NormedAddGroupHom is an AddMonoidHom. Similar to AddMonoidHom.coeFn.

                  Equations
                  • NormedAddGroupHom.coeAddHom = { toZeroHom := { toFun := DFunLike.coe, map_zero' := }, map_add' := }
                  Instances For
                    @[simp]
                    theorem NormedAddGroupHom.coe_sum {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {ι : Type u_5} (s : Finset ι) (f : ιNormedAddGroupHom V₁ V₂) :
                    (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => (f i)
                    theorem NormedAddGroupHom.sum_apply {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {ι : Type u_5} (s : Finset ι) (f : ιNormedAddGroupHom V₁ V₂) (v : V₁) :
                    (Finset.sum s fun (i : ι) => f i) v = Finset.sum s fun (i : ι) => (f i) v

                    Module structure on normed group homs #

                    Equations
                    instance NormedAddGroupHom.module {V₁ : Type u_2} {V₂ : Type u_3} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {R : Type u_5} [Semiring R] [Module R V₂] [PseudoMetricSpace R] [BoundedSMul R V₂] :
                    Equations

                    Composition of normed group homs #

                    @[simp]
                    theorem NormedAddGroupHom.comp_apply {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁ V₂) :
                    ∀ (a : V₁), (NormedAddGroupHom.comp g f) a = g (f a)
                    def NormedAddGroupHom.comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁ V₂) :

                    The composition of continuous normed group homs.

                    Equations
                    Instances For
                      theorem NormedAddGroupHom.norm_comp_le_of_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₂ V₃} {C₁ : } {C₂ : } (hg : g C₂) (hf : f C₁) :
                      theorem NormedAddGroupHom.norm_comp_le_of_le' {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {f : NormedAddGroupHom V₁ V₂} {g : NormedAddGroupHom V₂ V₃} (C₁ : ) (C₂ : ) (C₃ : ) (h : C₃ = C₂ * C₁) (hg : g C₂) (hf : f C₁) :

                      Composition of normed groups hom as an additive group morphism.

                      Equations
                      Instances For
                        @[simp]
                        theorem NormedAddGroupHom.comp_zero {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₂ V₃) :
                        @[simp]
                        theorem NormedAddGroupHom.zero_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) :
                        theorem NormedAddGroupHom.coe_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) :
                        (NormedAddGroupHom.comp g f) = g f
                        @[simp]
                        theorem NormedAddGroupHom.incl_apply {V : Type u_1} [SeminormedAddCommGroup V] (s : AddSubgroup V) (self : s) :
                        (NormedAddGroupHom.incl s) self = self

                        The inclusion of an AddSubgroup, as bounded group homomorphism.

                        Equations
                        Instances For

                          Kernel #

                          def NormedAddGroupHom.ker {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :

                          The kernel of a bounded group homomorphism. Naturally endowed with a SeminormedAddCommGroup instance.

                          Equations
                          Instances For
                            theorem NormedAddGroupHom.mem_ker {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₁) :
                            @[simp]
                            theorem NormedAddGroupHom.ker.lift_apply_coe {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) (h : NormedAddGroupHom.comp g f = 0) (v : V₁) :
                            ((NormedAddGroupHom.ker.lift f g h) v) = f v
                            def NormedAddGroupHom.ker.lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) (h : NormedAddGroupHom.comp g f = 0) :

                            Given a normed group hom f : V₁ → V₂ satisfying g.comp f = 0 for some g : V₂ → V₃, the corestriction of f to the kernel of g.

                            Equations
                            Instances For
                              theorem NormedAddGroupHom.coe_ker {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :

                              Range #

                              def NormedAddGroupHom.range {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) :

                              The image of a bounded group homomorphism. Naturally endowed with a SeminormedAddCommGroup instance.

                              Equations
                              Instances For
                                theorem NormedAddGroupHom.mem_range {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₂) :
                                v NormedAddGroupHom.range f ∃ (w : V₁), f w = v
                                @[simp]
                                theorem NormedAddGroupHom.mem_range_self {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] (f : NormedAddGroupHom V₁ V₂) (v : V₁) :

                                A NormedAddGroupHom is norm-nonincreasing if ‖f v‖ ≤ ‖v‖ for all v.

                                Equations
                                Instances For
                                  theorem NormedAddGroupHom.isometry_comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {g : NormedAddGroupHom V₂ V₃} {f : NormedAddGroupHom V₁ V₂} (hg : Isometry g) (hf : Isometry f) :

                                  The equalizer of two morphisms f g : NormedAddGroupHom V W.

                                  Equations
                                  Instances For

                                    If φ : NormedAddGroupHom V₁ V is such that f.comp φ = g.comp φ, the induced morphism NormedAddGroupHom V₁ (f.equalizer g).

                                    Equations
                                    Instances For
                                      @[simp]
                                      @[simp]
                                      theorem NormedAddGroupHom.Equalizer.liftEquiv_apply {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] [SeminormedAddCommGroup V₁] {f : NormedAddGroupHom V W} {g : NormedAddGroupHom V W} (φ : { φ : NormedAddGroupHom V₁ V // NormedAddGroupHom.comp f φ = NormedAddGroupHom.comp g φ }) :
                                      NormedAddGroupHom.Equalizer.liftEquiv φ = NormedAddGroupHom.Equalizer.lift φ

                                      The lifting property of the equalizer as an equivalence.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def NormedAddGroupHom.Equalizer.map {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {W₁ : Type u_6} {W₂ : Type u_7} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] {f₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {g₂ : NormedAddGroupHom V₂ W₂} (φ : NormedAddGroupHom V₁ V₂) (ψ : NormedAddGroupHom W₁ W₂) (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ) :

                                        Given φ : NormedAddGroupHom V₁ V₂ and ψ : NormedAddGroupHom W₁ W₂ such that ψ.comp f₁ = f₂.comp φ and ψ.comp g₁ = g₂.comp φ, the induced morphism NormedAddGroupHom (f₁.equalizer g₁) (f₂.equalizer g₂).

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem NormedAddGroupHom.Equalizer.comm_sq₂ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] [SeminormedAddCommGroup W₃] {f₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {f₃ : NormedAddGroupHom V₃ W₃} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} {φ' : NormedAddGroupHom V₂ V₃} {ψ' : NormedAddGroupHom W₂ W₃} (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hf' : NormedAddGroupHom.comp ψ' f₂ = NormedAddGroupHom.comp f₃ φ') :
                                          theorem NormedAddGroupHom.Equalizer.map_comp_map {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] [SeminormedAddCommGroup W₃] {f₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {g₂ : NormedAddGroupHom V₂ W₂} {f₃ : NormedAddGroupHom V₃ W₃} {g₃ : NormedAddGroupHom V₃ W₃} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} {φ' : NormedAddGroupHom V₂ V₃} {ψ' : NormedAddGroupHom W₂ W₃} (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ) (hf' : NormedAddGroupHom.comp ψ' f₂ = NormedAddGroupHom.comp f₃ φ') (hg' : NormedAddGroupHom.comp ψ' g₂ = NormedAddGroupHom.comp g₃ φ') :

                                          If φ satisfies ‖φ‖ ≤ C, then the same is true for the lifted morphism.

                                          theorem NormedAddGroupHom.Equalizer.map_normNoninc {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {W₁ : Type u_6} {W₂ : Type u_7} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] {f₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ) (hφ : NormedAddGroupHom.NormNoninc φ) :
                                          theorem NormedAddGroupHom.Equalizer.norm_map_le {V₁ : Type u_3} {V₂ : Type u_4} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] {W₁ : Type u_6} {W₂ : Type u_7} [SeminormedAddCommGroup W₁] [SeminormedAddCommGroup W₂] {f₁ : NormedAddGroupHom V₁ W₁} {g₁ : NormedAddGroupHom V₁ W₁} {f₂ : NormedAddGroupHom V₂ W₂} {g₂ : NormedAddGroupHom V₂ W₂} {φ : NormedAddGroupHom V₁ V₂} {ψ : NormedAddGroupHom W₁ W₂} (hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ) (hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ) (C : ) (hφ : NormedAddGroupHom.comp φ (NormedAddGroupHom.Equalizer.ι f₁ g₁) C) :