# mathlibdocumentation

analysis.normed_space.SemiNormedGroup.kernels

# Cokernels in SemiNormedGroup₁ and SemiNormedGroup #

We show that SemiNormedGroup₁ has cokernels (for which of course the cokernel.π f maps are norm non-increasing), as well as the easier result that SemiNormedGroup has cokernels.

So far, I don't see a way to state nicely what we really want: SemiNormedGroup has cokernels, and cokernel.π f is norm non-increasing. The problem is that the limits API doesn't promise you any particular model of the cokernel, and in SemiNormedGroup one can always take a cokernel and rescale its norm (and hence making cokernel.π f arbitrarily large in norm), obtaining another categorical cokernel.

Auxiliary definition for has_cokernels SemiNormedGroup₁.

Equations

Auxiliary definition for has_cokernels SemiNormedGroup₁.

Equations

Auxiliary definition for has_cokernels SemiNormedGroup.

Equations

Auxiliary definition for has_cokernels SemiNormedGroup.

Equations

Auxiliary definition for has_cokernels SemiNormedGroup.

Equations

An explicit choice of cokernel, which has good properties with respect to the norm.

Equations
def SemiNormedGroup.explicit_cokernel_desc {X Y Z : SemiNormedGroup} {f : X Y} {g : Y Z} (w : f g = 0) :

Descend to the explicit cokernel.

Equations

The projection from Y to the explicit cokernel of X ⟶ Y.

Equations
@[simp]
theorem SemiNormedGroup.comp_explicit_cokernel_π_assoc {X Y : SemiNormedGroup} (f : X Y) {X' : SemiNormedGroup} (f' : X') :
= 0 f'
@[simp]
theorem SemiNormedGroup.explicit_cokernel_π_desc {X Y Z : SemiNormedGroup} {f : X Y} {g : Y Z} (w : f g = 0) :
@[simp]
theorem SemiNormedGroup.explicit_cokernel_π_desc_assoc {X Y Z : SemiNormedGroup} {f : X Y} {g : Y Z} (w : f g = 0) {X' : SemiNormedGroup} (f' : Z X') :
theorem SemiNormedGroup.explicit_cokernel_desc_unique {X Y Z : SemiNormedGroup} {f : X Y} {g : Y Z} (w : f g = 0) (he : = g) :
@[ext]
theorem SemiNormedGroup.explicit_cokernel_hom_ext {X Y Z : SemiNormedGroup} {f : X Y} (e₁ e₂ : Z)  :
e₁ = e₂
theorem SemiNormedGroup.explicit_cokernel_desc_norm_le_of_norm_le {X Y Z : SemiNormedGroup} {f : X Y} {g : Y Z} (w : f g = 0) (c : ℝ≥0) (h : g c) :
theorem SemiNormedGroup.explicit_cokernel_desc_norm_le {X Y Z : SemiNormedGroup} {f : X Y} {g : Y Z} (w : f g = 0) :

The explicit cokernel is isomorphic to the usual cokernel.

Equations
@[simp]
@[simp]
@[simp]
theorem SemiNormedGroup.explicit_cokernel_iso_hom_desc {X Y Z : SemiNormedGroup} {f : X Y} {g : Y Z} (w : f g = 0) :