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.

def SemiNormedGroupCat : Type (u + 1)

The category of seminormed abelian groups and bounded group homomorphisms.

Equations

• SemiNormedGroupCat = CategoryTheory.Bundled SeminormedAddCommGroup

instance SemiNormedGroupCat.bundledHom : CategoryTheory.BundledHom NormedAddGroupHom

Equations

• SemiNormedGroupCat.bundledHom = CategoryTheory.BundledHom.mk (@NormedAddGroupHom.toFun) NormedAddGroupHom.id @NormedAddGroupHom.comp

instance SemiNormedGroupCat.instConcreteCategorySemiNormedGroupCatInstSemiNormedGroupCatLargeCategory : CategoryTheory.ConcreteCategory SemiNormedGroupCat

Equations

• SemiNormedGroupCat.instConcreteCategorySemiNormedGroupCatInstSemiNormedGroupCatLargeCategory = id inferInstance

instance SemiNormedGroupCat.instCoeSortSemiNormedGroupCatType : CoeSort SemiNormedGroupCat (Type u_1)

Equations

• SemiNormedGroupCat.instCoeSortSemiNormedGroupCatType = { coe := fun (X : SemiNormedGroupCat) => ↑X }

def SemiNormedGroupCat.of (M : Type u) [SeminormedAddCommGroup M] : SemiNormedGroupCat

Construct a bundled SemiNormedGroupCat from the underlying type and typeclass.

Equations

• SemiNormedGroupCat.of M = CategoryTheory.Bundled.of M

instance SemiNormedGroupCat.instSeminormedAddCommGroupα (M : SemiNormedGroupCat) : SeminormedAddCommGroup ↑M

Equations

• SemiNormedGroupCat.instSeminormedAddCommGroupα M = M.str

instance SemiNormedGroupCat.funLike {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} : FunLike (V ⟶ W) ↑V ↑W

Equations

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

instance SemiNormedGroupCat.toAddMonoidHomClass {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} : AddMonoidHomClass (V ⟶ W) ↑V ↑W

Equations

• (_ : AddMonoidHomClass (V ⟶ W) ↑V ↑W) = (_ : AddMonoidHomClass (V ⟶ W) ↑V ↑W)

theorem SemiNormedGroupCat.ext {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} {f₁ : M ⟶ N} {f₂ : M ⟶ N} (h : ∀ (x : ↑M), f₁ x = f₂ x) : f₁ = f₂

@[simp]

theorem SemiNormedGroupCat.coe_of (V : Type u) [SeminormedAddCommGroup V] : ↑(SemiNormedGroupCat.of V) = V

@[simp]

theorem SemiNormedGroupCat.coe_id (V : SemiNormedGroupCat) : ⇑(CategoryTheory.CategoryStruct.id V) = id

@[simp]

theorem SemiNormedGroupCat.coe_comp {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} {K : SemiNormedGroupCat} (f : M ⟶ N) (g : N ⟶ K) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

instance SemiNormedGroupCat.instInhabitedSemiNormedGroupCat : Inhabited SemiNormedGroupCat

Equations

• SemiNormedGroupCat.instInhabitedSemiNormedGroupCat = { default := SemiNormedGroupCat.of PUnit.{u_1 + 1} }

instance SemiNormedGroupCat.ofUnique (V : Type u) [SeminormedAddCommGroup V] [i : Unique V] : Unique ↑(SemiNormedGroupCat.of V)

Equations

• SemiNormedGroupCat.ofUnique V = i

instance SemiNormedGroupCat.instZeroHomSemiNormedGroupCatToQuiverToCategoryStructInstSemiNormedGroupCatLargeCategory {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} : Zero (M ⟶ N)

Equations

• SemiNormedGroupCat.instZeroHomSemiNormedGroupCatToQuiverToCategoryStructInstSemiNormedGroupCatLargeCategory = NormedAddGroupHom.zero

@[simp]

theorem SemiNormedGroupCat.zero_apply {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} (x : ↑V) : 0 x = 0

instance SemiNormedGroupCat.instHasZeroMorphismsSemiNormedGroupCatInstSemiNormedGroupCatLargeCategory : CategoryTheory.Limits.HasZeroMorphisms SemiNormedGroupCat

Equations

• SemiNormedGroupCat.instHasZeroMorphismsSemiNormedGroupCatInstSemiNormedGroupCatLargeCategory = CategoryTheory.Limits.HasZeroMorphisms.mk

theorem SemiNormedGroupCat.isZero_of_subsingleton (V : SemiNormedGroupCat) [Subsingleton ↑V] : CategoryTheory.Limits.IsZero V

instance SemiNormedGroupCat.hasZeroObject : CategoryTheory.Limits.HasZeroObject SemiNormedGroupCat

Equations

• SemiNormedGroupCat.hasZeroObject = (_ : CategoryTheory.Limits.HasZeroObject SemiNormedGroupCat)

theorem SemiNormedGroupCat.iso_isometry_of_normNoninc {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} (i : V ≅ W) (h1 : NormedAddGroupHom.NormNoninc i.hom) (h2 : NormedAddGroupHom.NormNoninc i.inv) : Isometry ⇑i.hom

def SemiNormedGroupCat₁ : Type (u + 1)

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

Equations

• SemiNormedGroupCat₁ = CategoryTheory.Bundled SeminormedAddCommGroup

instance SemiNormedGroupCat₁.instCoeSortSemiNormedGroupCat₁Type : CoeSort SemiNormedGroupCat₁ (Type u_1)

Equations

• SemiNormedGroupCat₁.instCoeSortSemiNormedGroupCat₁Type = { coe := fun (X : SemiNormedGroupCat₁) => ↑X }

instance SemiNormedGroupCat₁.instLargeCategorySemiNormedGroupCat₁ : CategoryTheory.LargeCategory SemiNormedGroupCat₁

Equations

• SemiNormedGroupCat₁.instLargeCategorySemiNormedGroupCat₁ = CategoryTheory.Category.mk

instance SemiNormedGroupCat₁.instFunLike (X : SemiNormedGroupCat₁) (Y : SemiNormedGroupCat₁) : FunLike (X ⟶ Y) ↑X ↑Y

Equations

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

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

instance SemiNormedGroupCat₁.instConcreteCategorySemiNormedGroupCat₁InstLargeCategorySemiNormedGroupCat₁ : CategoryTheory.ConcreteCategory SemiNormedGroupCat₁

Equations

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

instance SemiNormedGroupCat₁.toAddMonoidHomClass {V : SemiNormedGroupCat₁} {W : SemiNormedGroupCat₁} : AddMonoidHomClass (V ⟶ W) ↑V ↑W

Equations

• (_ : AddMonoidHomClass (V ⟶ W) ↑V ↑W) = (_ : AddMonoidHomClass (V ⟶ W) ↑V ↑W)

def SemiNormedGroupCat₁.of (M : Type u) [SeminormedAddCommGroup M] : SemiNormedGroupCat₁

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

Equations

• SemiNormedGroupCat₁.of M = CategoryTheory.Bundled.of M

instance SemiNormedGroupCat₁.instSeminormedAddCommGroupα (M : SemiNormedGroupCat₁) : SeminormedAddCommGroup ↑M

Equations

• SemiNormedGroupCat₁.instSeminormedAddCommGroupα M = M.str

def SemiNormedGroupCat₁.mkHom {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} (f : M ⟶ N) (i : NormedAddGroupHom.NormNoninc f) : SemiNormedGroupCat₁.of ↑M ⟶ SemiNormedGroupCat₁.of ↑N

Promote a morphism in SemiNormedGroupCat to a morphism in SemiNormedGroupCat₁.

Equations

• SemiNormedGroupCat₁.mkHom f i = { val := f, property := i }

theorem SemiNormedGroupCat₁.mkHom_apply {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} (f : M ⟶ N) (i : NormedAddGroupHom.NormNoninc f) (x : ↑(SemiNormedGroupCat₁.of ↑M)) : (SemiNormedGroupCat₁.mkHom f i) x = f x

@[simp]

theorem SemiNormedGroupCat₁.mkIso_inv {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} (f : M ≅ N) (i : NormedAddGroupHom.NormNoninc f.hom) (i' : NormedAddGroupHom.NormNoninc f.inv) : (SemiNormedGroupCat₁.mkIso f i i').inv = SemiNormedGroupCat₁.mkHom f.inv i'

@[simp]

theorem SemiNormedGroupCat₁.mkIso_hom {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} (f : M ≅ N) (i : NormedAddGroupHom.NormNoninc f.hom) (i' : NormedAddGroupHom.NormNoninc f.inv) : (SemiNormedGroupCat₁.mkIso f i i').hom = SemiNormedGroupCat₁.mkHom f.hom i

def SemiNormedGroupCat₁.mkIso {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} (f : M ≅ N) (i : NormedAddGroupHom.NormNoninc f.hom) (i' : NormedAddGroupHom.NormNoninc f.inv) : SemiNormedGroupCat₁.of ↑M ≅ SemiNormedGroupCat₁.of ↑N

Promote an isomorphism in SemiNormedGroupCat to an isomorphism in SemiNormedGroupCat₁.

Equations

• SemiNormedGroupCat₁.mkIso f i i' = CategoryTheory.Iso.mk (SemiNormedGroupCat₁.mkHom f.hom i) (SemiNormedGroupCat₁.mkHom f.inv i')

instance SemiNormedGroupCat₁.instHasForget₂SemiNormedGroupCat₁SemiNormedGroupCatInstLargeCategorySemiNormedGroupCat₁InstConcreteCategorySemiNormedGroupCat₁InstLargeCategorySemiNormedGroupCat₁InstSemiNormedGroupCatLargeCategoryInstConcreteCategorySemiNormedGroupCatInstSemiNormedGroupCatLargeCategory : CategoryTheory.HasForget₂ SemiNormedGroupCat₁ SemiNormedGroupCat

Equations

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

@[simp]

theorem SemiNormedGroupCat₁.coe_of (V : Type u) [SeminormedAddCommGroup V] : ↑(SemiNormedGroupCat₁.of V) = V

@[simp]

theorem SemiNormedGroupCat₁.coe_id (V : SemiNormedGroupCat₁) : ⇑(CategoryTheory.CategoryStruct.id V) = id

@[simp]

theorem SemiNormedGroupCat₁.coe_comp {M : SemiNormedGroupCat₁} {N : SemiNormedGroupCat₁} {K : SemiNormedGroupCat₁} (f : M ⟶ N) (g : N ⟶ K) : ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f

instance SemiNormedGroupCat₁.instInhabitedSemiNormedGroupCat₁ : Inhabited SemiNormedGroupCat₁

Equations

• SemiNormedGroupCat₁.instInhabitedSemiNormedGroupCat₁ = { default := SemiNormedGroupCat₁.of PUnit.{u_1 + 1} }

instance SemiNormedGroupCat₁.ofUnique (V : Type u) [SeminormedAddCommGroup V] [i : Unique V] : Unique ↑(SemiNormedGroupCat₁.of V)

Equations

• SemiNormedGroupCat₁.ofUnique V = i

instance SemiNormedGroupCat₁.instZeroHomSemiNormedGroupCat₁ToQuiverToCategoryStructInstLargeCategorySemiNormedGroupCat₁ (X : SemiNormedGroupCat₁) (Y : SemiNormedGroupCat₁) : Zero (X ⟶ Y)

Equations

• SemiNormedGroupCat₁.instZeroHomSemiNormedGroupCat₁ToQuiverToCategoryStructInstLargeCategorySemiNormedGroupCat₁ X Y = { zero := { val := 0, property := (_ : NormedAddGroupHom.NormNoninc 0) } }

@[simp]

theorem SemiNormedGroupCat₁.zero_apply {V : SemiNormedGroupCat₁} {W : SemiNormedGroupCat₁} (x : ↑V) : 0 x = 0

instance SemiNormedGroupCat₁.instHasZeroMorphismsSemiNormedGroupCat₁InstLargeCategorySemiNormedGroupCat₁ : CategoryTheory.Limits.HasZeroMorphisms SemiNormedGroupCat₁

Equations

• SemiNormedGroupCat₁.instHasZeroMorphismsSemiNormedGroupCat₁InstLargeCategorySemiNormedGroupCat₁ = CategoryTheory.Limits.HasZeroMorphisms.mk

theorem SemiNormedGroupCat₁.isZero_of_subsingleton (V : SemiNormedGroupCat₁) [Subsingleton ↑V] : CategoryTheory.Limits.IsZero V

instance SemiNormedGroupCat₁.hasZeroObject : CategoryTheory.Limits.HasZeroObject SemiNormedGroupCat₁

Equations

• SemiNormedGroupCat₁.hasZeroObject = (_ : CategoryTheory.Limits.HasZeroObject SemiNormedGroupCat₁)

theorem SemiNormedGroupCat₁.iso_isometry {V : SemiNormedGroupCat₁} {W : SemiNormedGroupCat₁} (i : V ≅ W) : Isometry ⇑i.hom