Documentation

Mathlib.Analysis.Normed.Group.SemiNormedGroupCat.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 CompleteSemiNormedGroupCat and promote the Completion functor below to a functor landing in this category.
  2. Prove that the functor Completion : SemiNormedGroupCat ⥤ CompleteSemiNormedGroupCat is left adjoint to the forgetful functor.
source
@[simp]
theorem SemiNormedGroupCat.completion_obj (V : SemiNormedGroupCat) :
SemiNormedGroupCat.completion.toPrefunctor.obj V = SemiNormedGroupCat.of (UniformSpace.Completion ↑V)
source
@[simp]
theorem SemiNormedGroupCat.completion_map :
∀ {X Y : SemiNormedGroupCat} (f : X ⟶ Y), SemiNormedGroupCat.completion.toPrefunctor.map f = NormedAddGroupHom.completion f
source
def SemiNormedGroupCat.completion :
CategoryTheory.Functor SemiNormedGroupCat SemiNormedGroupCat

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance SemiNormedGroupCat.completion_completeSpace {V : SemiNormedGroupCat} :
    CompleteSpace ↑(SemiNormedGroupCat.completion.toPrefunctor.obj V)
    Equations
    source
    @[simp]
    theorem SemiNormedGroupCat.completion.incl_apply {V : SemiNormedGroupCat} (v : ↑V) :
    SemiNormedGroupCat.completion.incl v = ↑↑V v
    source
    def SemiNormedGroupCat.completion.incl {V : SemiNormedGroupCat} :
    V ⟶ SemiNormedGroupCat.completion.toPrefunctor.obj V

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem SemiNormedGroupCat.completion.norm_incl_eq {V : SemiNormedGroupCat} {v : ↑V} :
      ‖SemiNormedGroupCat.completion.incl v‖ = ‖v‖
      source
      theorem SemiNormedGroupCat.completion.map_normNoninc {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} {f : V ⟶ W} (hf : NormedAddGroupHom.NormNoninc f) :
      NormedAddGroupHom.NormNoninc (SemiNormedGroupCat.completion.toPrefunctor.map f)
      source
      def SemiNormedGroupCat.completion.mapHom (V : SemiNormedGroupCat) (W : SemiNormedGroupCat) :
      let_fun this := fun (V W : SemiNormedGroupCat) => inferInstanceAs (AddGroup (NormedAddGroupHom ↑V ↑W)); (V ⟶ W) →+ (SemiNormedGroupCat.completion.toPrefunctor.obj V ⟶ SemiNormedGroupCat.completion.toPrefunctor.obj W)

      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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem SemiNormedGroupCat.completion.map_zero (V : SemiNormedGroupCat) (W : SemiNormedGroupCat) :
        SemiNormedGroupCat.completion.toPrefunctor.map 0 = 0
        source
        instance SemiNormedGroupCat.instPreadditiveSemiNormedGroupCatInstSemiNormedGroupCatLargeCategory :
        CategoryTheory.Preadditive SemiNormedGroupCat
        Equations
        source
        instance SemiNormedGroupCat.instAdditiveSemiNormedGroupCatInstSemiNormedGroupCatLargeCategoryInstPreadditiveSemiNormedGroupCatInstSemiNormedGroupCatLargeCategoryCompletion :
        CategoryTheory.Functor.Additive SemiNormedGroupCat.completion
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def SemiNormedGroupCat.completion.lift {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} [CompleteSpace ↑W] [SeparatedSpace ↑W] (f : V ⟶ W) :
        SemiNormedGroupCat.completion.toPrefunctor.obj V ⟶ W

        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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem SemiNormedGroupCat.completion.lift_comp_incl {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} [CompleteSpace ↑W] [SeparatedSpace ↑W] (f : V ⟶ W) :
          CategoryTheory.CategoryStruct.comp SemiNormedGroupCat.completion.incl (SemiNormedGroupCat.completion.lift f) = f
          source
          theorem SemiNormedGroupCat.completion.lift_unique {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} [CompleteSpace ↑W] [SeparatedSpace ↑W] (f : V ⟶ W) (g : SemiNormedGroupCat.completion.toPrefunctor.obj V ⟶ W) :
          CategoryTheory.CategoryStruct.comp SemiNormedGroupCat.completion.incl g = f → g = SemiNormedGroupCat.completion.lift f