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.

source

def SemiNormedGroupCat :

Type (u + 1)

The category of seminormed abelian groups and bounded group homomorphisms.

Instances For

source

instance SemiNormedGroupCat.bundledHom :

CategoryTheory.BundledHom NormedAddGroupHom

source

instance SemiNormedGroupCat.instConcreteCategorySemiNormedGroupCatInstSemiNormedGroupCatLargeCategory :

CategoryTheory.ConcreteCategory SemiNormedGroupCat

source

instance SemiNormedGroupCat.instCoeSortSemiNormedGroupCatType :

CoeSort SemiNormedGroupCat (Type u_1)

source

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

SemiNormedGroupCat

Construct a bundled SemiNormedGroupCat from the underlying type and typeclass.

Instances For

source

instance SemiNormedGroupCat.instSeminormedAddCommGroupα (M : SemiNormedGroupCat) :

SeminormedAddCommGroup ↑M

source

instance SemiNormedGroupCat.toAddMonoidHomClass {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} :

AddMonoidHomClass (V ⟶ W) ↑V ↑W

source

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

f₁ = f₂

source

@[simp]

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

↑(SemiNormedGroupCat.of V) = V

source

@[simp]

theorem SemiNormedGroupCat.coe_id (V : SemiNormedGroupCat) :

↑(CategoryTheory.CategoryStruct.id V) = id

source

@[simp]

theorem SemiNormedGroupCat.coe_comp {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} {K : SemiNormedGroupCat} (f : M ⟶ N) (g : N ⟶ K) :

↑(CategoryTheory.CategoryStruct.comp f g) = ↑g ∘ ↑f

source

instance SemiNormedGroupCat.instInhabitedSemiNormedGroupCat :

Inhabited SemiNormedGroupCat

source

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

Unique ↑(SemiNormedGroupCat.of V)

source

instance SemiNormedGroupCat.instZeroHomSemiNormedGroupCatToQuiverToCategoryStructInstSemiNormedGroupCatLargeCategory {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} :

Zero (M ⟶ N)

source

@[simp]

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

↑0 x = 0

source

instance SemiNormedGroupCat.instHasZeroMorphismsSemiNormedGroupCatInstSemiNormedGroupCatLargeCategory :

CategoryTheory.Limits.HasZeroMorphisms SemiNormedGroupCat

source

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

CategoryTheory.Limits.IsZero V

source

instance SemiNormedGroupCat.hasZeroObject :

CategoryTheory.Limits.HasZeroObject SemiNormedGroupCat

source

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

source

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.

Instances For

source

instance SemiNormedGroupCat₁.instCoeSortSemiNormedGroupCat₁Type :

CoeSort SemiNormedGroupCat₁ (Type u_1)

source

instance SemiNormedGroupCat₁.instLargeCategorySemiNormedGroupCat₁ :

CategoryTheory.LargeCategory SemiNormedGroupCat₁

source

instance SemiNormedGroupCat₁.instFunLike (X : SemiNormedGroupCat₁) (Y : SemiNormedGroupCat₁) :

FunLike (X ⟶ Y) ↑X fun x => ↑Y

source