Documentation

Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion

Completions of normed groups #

This file contains an API for completions of seminormed groups (basic facts about objects and morphisms).

Main definitions #

Projects #

  1. Construct the category of complete seminormed groups, say CompleteSemiNormedGrp and promote the Completion functor below to a functor landing in this category.
  2. Prove that the functor Completion : SemiNormedGrp ⥤ CompleteSemiNormedGrp is left adjoint to the forgetful functor.

The completion of a seminormed group, as an endofunctor on SemiNormedGrp.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem SemiNormedGrp.completion.incl_apply {V : SemiNormedGrp} (v : V) :
    SemiNormedGrp.completion.incl v = V v

    The canonical morphism from a seminormed group V to its completion.

    Equations
    • SemiNormedGrp.completion.incl = { toFun := fun (v : V) => V v, map_add' := , bound' := }
    Instances For
      theorem SemiNormedGrp.completion.norm_incl_eq {V : SemiNormedGrp} {v : V} :
      SemiNormedGrp.completion.incl v = v

      Given a normed group hom V ⟶ W, this defines the associated morphism from the completion of V to the completion of W. The difference from the definition obtained from the functoriality of completion is in that the map sending a morphism f to the associated morphism of completions is itself additive.

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

        Given a normed group hom f : V → W with W complete, this provides a lift of f to the completion of V. The lemmas lift_unique and lift_comp_incl provide the api for the universal property of the completion.

        Equations
        Instances For