The category of seminormed groups #

We define SemiNormedGroupCat, the category of seminormed groups and normed group homs between them, as well as SemiNormedGroupCat₁, the subcategory of norm non-increasing morphisms.

The category of seminormed abelian groups and bounded group homomorphisms.

Instances For

    Construct a bundled SemiNormedGroupCat from the underlying type and typeclass.

    Instances For
      theorem SemiNormedGroupCat.ext {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} {f₁ : M N} {f₂ : M N} (h : ∀ (x : M), f₁ x = f₂ x) :
      f₁ = f₂
      theorem SemiNormedGroupCat.zero_apply {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} (x : V) :
      0 x = 0

      SemiNormedGroupCat₁ is a type synonym for SemiNormedGroupCat, which we shall equip with the category structure consisting only of the norm non-increasing maps.

      Instances For
        theorem SemiNormedGroupCat₁.hom_ext {M : SemiNormedGroupCat₁} {N : SemiNormedGroupCat₁} (f : M N) (g : M N) (w : f = g) :
        f = g

        Construct a bundled SemiNormedGroupCat₁ from the underlying type and typeclass.

        Instances For