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

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

instance SemiNormedGroupCat.instConcreteCategory : CategoryTheory.ConcreteCategory SemiNormedGroupCat

Equations

• SemiNormedGroupCat.instConcreteCategory = id inferInstance

instance SemiNormedGroupCat.instCoeSortType : CoeSort SemiNormedGroupCat (Type u_1)

Equations

• SemiNormedGroupCat.instCoeSortType = { 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

• M.instSeminormedAddCommGroupα = M.str

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

Equations

• SemiNormedGroupCat.funLike = { coe := (CategoryTheory.forget SemiNormedGroupCat).map, coe_injective' := ⋯ }

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

Equations

• ⋯ = ⋯

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.instInhabited : Inhabited SemiNormedGroupCat

Equations

• SemiNormedGroupCat.instInhabited = { 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.instZeroHom {M : SemiNormedGroupCat} {N : SemiNormedGroupCat} : Zero (M ⟶ N)

Equations

• SemiNormedGroupCat.instZeroHom = NormedAddGroupHom.zero

@[simp]

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

instance SemiNormedGroupCat.instHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms SemiNormedGroupCat

Equations

• SemiNormedGroupCat.instHasZeroMorphisms = CategoryTheory.Limits.HasZeroMorphisms.mk (@SemiNormedGroupCat.instHasZeroMorphisms.proof_1) SemiNormedGroupCat.instHasZeroMorphisms.proof_2

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

instance SemiNormedGroupCat.hasZeroObject : CategoryTheory.Limits.HasZeroObject SemiNormedGroupCat

Equations

• SemiNormedGroupCat.hasZeroObject = ⋯

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₁.instCoeSortType : CoeSort SemiNormedGroupCat₁ (Type u_1)

Equations

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

instance SemiNormedGroupCat₁.instLargeCategory : CategoryTheory.LargeCategory SemiNormedGroupCat₁

Equations

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

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

Equations

• X.instFunLike Y = { coe := fun (f : X ⟶ Y) => (↑f).toFun, coe_injective' := ⋯ }

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

instance SemiNormedGroupCat₁.instConcreteCategory : 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

• ⋯ = ⋯

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

• M.instSeminormedAddCommGroupα = 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 = ⟨f, 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_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

@[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'

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' = { hom := SemiNormedGroupCat₁.mkHom f.hom i, inv := SemiNormedGroupCat₁.mkHom f.inv i', hom_inv_id := ⋯, inv_hom_id := ⋯ }

instance SemiNormedGroupCat₁.instHasForget₂SemiNormedGroupCat : 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₁.instInhabited : Inhabited SemiNormedGroupCat₁

Equations

• SemiNormedGroupCat₁.instInhabited = { 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₁.instZeroHom (X : SemiNormedGroupCat₁) (Y : SemiNormedGroupCat₁) : Zero (X ⟶ Y)

Equations

• X.instZeroHom Y = { zero := ⟨0, ⋯⟩ }

@[simp]

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

instance SemiNormedGroupCat₁.instHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms SemiNormedGroupCat₁

Equations

• SemiNormedGroupCat₁.instHasZeroMorphisms = CategoryTheory.Limits.HasZeroMorphisms.mk (@SemiNormedGroupCat₁.instHasZeroMorphisms.proof_1) SemiNormedGroupCat₁.instHasZeroMorphisms.proof_2

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

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

Equations

• SemiNormedGroupCat₁.hasZeroObject = ⋯

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