Documentation

Mathlib.Analysis.Normed.Group.SemiNormedGrp

The category of seminormed groups #

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

def SemiNormedGrp :
Type (u + 1)

The category of seminormed abelian groups and bounded group homomorphisms.

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.

    Construct a bundled SemiNormedGrp from the underlying type and typeclass.

    Equations
    Instances For
      Equations
      • M.instSeminormedAddCommGroupα = M.str
      instance SemiNormedGrp.funLike {V : SemiNormedGrp} {W : SemiNormedGrp} :
      FunLike (V W) V W
      Equations
      Equations
      • =
      theorem SemiNormedGrp.ext_iff {M : SemiNormedGrp} {N : SemiNormedGrp} {f₁ : M N} {f₂ : M N} :
      f₁ = f₂ ∀ (x : M), f₁ x = f₂ x
      theorem SemiNormedGrp.ext {M : SemiNormedGrp} {N : SemiNormedGrp} {f₁ : M N} {f₂ : M N} (h : ∀ (x : M), f₁ x = f₂ x) :
      f₁ = f₂
      @[simp]
      theorem SemiNormedGrp.coe_comp {M : SemiNormedGrp} {N : SemiNormedGrp} {K : SemiNormedGrp} (f : M N) (g : N K) :
      Equations
      • SemiNormedGrp.instZeroHom = NormedAddGroupHom.zero
      @[simp]
      theorem SemiNormedGrp.zero_apply {V : SemiNormedGrp} {W : SemiNormedGrp} (x : V) :
      0 x = 0
      def SemiNormedGrp₁ :
      Type (u + 1)

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

      Equations
      Instances For
        Equations
        • X.instFunLike Y = { coe := fun (f : X Y) => (↑f).toFun, coe_injective' := }
        theorem SemiNormedGrp₁.hom_ext_iff {M : SemiNormedGrp₁} {N : SemiNormedGrp₁} {f : M N} {g : M N} :
        f = g f = g
        theorem SemiNormedGrp₁.hom_ext {M : SemiNormedGrp₁} {N : SemiNormedGrp₁} (f : M N) (g : M N) (w : f = g) :
        f = g
        Equations
        • One or more equations did not get rendered due to their size.

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

        Equations
        Instances For
          Equations
          • M.instSeminormedAddCommGroupα = M.str

          Promote a morphism in SemiNormedGrp to a morphism in SemiNormedGrp₁.

          Equations
          Instances For

            Promote an isomorphism in SemiNormedGrp to an isomorphism in SemiNormedGrp₁.

            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              Equations
              • X.instZeroHom Y = { zero := 0, }
              @[simp]
              theorem SemiNormedGrp₁.zero_apply {V : SemiNormedGrp₁} {W : SemiNormedGrp₁} (x : V) :
              0 x = 0