# mathlibdocumentation

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

structure normed_group_hom (V : Type u_1) (W : Type u_2)  :
Type (max u_1 u_2)

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

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

Equations
def add_monoid_hom.mk_normed_group_hom' {V : Type u_1} {W : Type u_2} (f : V →+ W) (C : ℝ≥0) (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_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} {f : V → W} (M : ) (h : ∀ (x : V), f x M * x) :
∃ (N : ), 0 < N ∀ (x : V), f x N * x
@[instance]
def normed_group_hom.has_coe_to_fun {V₁ : Type u_2} {V₂ : Type u_3}  :
Equations
theorem normed_group_hom.coe_inj {V₁ : Type u_2} {V₂ : Type u_3} {f g : V₂} (H : f = g) :
f = g
theorem normed_group_hom.coe_injective {V₁ : Type u_2} {V₂ : Type u_3}  :
theorem normed_group_hom.coe_inj_iff {V₁ : Type u_2} {V₂ : Type u_3} {f g : V₂} :
f = g f = g
@[ext]
theorem normed_group_hom.ext {V₁ : Type u_2} {V₂ : Type u_3} {f g : V₂} (H : ∀ (x : V₁), f x = g x) :
f = g
theorem normed_group_hom.ext_iff {V₁ : Type u_2} {V₂ : Type u_3} {f g : V₂} :
f = g ∀ (x : V₁), f x = g x
@[simp]
theorem normed_group_hom.to_fun_eq_coe {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) :
@[simp]
theorem normed_group_hom.coe_mk {V₁ : Type u_2} {V₂ : Type u_3} (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_group_hom.coe_mk_normed_group_hom {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) (C : ) (hC : ∀ (v : V₁), f v C * v) :
hC) = f
@[simp]
theorem normed_group_hom.coe_mk_normed_group_hom' {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) (C : ℝ≥0) (hC : ∀ (x : V₁), f x∥₊ C * x∥₊) :
hC) = f
def normed_group_hom.to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) :
V₁ →+ V₂

The group homomorphism underlying a bounded group homomorphism.

Equations
@[simp]
theorem normed_group_hom.coe_to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) :
theorem normed_group_hom.to_add_monoid_hom_injective {V₁ : Type u_2} {V₂ : Type u_3}  :
@[simp]
theorem normed_group_hom.mk_to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ → V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ∃ (C : ), ∀ (v : V₁), f v C * v) :
@[simp]
theorem normed_group_hom.map_zero {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) :
f 0 = 0
@[simp]
theorem normed_group_hom.map_add {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) (x y : V₁) :
f (x + y) = f x + f y
@[simp]
theorem normed_group_hom.map_sum {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) {ι : Type u_1} (v : ι → V₁) (s : finset ι) :
f (∑ (i : ι) in s, v i) = ∑ (i : ι) in s, f (v i)
@[simp]
theorem normed_group_hom.map_sub {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) (x y : V₁) :
f (x - y) = f x - f y
@[simp]
theorem normed_group_hom.map_neg {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) (x : V₁) :
f (-x) = -f x
theorem normed_group_hom.bound {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) :
∃ (C : ), 0 < C ∀ (x : V₁), f x C * x
theorem normed_group_hom.antilipschitz_of_norm_ge {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) {K : ℝ≥0} (h : ∀ (x : V₁), x (K) * f x) :

### The operator norm #

def normed_group_hom.op_norm {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) :

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

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

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

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

continuous linear maps are Lipschitz continuous.

theorem normed_group_hom.uniform_continuous {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) :
theorem normed_group_hom.continuous {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) :
theorem normed_group_hom.ratio_le_op_norm {V₁ : Type u_2} {V₂ : Type u_3} (f : V₂) (x : V₁) :
theorem normed_group_hom.op_norm_le_bound {V₁ : Type u_2} {V₂ : Type u_3} (f : 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_group_hom.op_norm_le_of_lipschitz {V₁ : Type u_2} {V₂ : Type u_3} {f : V₂} {K : ℝ≥0} (hf : f) :
theorem normed_group_hom.mk_normed_group_hom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} (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_group_hom, then its norm is bounded by the bound given to the constructor if it is nonnegative.

theorem normed_group_hom.mk_normed_group_hom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) {C : } (h : ∀ (x : V₁), f x C * x) :
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.

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

Alias of mk_normed_group_hom_norm_le.

theorem add_monoid_hom.mk_normed_group_hom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} (f : V₁ →+ V₂) {C : } (h : ∀ (x : V₁), f x C * x) :
h max C 0

Alias of mk_normed_group_hom_norm_le'.

### Addition of normed group homs #

@[instance]
def normed_group_hom.has_add {V₁ : Type u_2} {V₂ : Type u_3}  :

Equations
theorem normed_group_hom.op_norm_add_le {V₁ : Type u_2} {V₂ : Type u_3} (f g : V₂) :

The operator norm satisfies the triangle inequality.

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

### The zero normed group hom #

@[instance]
def normed_group_hom.has_zero {V₁ : Type u_2} {V₂ : Type u_3}  :
has_zero V₂)
Equations
@[instance]
def normed_group_hom.inhabited {V₁ : Type u_2} {V₂ : Type u_3}  :
inhabited V₂)
Equations
theorem normed_group_hom.op_norm_zero {V₁ : Type u_2} {V₂ : Type u_3}  :

The norm of the 0 operator is 0.

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

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

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

### The identity normed group hom #

@[simp]
theorem normed_group_hom.id_apply (V : Type u_1) (ᾰ : V) :
=
def normed_group_hom.id (V : Type u_1)  :

The identity as a continuous normed group hom.

Equations
theorem normed_group_hom.norm_id_le (V : Type u_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.

theorem normed_group_hom.norm_id_of_nontrivial_seminorm (V : Type u_1) (h : ∃ (x : V), x 0) :

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

theorem normed_group_hom.norm_id {V : Type u_1} [normed_group V] [nontrivial V] :

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

theorem normed_group_hom.coe_id (V : Type u_1)  :

### The negation of a normed group hom #

@[instance]
def normed_group_hom.has_neg {V₁ : Type u_2} {V₂ : Type u_3}  :
has_neg V₂)

Opposite of a normed group hom.

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

### Subtraction of normed group homs #

@[instance]
def normed_group_hom.has_sub {V₁ : Type u_2} {V₂ : Type u_3}  :
has_sub V₂)

Subtraction of normed group homs.

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

### Normed group structure on normed group homs #

@[instance]
def normed_group_hom.add_comm_group {V₁ : Type u_2} {V₂ : Type u_3}  :

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

Equations
@[instance]
def normed_group_hom.to_semi_normed_group {V₁ : Type u_2} {V₂ : Type u_3}  :

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

Equations
@[instance]
def normed_group_hom.to_normed_group {V₁ : Type u_1} {V₂ : Type u_2} [normed_group V₁] [normed_group V₂] :

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

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

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

### Composition of normed group homs #

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

The composition of continuous normed group homs.

Equations
theorem normed_group_hom.norm_comp_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} (g : V₃) (f : V₂) :
theorem normed_group_hom.norm_comp_le_of_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {f : V₂} {g : V₃} {C₁ C₂ : } (hg : g C₂) (hf : f C₁) :
g.comp f C₂ * C₁
theorem normed_group_hom.norm_comp_le_of_le' {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {f : V₂} {g : V₃} (C₁ C₂ C₃ : ) (h : C₃ = C₂ * C₁) (hg : g C₂) (hf : f C₁) :
g.comp f C₃
def normed_group_hom.comp_hom {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4}  :
V₃ →+ V₂ →+ V₃

Composition of normed groups hom as an additive group morphism.

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

The inclusion of an add_subgroup, as bounded group homomorphism.

Equations
@[simp]
theorem normed_group_hom.incl_apply {V : Type u_1} (s : add_subgroup V) (ᾰ : s) :
=
theorem normed_group_hom.norm_incl {V : Type u_1} {V' : add_subgroup V} (x : V') :

### Kernel #

def normed_group_hom.ker {V₁ : Type u_3} {V₂ : Type u_4} (f : V₂) :

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

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

### Range #

def normed_group_hom.range {V₁ : Type u_3} {V₂ : Type u_4} (f : V₂) :

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

Equations
theorem normed_group_hom.mem_range {V₁ : Type u_3} {V₂ : Type u_4} (f : V₂) (v : V₂) :
v f.range ∃ (w : V₁), f w = v
theorem normed_group_hom.comp_range {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} (f : V₂) (g : V₃) :
(g.comp f).range =
theorem normed_group_hom.incl_range {V₁ : Type u_3} (s : add_subgroup V₁) :
@[simp]
theorem normed_group_hom.range_comp_incl_top {V₁ : Type u_3} {V₂ : Type u_4} (f : V₂) :
def normed_group_hom.norm_noninc {V : Type u_1} {W : Type u_2} (f : W) :
Prop

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

Equations
theorem normed_group_hom.norm_noninc.norm_noninc_iff_norm_le_one {V : Type u_1} {W : Type u_2} {f : W} :
theorem normed_group_hom.norm_noninc.zero {V₁ : Type u_3} {V₂ : Type u_4}  :
theorem normed_group_hom.norm_noninc.id {V : Type u_1}  :
theorem normed_group_hom.norm_noninc.comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} {g : V₃} {f : V₂} (hg : g.norm_noninc) (hf : f.norm_noninc) :
theorem normed_group_hom.isometry_iff_norm {V : Type u_1} {W : Type u_2} (f : W) :
∀ (v : V), f v = v
theorem normed_group_hom.isometry_of_norm {V : Type u_1} {W : Type u_2} (f : W) (hf : ∀ (v : V), f v = v) :
theorem normed_group_hom.norm_eq_of_isometry {V : Type u_1} {W : Type u_2} {f : W} (hf : isometry f) (v : V) :
theorem normed_group_hom.isometry_id {V : Type u_1}  :
theorem normed_group_hom.isometry_comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} {g : V₃} {f : V₂} (hg : isometry g) (hf : isometry f) :
theorem normed_group_hom.norm_noninc_of_isometry {V : Type u_1} {W : Type u_2} {f : W} (hf : isometry f) :
def normed_group_hom.equalizer {V : Type u_1} {W : Type u_2} (f g : W) :

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

Equations
def normed_group_hom.equalizer.ι {V : Type u_1} {W : Type u_2} (f g : W) :
V

The inclusion of f.equalizer g as a normed_group_hom.

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

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

Equations
@[simp]
theorem normed_group_hom.equalizer.ι_comp_lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f g : W} (φ : V) (h : f.comp φ = g.comp φ) :
@[simp]
theorem normed_group_hom.equalizer.lift_equiv_apply {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f g : W} (φ : {φ // f.comp φ = g.comp φ}) :
def normed_group_hom.equalizer.lift_equiv {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f g : W} :
{φ // f.comp φ = g.comp φ} (f.equalizer g)

The lifting property of the equalizer as an equivalence.

Equations
@[simp]
theorem normed_group_hom.equalizer.lift_equiv_symm_apply_coe {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f g : W} (ψ : (f.equalizer g)) :
def normed_group_hom.equalizer.map {V₁ : Type u_3} {V₂ : Type u_4} {W₁ : Type u_6} {W₂ : Type u_7} {f₁ g₁ : W₁} {f₂ g₂ : W₂} (φ : V₂) (ψ : W₂) (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :

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

Equations
• hg =
@[simp]
theorem normed_group_hom.equalizer.ι_comp_map {V₁ : Type u_3} {V₂ : Type u_4} {W₁ : Type u_6} {W₂ : Type u_7} {f₁ g₁ : W₁} {f₂ g₂ : W₂} {φ : V₂} {ψ : W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :
g₂).comp hg) = φ.comp g₁)
@[simp]
theorem normed_group_hom.equalizer.map_id {V₁ : Type u_3} {W₁ : Type u_6} {f₁ g₁ : W₁} :
theorem normed_group_hom.equalizer.comm_sq₂ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} {f₁ : W₁} {f₂ : W₂} {f₃ : W₃} {φ : V₂} {ψ : W₂} {φ' : V₃} {ψ' : W₃} (hf : ψ.comp f₁ = f₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') :
(ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)
theorem normed_group_hom.equalizer.map_comp_map {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} {f₁ g₁ : W₁} {f₂ g₂ : W₂} {f₃ g₃ : W₃} {φ : V₂} {ψ : W₂} {φ' : V₃} {ψ' : W₃} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') (hg' : ψ'.comp g₂ = g₃.comp φ') :
hf' hg').comp hg) = (ψ'.comp ψ) _ _
theorem normed_group_hom.equalizer.ι_norm_noninc {V : Type u_1} {W : Type u_2} {f g : W} :
theorem normed_group_hom.equalizer.lift_norm_noninc {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} {f g : W} (φ : V) (h : f.comp φ = g.comp φ) (hφ : φ.norm_noninc) :

The lifting of a norm nonincreasing morphism is norm nonincreasing.

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

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

theorem normed_group_hom.equalizer.map_norm_noninc {V₁ : Type u_3} {V₂ : Type u_4} {W₁ : Type u_6} {W₂ : Type u_7} {f₁ g₁ : W₁} {f₂ g₂ : W₂} {φ : V₂} {ψ : W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hφ : φ.norm_noninc) :
theorem normed_group_hom.equalizer.norm_map_le {V₁ : Type u_3} {V₂ : Type u_4} {W₁ : Type u_6} {W₂ : Type u_7} {f₁ g₁ : W₁} {f₂ g₂ : W₂} {φ : V₂} {ψ : W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (C : ) (hφ : φ.comp g₁) C) :
hg C