mathlib documentation

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 seminormed_add_group_hom and we specialize to normed_add_group_hom when needed.

def add_monoid_hom.mk_normed_add_group_hom {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group 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 add_monoid_hom.mk_normed_add_group_hom' for a version that uses ℝ≥0 for the bound.

Equations
def add_monoid_hom.mk_normed_add_group_hom' {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group 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 add_monoid_hom.mk_normed_add_group_hom for a version that uses for the bound.

Equations
theorem exists_pos_bound_of_bound {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] {f : V → W} (M : ) (h : ∀ (x : V), f x M * x) :
∃ (N : ), 0 < N ∀ (x : V), f x N * x
@[protected, instance]
def normed_add_group_hom.has_coe_to_fun {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :
has_coe_to_fun (normed_add_group_hom V₁ V₂) (λ (_x : normed_add_group_hom V₁ V₂), V₁ → V₂)
Equations
theorem normed_add_group_hom.coe_inj {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f g : normed_add_group_hom V₁ V₂} (H : f = g) :
f = g
theorem normed_add_group_hom.coe_inj_iff {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f g : normed_add_group_hom V₁ V₂} :
f = g f = g
@[ext]
theorem normed_add_group_hom.ext {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f g : normed_add_group_hom V₁ V₂} (H : ∀ (x : V₁), f x = g x) :
f = g
theorem normed_add_group_hom.ext_iff {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f g : normed_add_group_hom V₁ V₂} :
f = g ∀ (x : V₁), f x = g x
@[simp]
theorem normed_add_group_hom.to_fun_eq_coe {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :
@[simp]
theorem normed_add_group_hom.coe_mk {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_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
@[simp]
theorem normed_add_group_hom.coe_mk_normed_add_group_hom {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ →+ V₂) (C : ) (hC : ∀ (v : V₁), f v C * v) :
@[simp]
theorem normed_add_group_hom.coe_mk_normed_add_group_hom' {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ →+ V₂) (C : nnreal) (hC : ∀ (x : V₁), f x∥₊ C * x∥₊) :
def normed_add_group_hom.to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :
V₁ →+ V₂

The group homomorphism underlying a bounded group homomorphism.

Equations
@[simp]
@[simp]
theorem normed_add_group_hom.mk_to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ → V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ∃ (C : ), ∀ (v : V₁), f v C * v) :
theorem normed_add_group_hom.bound {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :
∃ (C : ), 0 < C ∀ (x : V₁), f x C * x
theorem normed_add_group_hom.antilipschitz_of_norm_ge {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {K : nnreal} (h : ∀ (x : V₁), x K * f x) :
def normed_add_group_hom.surjective_on_with {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (K : add_subgroup V₂) (C : ) :
Prop

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
theorem normed_add_group_hom.surjective_on_with.mono {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} {K : add_subgroup V₂} {C C' : } (h : f.surjective_on_with K C) (H : C C') :
theorem normed_add_group_hom.surjective_on_with.exists_pos {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} {K : add_subgroup V₂} {C : } (h : f.surjective_on_with K C) :
∃ (C' : ) (H : C' > 0), f.surjective_on_with K C'
theorem normed_add_group_hom.surjective_on_with.surj_on {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} {K : add_subgroup V₂} {C : } (h : f.surjective_on_with K C) :

The operator norm #

noncomputable def normed_add_group_hom.op_norm {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

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

Equations
@[protected, instance]
noncomputable def normed_add_group_hom.has_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :
Equations
theorem normed_add_group_hom.norm_def {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :
f = has_Inf.Inf {c : | 0 c ∀ (x : V₁), f x c * x}
theorem normed_add_group_hom.bounds_nonempty {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} :
∃ (c : ), c {c : | 0 c ∀ (x : V₁), f x c * x}
theorem normed_add_group_hom.bounds_bdd_below {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} :
bdd_below {c : | 0 c ∀ (x : V₁), f x c * x}
theorem normed_add_group_hom.op_norm_nonneg {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :
theorem normed_add_group_hom.le_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (x : V₁) :

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

theorem normed_add_group_hom.le_op_norm_of_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {c : } {x : V₁} (h : x c) :
theorem normed_add_group_hom.le_of_op_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {c : } (h : f c) (x : V₁) :
theorem normed_add_group_hom.lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

continuous linear maps are Lipschitz continuous.

@[protected]
@[protected, continuity]
theorem normed_add_group_hom.continuous {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :
theorem normed_add_group_hom.ratio_le_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (x : V₁) :
theorem normed_add_group_hom.op_norm_le_bound {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom 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 normed_add_group_hom.op_norm_eq_of_bounds {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {M : } (M_nonneg : 0 M) (h_above : ∀ (x : V₁), f x M * x) (h_below : ∀ (N : ), N 0(∀ (x : V₁), f x N * x)M N) :
theorem normed_add_group_hom.op_norm_le_of_lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} {K : nnreal} (hf : lipschitz_with K f) :
theorem normed_add_group_hom.mk_normed_add_group_hom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group 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 mk_normed_add_group_hom, then its norm is bounded by the bound given to the constructor if it is nonnegative.

theorem normed_add_group_hom.mk_normed_add_group_hom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group 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 mk_normed_add_group_hom, then its norm is bounded by the bound given to the constructor or zero if this bound is negative.

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

Alias of normed_add_group_hom.mk_normed_add_group_hom_norm_le.

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

Alias of normed_add_group_hom.mk_normed_add_group_hom_norm_le'.

Addition of normed group homs #

@[protected, instance]
noncomputable def normed_add_group_hom.has_add {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

Addition of normed group homs.

Equations
theorem normed_add_group_hom.op_norm_add_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f g : normed_add_group_hom V₁ V₂) :

The operator norm satisfies the triangle inequality.

Terms containing @has_add.add (has_coe_to_fun.F ...) pi.has_add seem to cause leanchecker to crash due to an out-of-memory condition. As a workaround, we add a type annotation: (f + g : V₁ → V₂)

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

The zero normed group hom #

@[protected, instance]
def normed_add_group_hom.has_zero {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :
Equations
@[protected, instance]
def normed_add_group_hom.inhabited {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :
Equations
theorem normed_add_group_hom.op_norm_zero {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

The norm of the 0 operator is 0.

theorem normed_add_group_hom.op_norm_zero_iff {V₁ : Type u_1} {V₂ : Type u_2} [normed_add_comm_group V₁] [normed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} :
f = 0 f = 0

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

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

The identity normed group hom #

@[simp]
theorem normed_add_group_hom.id_apply (V : Type u_1) [seminormed_add_comm_group V] (ᾰ : V) :

The identity as a continuous normed group hom.

Equations

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 #

@[protected, instance]
noncomputable def normed_add_group_hom.has_neg {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

Opposite of a normed group hom.

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

Subtraction of normed group homs #

@[protected, instance]
def normed_add_group_hom.has_sub {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

Subtraction of normed group homs.

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

Scalar actions on normed group homs #

@[protected, instance]
def normed_add_group_hom.has_smul {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] :
Equations
@[simp]
theorem normed_add_group_hom.coe_smul {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] (r : R) (f : normed_add_group_hom V₁ V₂) :
(r f) = r f
@[simp]
theorem normed_add_group_hom.smul_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] (r : R) (f : normed_add_group_hom V₁ V₂) (v : V₁) :
(r f) v = r f v
@[protected, instance]
def normed_add_group_hom.smul_comm_class {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} {R' : Type u_6} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] [monoid_with_zero R'] [distrib_mul_action R' V₂] [pseudo_metric_space R'] [has_bounded_smul R' V₂] [smul_comm_class R R' V₂] :
@[protected, instance]
def normed_add_group_hom.is_scalar_tower {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} {R' : Type u_6} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] [monoid_with_zero R'] [distrib_mul_action R' V₂] [pseudo_metric_space R'] [has_bounded_smul R' V₂] [has_smul R R'] [is_scalar_tower R R' V₂] :
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem normed_add_group_hom.coe_nsmul {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (r : ) (f : normed_add_group_hom V₁ V₂) :
(r f) = r f
@[simp]
theorem normed_add_group_hom.nsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (r : ) (f : normed_add_group_hom V₁ V₂) (v : V₁) :
(r f) v = r f v
@[protected, instance]
Equations
@[simp]
theorem normed_add_group_hom.coe_zsmul {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (r : ) (f : normed_add_group_hom V₁ V₂) :
(r f) = r f
@[simp]
theorem normed_add_group_hom.zsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (r : ) (f : normed_add_group_hom V₁ V₂) (v : V₁) :
(r f) v = r f v

Normed group structure on normed group homs #

@[protected, instance]
noncomputable def normed_add_group_hom.add_comm_group {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]
noncomputable def normed_add_group_hom.to_normed_add_comm_group {V₁ : Type u_1} {V₂ : Type u_2} [normed_add_comm_group V₁] [normed_add_comm_group V₂] :

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

Equations
@[simp]
theorem normed_add_group_hom.coe_fn_add_hom_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (x : normed_add_group_hom V₁ V₂) (ᾰ : V₁) :
@[simp]
theorem normed_add_group_hom.coe_sum {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {ι : Type u_1} (s : finset ι) (f : ι → normed_add_group_hom V₁ V₂) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
theorem normed_add_group_hom.sum_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {ι : Type u_1} (s : finset ι) (f : ι → normed_add_group_hom V₁ V₂) (v : V₁) :
(s.sum (λ (i : ι), f i)) v = s.sum (λ (i : ι), (f i) v)

Module structure on normed group homs #

@[protected, instance]
noncomputable def normed_add_group_hom.module {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_1} [semiring R] [module R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] :
Equations

Composition of normed group homs #

@[protected]
noncomputable def normed_add_group_hom.comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) :

The composition of continuous normed group homs.

Equations
@[simp]
theorem normed_add_group_hom.comp_apply {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) (ᾰ : V₁) :
(g.comp f) = g (f ᾰ)
theorem normed_add_group_hom.norm_comp_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) :
theorem normed_add_group_hom.norm_comp_le_of_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {f : normed_add_group_hom V₁ V₂} {g : normed_add_group_hom V₂ V₃} {C₁ C₂ : } (hg : g C₂) (hf : f C₁) :
g.comp f C₂ * C₁
theorem normed_add_group_hom.norm_comp_le_of_le' {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {f : normed_add_group_hom V₁ V₂} {g : normed_add_group_hom V₂ V₃} (C₁ C₂ C₃ : ) (h : C₃ = C₂ * C₁) (hg : g C₂) (hf : f C₁) :
g.comp f C₃
noncomputable def normed_add_group_hom.comp_hom {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] :

Composition of normed groups hom as an additive group morphism.

Equations
@[simp]
theorem normed_add_group_hom.comp_zero {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₂ V₃) :
f.comp 0 = 0
@[simp]
theorem normed_add_group_hom.zero_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) :
0.comp f = 0
theorem normed_add_group_hom.comp_assoc {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {V₄ : Type u_1} [seminormed_add_comm_group V₄] (h : normed_add_group_hom V₃ V₄) (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) :
(h.comp g).comp f = h.comp (g.comp f)
theorem normed_add_group_hom.coe_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) :
(g.comp f) = g f

The inclusion of an add_subgroup, as bounded group homomorphism.

Equations
@[simp]

Kernel #

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

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

Equations
theorem normed_add_group_hom.mem_ker {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (v : V₁) :
v f.ker f v = 0
@[simp]
theorem normed_add_group_hom.ker.lift_apply_coe {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) (h : g.comp f = 0) (v : V₁) :
def normed_add_group_hom.ker.lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) (h : g.comp 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
@[simp]
theorem normed_add_group_hom.ker.incl_comp_lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) (h : g.comp f = 0) :
@[simp]
theorem normed_add_group_hom.ker_zero {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :
theorem normed_add_group_hom.coe_ker {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :
(f.ker) = f ⁻¹' {0}
theorem normed_add_group_hom.is_closed_ker {V₁ : Type u_3} [seminormed_add_comm_group V₁] {V₂ : Type u_1} [normed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

Range #

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

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

Equations
theorem normed_add_group_hom.mem_range {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (v : V₂) :
v f.range ∃ (w : V₁), f w = v
@[simp]
theorem normed_add_group_hom.mem_range_self {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (v : V₁) :
theorem normed_add_group_hom.comp_range {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) :

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

Equations
theorem normed_add_group_hom.norm_noninc.comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {g : normed_add_group_hom V₂ V₃} {f : normed_add_group_hom V₁ V₂} (hg : g.norm_noninc) (hf : f.norm_noninc) :
@[simp]
theorem normed_add_group_hom.norm_noninc.neg_iff {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} :
theorem normed_add_group_hom.isometry_comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {g : normed_add_group_hom V₂ V₃} {f : normed_add_group_hom V₁ V₂} (hg : isometry g) (hf : isometry f) :

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

Equations
@[simp]
theorem normed_add_group_hom.equalizer.lift_apply_coe {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) (v : V₁) :
def normed_add_group_hom.equalizer.lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) :

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

Equations
noncomputable def normed_add_group_hom.equalizer.lift_equiv {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} :
{φ // f.comp φ = g.comp φ} normed_add_group_hom V₁ (f.equalizer g)

The lifting property of the equalizer as an equivalence.

Equations
noncomputable def normed_add_group_hom.equalizer.map {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {W₁ : Type u_6} {W₂ : Type u_7} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} (φ : normed_add_group_hom V₁ V₂) (ψ : normed_add_group_hom W₁ W₂) (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :

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

Equations
@[simp]
theorem normed_add_group_hom.equalizer.ι_comp_map {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {W₁ : Type u_6} {W₂ : Type u_7} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :
theorem normed_add_group_hom.equalizer.comm_sq₂ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] [seminormed_add_comm_group W₃] {f₁ : normed_add_group_hom V₁ W₁} {f₂ : normed_add_group_hom V₂ W₂} {f₃ : normed_add_group_hom V₃ W₃} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} {φ' : normed_add_group_hom V₂ V₃} {ψ' : normed_add_group_hom W₂ W₃} (hf : ψ.comp f₁ = f₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') :
(ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
theorem normed_add_group_hom.equalizer.map_comp_map {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] [seminormed_add_comm_group W₃] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} {f₃ g₃ : normed_add_group_hom V₃ W₃} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} {φ' : normed_add_group_hom V₂ V₃} {ψ' : normed_add_group_hom W₂ W₃} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') (hg' : ψ'.comp g₂ = g₃.comp φ') :

The lifting of a norm nonincreasing morphism is norm nonincreasing.

theorem normed_add_group_hom.equalizer.norm_lift_le {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) (C : ) (hφ : φ C) :

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

theorem normed_add_group_hom.equalizer.map_norm_noninc {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {W₁ : Type u_6} {W₂ : Type u_7} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hφ : φ.norm_noninc) :
theorem normed_add_group_hom.equalizer.norm_map_le {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {W₁ : Type u_6} {W₂ : Type u_7} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (C : ) (hφ : φ.comp (normed_add_group_hom.equalizer.ι f₁ g₁) C) :
theorem controlled_closure_of_complete {G : Type u_1} [normed_add_comm_group G] [complete_space G] {H : Type u_2} [normed_add_comm_group H] {f : normed_add_group_hom G H} {K : add_subgroup H} {C ε : } (hC : 0 < C) (hε : 0 < ε) (hyp : f.surjective_on_with K C) :

Given f : normed_add_group_hom G H for some complete G and a subgroup K of H, if every element x of K has a preimage under f whose norm is at most C*∥x∥ then the same holds for elements of the (topological) closure of K with constant C+ε instead of C, for any positive ε.

theorem controlled_closure_range_of_complete {G : Type u_1} [normed_add_comm_group G] [complete_space G] {H : Type u_2} [normed_add_comm_group H] {f : normed_add_group_hom G H} {K : Type u_3} [seminormed_add_comm_group K] {j : normed_add_group_hom K H} (hj : ∀ (x : K), j x = x) {C ε : } (hC : 0 < C) (hε : 0 < ε) (hyp : ∀ (k : K), ∃ (g : G), f g = j k g C * k) :

Given f : normed_add_group_hom G H for some complete G, if every element x of the image of an isometric immersion j : normed_add_group_hom K H has a preimage under f whose norm is at most C*∥x∥ then the same holds for elements of the (topological) closure of this image with constant C+ε instead of C, for any positive ε. This is useful in particular if j is the inclusion of a normed group into its completion (in this case the closure is the full target group).