mathlib documentation

analysis.normed_space.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.

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 semi_normed_group_hom and we specialize to normed_group_hom when needed.

source
structure normed_group_hom (V : Type u_1) (W : Type u_2) [semi_normed_group V] [semi_normed_group W] :
Type (max u_1 u_2)

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

source
def add_monoid_hom.mk_normed_group_hom {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] (f : V →+ W) (C : ℝ) (h : ∀ (v : V), ∥⇑f v∥ ≤ C * ∥v∥) :
normed_group_hom V W

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

See add_monoid_hom.mk_normed_group_hom' for a version that uses ℝ≥0 for the bound.

Equations
source
def add_monoid_hom.mk_normed_group_hom' {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] (f : V →+ W) (C : ℝ≥0) (hC : ∀ (x : V), nnnorm (⇑f x) ≤ C * nnnorm x) :
normed_group_hom V W

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

See add_monoid_hom.mk_normed_group_hom for a version that uses ℝ for the bound.

Equations
source
theorem exists_pos_bound_of_bound {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] {f : V → W} (M : ℝ) (h : ∀ (x : V), ∥f x∥ ≤ M * ∥x∥) :
∃ (N : ℝ), 0 < N ∧ ∀ (x : V), ∥f x∥ ≤ N * ∥x∥
source
@[protected, instance]
def normed_group_hom.has_coe_to_fun {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
has_coe_to_fun (normed_group_hom V₁ V₂)
Equations
source
theorem normed_group_hom.coe_inj {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {f g : normed_group_hom V₁ V₂} (H : ⇑f = ⇑g) :
f = g
source
theorem normed_group_hom.coe_injective {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
function.injective coe_fn
source
theorem normed_group_hom.coe_inj_iff {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {f g : normed_group_hom V₁ V₂} :
f = g ↔ ⇑f = ⇑g
source
@[ext]
theorem normed_group_hom.ext {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {f g : normed_group_hom V₁ V₂} (H : ∀ (x : V₁), ⇑f x = ⇑g x) :
f = g
source
theorem normed_group_hom.ext_iff {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {f g : normed_group_hom V₁ V₂} :
f = g ↔ ∀ (x : V₁), ⇑f x = ⇑g x
source
@[simp]
theorem normed_group_hom.to_fun_eq_coe {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
f.to_fun = ⇑f
source
@[simp]
theorem normed_group_hom.coe_mk {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ → V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ℝ) (h₃ : ∀ (v : V₁), ∥f v∥ ≤ h₂ * ∥v∥) :
⇑{to_fun := f, map_add' := h₁, bound' := _} = f
source
@[simp]
theorem normed_group_hom.coe_mk_normed_group_hom {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ →+ V₂) (C : ℝ) (hC : ∀ (v : V₁), ∥⇑f v∥ ≤ C * ∥v∥) :
⇑(f.mk_normed_group_hom C hC) = ⇑f
source
@[simp]
theorem normed_group_hom.coe_mk_normed_group_hom' {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ →+ V₂) (C : ℝ≥0) (hC : ∀ (x : V₁), nnnorm (⇑f x) ≤ C * nnnorm x) :
⇑(f.mk_normed_group_hom' C hC) = ⇑f
source
def normed_group_hom.to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
V₁ →+ V₂

The group homomorphism underlying a bounded group homomorphism.

Equations
source
@[simp]
theorem normed_group_hom.coe_to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
⇑(f.to_add_monoid_hom) = ⇑f
source
theorem normed_group_hom.to_add_monoid_hom_injective {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
function.injective normed_group_hom.to_add_monoid_hom
source
@[simp]
theorem normed_group_hom.mk_to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ → V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ∃ (C : ℝ), ∀ (v : V₁), ∥f v∥ ≤ C * ∥v∥) :
{to_fun := f, map_add' := h₁, bound' := h₂}.to_add_monoid_hom = add_monoid_hom.mk' f h₁
source
@[simp]
theorem normed_group_hom.map_zero {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
⇑f 0 = 0
source
@[simp]
theorem normed_group_hom.map_add {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (x y : V₁) :
⇑f (x + y) = ⇑f x + ⇑f y
source
@[simp]
theorem normed_group_hom.map_sum {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) {ι : Type u_1} (v : ι → V₁) (s : finset ι) :
⇑f (∑ (i : ι) in s, v i) = ∑ (i : ι) in s, ⇑f (v i)
source
@[simp]
theorem normed_group_hom.map_sub {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (x y : V₁) :
⇑f (x - y) = ⇑f x - ⇑f y
source
@[simp]
theorem normed_group_hom.map_neg {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (x : V₁) :
⇑f (-x) = -⇑f x
source
def normed_group_hom.bound_by {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (C : ℝ≥0) :
Prop

Predicate asserting a norm bound on a normed group hom.

Equations
source
theorem normed_group_hom.mk_normed_group_hom'_bound_by {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ →+ V₂) (C : ℝ≥0) (hC : ∀ (x : V₁), nnnorm (⇑f x) ≤ C * nnnorm x) :
(f.mk_normed_group_hom' C hC).bound_by C
source
theorem normed_group_hom.bound {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
∃ (C : ℝ≥0), 0 < C ∧ f.bound_by C
source
theorem normed_group_hom.lipschitz_of_bound_by {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (C : ℝ≥0) (h : f.bound_by C) :
lipschitz_with (nnreal.of_real ↑C) ⇑f
source
theorem normed_group_hom.antilipschitz_of_bound_by {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) {K : ℝ≥0} (h : ∀ (x : V₁), ∥x∥ ≤ (↑K) * ∥⇑f x∥) :
antilipschitz_with K ⇑f
source
@[protected]
theorem normed_group_hom.uniform_continuous {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
uniform_continuous ⇑f
source
@[protected, continuity]
theorem normed_group_hom.continuous {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
continuous ⇑f

The operator norm #

source
def normed_group_hom.op_norm {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
ℝ

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

Equations
source
@[protected, instance]
def normed_group_hom.has_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
has_norm (normed_group_hom V₁ V₂)
Equations
source
theorem normed_group_hom.norm_def {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
∥f∥ = Inf {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ∥⇑f x∥ ≤ c * ∥x∥}
source
theorem normed_group_hom.bounds_nonempty {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {f : normed_group_hom V₁ V₂} :
∃ (c : ℝ), c ∈ {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ∥⇑f x∥ ≤ c * ∥x∥}
source
theorem normed_group_hom.bounds_bdd_below {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {f : normed_group_hom V₁ V₂} :
bdd_below {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ∥⇑f x∥ ≤ c * ∥x∥}
source
theorem normed_group_hom.op_norm_nonneg {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
0 ≤ ∥f∥
source
theorem normed_group_hom.le_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (x : V₁) :
∥⇑f x∥ ≤ ∥f∥ * ∥x∥

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

source
theorem normed_group_hom.le_op_norm_of_le {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) {c : ℝ} {x : V₁} (h : ∥x∥ ≤ c) :
∥⇑f x∥ ≤ ∥f∥ * c
source
theorem normed_group_hom.le_of_op_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) {c : ℝ} (h : ∥f∥ ≤ c) (x : V₁) :
∥⇑f x∥ ≤ c * ∥x∥
source
theorem normed_group_hom.lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
lipschitz_with ⟨∥f∥, _⟩ ⇑f

continuous linear maps are Lipschitz continuous.

source
theorem normed_group_hom.ratio_le_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (x : V₁) :
∥⇑f x∥ / ∥x∥ ≤ ∥f∥
source
theorem normed_group_hom.op_norm_le_bound {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : V₁), ∥⇑f x∥ ≤ M * ∥x∥) :
∥f∥ ≤ M

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

source
theorem normed_group_hom.op_norm_le_of_lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {f : normed_group_hom V₁ V₂} {K : ℝ≥0} (hf : lipschitz_with K ⇑f) :
∥f∥ ≤ ↑K
source
theorem normed_group_hom.mk_normed_group_hom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ →+ V₂) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : V₁), ∥⇑f x∥ ≤ C * ∥x∥) :
∥f.mk_normed_group_hom C h∥ ≤ C

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

source
theorem normed_group_hom.mk_normed_group_hom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ →+ V₂) {C : ℝ} (h : ∀ (x : V₁), ∥⇑f x∥ ≤ C * ∥x∥) :
∥f.mk_normed_group_hom C h∥ ≤ max C 0

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

source
theorem add_monoid_hom.mk_normed_group_hom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ →+ V₂) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : V₁), ∥⇑f x∥ ≤ C * ∥x∥) :
∥f.mk_normed_group_hom C h∥ ≤ C

Alias of mk_normed_group_hom_norm_le.

source
theorem add_monoid_hom.mk_normed_group_hom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : V₁ →+ V₂) {C : ℝ} (h : ∀ (x : V₁), ∥⇑f x∥ ≤ C * ∥x∥) :
∥f.mk_normed_group_hom C h∥ ≤ max C 0

Alias of mk_normed_group_hom_norm_le'.

Addition of normed group homs #

source
@[protected, instance]
def normed_group_hom.has_add {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
has_add (normed_group_hom V₁ V₂)

Addition of normed group homs.

Equations
source
theorem normed_group_hom.op_norm_add_le {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f g : normed_group_hom V₁ V₂) :
∥f + g∥ ≤ ∥f∥ + ∥g∥

The operator norm satisfies the triangle inequality.

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

The zero normed group hom #

source
@[protected, instance]
def normed_group_hom.has_zero {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
has_zero (normed_group_hom V₁ V₂)
Equations
source
@[protected, instance]
def normed_group_hom.inhabited {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
inhabited (normed_group_hom V₁ V₂)
Equations
source
theorem normed_group_hom.op_norm_zero {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
∥0∥ = 0

The norm of the 0 operator is 0.

source
theorem normed_group_hom.op_norm_zero_iff {V₁ : Type u_1} {V₂ : Type u_2} [normed_group V₁] [normed_group V₂] {f : normed_group_hom V₁ V₂} :
∥f∥ = 0 ↔ f = 0

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

source
@[simp]
theorem normed_group_hom.coe_zero {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
⇑0 = 0
source
@[simp]
theorem normed_group_hom.zero_apply {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (v : V₁) :
⇑0 v = 0

The identity normed group hom #

source
@[simp]
theorem normed_group_hom.id_apply {V : Type u_1} [semi_normed_group V] (ᾰ : V) :
⇑normed_group_hom.id ᾰ = ᾰ
source
def normed_group_hom.id {V : Type u_1} [semi_normed_group V] :
normed_group_hom V V

The identity as a continuous normed group hom.

Equations
source
theorem normed_group_hom.norm_id_le {V : Type u_1} [semi_normed_group V] :
∥normed_group_hom.id∥ ≤ 1

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.

source
theorem normed_group_hom.norm_id_of_nontrivial_seminorm {V : Type u_1} [semi_normed_group V] (h : ∃ (x : V), ∥x∥ ≠ 0) :
∥normed_group_hom.id∥ = 1

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.)

source
theorem normed_group_hom.norm_id {V : Type u_1} [normed_group V] [nontrivial V] :
∥normed_group_hom.id∥ = 1

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

The negation of a normed group hom #

source
@[protected, instance]
def normed_group_hom.has_neg {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
has_neg (normed_group_hom V₁ V₂)

Opposite of a normed group hom.

Equations
source
@[simp]
theorem normed_group_hom.coe_neg {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
⇑-f = -⇑f
source
@[simp]
theorem normed_group_hom.neg_apply {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (v : V₁) :
(⇑-f) v = -⇑f v
source
theorem normed_group_hom.op_norm_neg {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
∥-f∥ = ∥f∥

Subtraction of normed group homs #

source
@[protected, instance]
def normed_group_hom.has_sub {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
has_sub (normed_group_hom V₁ V₂)

Subtraction of normed group homs.

Equations
source
@[simp]
theorem normed_group_hom.coe_sub {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f g : normed_group_hom V₁ V₂) :
⇑(f - g) = ⇑f - ⇑g
source
@[simp]
theorem normed_group_hom.sub_apply {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (f g : normed_group_hom V₁ V₂) (v : V₁) :
⇑(f - g) v = ⇑f v - ⇑g v

Normed group structure on normed group homs #

source
@[protected, instance]
def normed_group_hom.add_comm_group {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
add_comm_group (normed_group_hom V₁ V₂)

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

Equations
source
@[protected, instance]
def normed_group_hom.to_semi_normed_group {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
semi_normed_group (normed_group_hom V₁ V₂)

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

Equations
source
@[protected, instance]
def normed_group_hom.to_normed_group {V₁ : Type u_1} {V₂ : Type u_2} [normed_group V₁] [normed_group V₂] :
normed_group (normed_group_hom V₁ V₂)

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

Equations
source
@[simp]
theorem normed_group_hom.coe_fn_add_hom_apply {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] (x : normed_group_hom V₁ V₂) (ᾰ : V₁) :
⇑normed_group_hom.coe_fn_add_hom x ᾰ = ⇑x ᾰ
source
def normed_group_hom.coe_fn_add_hom {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] :
normed_group_hom V₁ V₂ →+ V₁ → V₂

Coercion of a normed_group_hom is an add_monoid_hom. Similar to add_monoid_hom.coe_fn

Equations
source
@[simp]
theorem normed_group_hom.coe_sum {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {ι : Type u_1} (s : finset ι) (f : ι → normed_group_hom V₁ V₂) :
⇑∑ (i : ι) in s, f i = ∑ (i : ι) in s, ⇑(f i)
source
theorem normed_group_hom.sum_apply {V₁ : Type u_2} {V₂ : Type u_3} [semi_normed_group V₁] [semi_normed_group V₂] {ι : Type u_1} (s : finset ι) (f : ι → normed_group_hom V₁ V₂) (v : V₁) :
(⇑∑ (i : ι) in s, f i) v = ∑ (i : ι) in s, ⇑(f i) v

Composition of normed group homs #

source
@[simp]
theorem normed_group_hom.comp_apply {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] (g : normed_group_hom V₂ V₃) (f : normed_group_hom V₁ V₂) (ᾰ : V₁) :
⇑(g.comp f) ᾰ = ⇑g (⇑f ᾰ)
source
@[protected]
def normed_group_hom.comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] (g : normed_group_hom V₂ V₃) (f : normed_group_hom V₁ V₂) :
normed_group_hom V₁ V₃

The composition of continuous normed group homs.

Equations
source
theorem normed_group_hom.norm_comp_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] (g : normed_group_hom V₂ V₃) (f : normed_group_hom V₁ V₂) :
∥g.comp f∥ ≤ ∥g∥ * ∥f∥
source
def normed_group_hom.comp_hom {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] :
normed_group_hom V₂ V₃ →+ normed_group_hom V₁ V₂ →+ normed_group_hom V₁ V₃

Composition of normed groups hom as an additive group morphism.

Equations
source
@[simp]
theorem normed_group_hom.comp_zero {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] (f : normed_group_hom V₂ V₃) :
f.comp 0 = 0
source
@[simp]
theorem normed_group_hom.zero_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] (f : normed_group_hom V₁ V₂) :
0.comp f = 0
source
def normed_group_hom.incl {V : Type u_1} [semi_normed_group V] (s : add_subgroup V) :
normed_group_hom ↥s V

The inclusion of an add_subgroup, as bounded group homomorphism.

Equations
source
@[simp]
theorem normed_group_hom.incl_apply {V : Type u_1} [semi_normed_group V] (s : add_subgroup V) (ᾰ : ↥s) :
⇑(normed_group_hom.incl s) ᾰ = ↑ᾰ

Kernel #

source
def normed_group_hom.ker {V₁ : Type u_3} {V₂ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
add_subgroup V₁

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

Equations
source
theorem normed_group_hom.mem_ker {V₁ : Type u_3} {V₂ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (v : V₁) :
v ∈ f.ker ↔ ⇑f v = 0
source
@[simp]
theorem normed_group_hom.ker.lift_apply_coe {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] (f : normed_group_hom V₁ V₂) (g : normed_group_hom V₂ V₃) (h : g.comp f = 0) (v : V₁) :
↑(⇑(normed_group_hom.ker.lift f g h) v) = ⇑f v
source
def normed_group_hom.ker.lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] (f : normed_group_hom V₁ V₂) (g : normed_group_hom V₂ V₃) (h : g.comp f = 0) :
normed_group_hom V₁ ↥(g.ker)

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
source
@[simp]
theorem normed_group_hom.ker.incl_comp_lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] (f : normed_group_hom V₁ V₂) (g : normed_group_hom V₂ V₃) (h : g.comp f = 0) :
(normed_group_hom.incl g.ker).comp (normed_group_hom.ker.lift f g h) = f
source
@[simp]
theorem normed_group_hom.ker_zero {V₁ : Type u_3} {V₂ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] :
0.ker = ⊤
source
theorem normed_group_hom.coe_ker {V₁ : Type u_3} {V₂ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
↑(f.ker) = ⇑f ⁻¹' {0}
source
theorem normed_group_hom.is_closed_ker {V₁ : Type u_3} [semi_normed_group V₁] {V₂ : Type u_1} [normed_group V₂] (f : normed_group_hom V₁ V₂) :
is_closed ↑(f.ker)

Range #

source
def normed_group_hom.range {V₁ : Type u_3} {V₂ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) :
add_subgroup V₂

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

Equations
source
theorem normed_group_hom.mem_range {V₁ : Type u_3} {V₂ : Type u_4} [semi_normed_group V₁] [semi_normed_group V₂] (f : normed_group_hom V₁ V₂) (v : V₂) :
v ∈ f.range ↔ ∃ (w : V₁), ⇑f w = v
source
def normed_group_hom.norm_noninc {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] (f : normed_group_hom V W) :
Prop

A normed_group_hom is norm-nonincreasing if ∥f v∥ ≤ ∥v∥ for all v.

Equations
source
theorem normed_group_hom.norm_noninc.bound_by_one {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] {f : normed_group_hom V W} (hf : f.norm_noninc) :
f.bound_by 1
source
theorem normed_group_hom.norm_noninc.id {V : Type u_1} [semi_normed_group V] :
normed_group_hom.id.norm_noninc
source
theorem normed_group_hom.norm_noninc.comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] {g : normed_group_hom V₂ V₃} {f : normed_group_hom V₁ V₂} (hg : g.norm_noninc) (hf : f.norm_noninc) :
(g.comp f).norm_noninc
source
theorem normed_group_hom.isometry_iff_norm {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] (f : normed_group_hom V W) :
isometry ⇑f ↔ ∀ (v : V), ∥⇑f v∥ = ∥v∥
source
theorem normed_group_hom.isometry_of_norm {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] (f : normed_group_hom V W) (hf : ∀ (v : V), ∥⇑f v∥ = ∥v∥) :
isometry ⇑f
source
theorem normed_group_hom.norm_eq_of_isometry {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] {f : normed_group_hom V W} (hf : isometry ⇑f) (v : V) :
∥⇑f v∥ = ∥v∥
source
theorem normed_group_hom.isometry_id {V : Type u_1} [semi_normed_group V] :
isometry ⇑normed_group_hom.id
source
theorem normed_group_hom.isometry_comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [semi_normed_group V₁] [semi_normed_group V₂] [semi_normed_group V₃] {g : normed_group_hom V₂ V₃} {f : normed_group_hom V₁ V₂} (hg : isometry ⇑g) (hf : isometry ⇑f) :
isometry ⇑(g.comp f)
source
theorem normed_group_hom.norm_noninc_of_isometry {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] {f : normed_group_hom V W} (hf : isometry ⇑f) :
f.norm_noninc
source
theorem normed_group_hom.bound_by_one_of_isometry {V : Type u_1} {W : Type u_2} [semi_normed_group V] [semi_normed_group W] {f : normed_group_hom V W} (hf : isometry ⇑f) :
f.bound_by 1