The category of seminormed groups

We define SemiNormedGrp, the category of seminormed groups and normed group homs between them, as well as SemiNormedGrp₁, the subcategory of norm non-increasing morphisms.

def SemiNormedGrp : Type (u + 1)

The category of seminormed abelian groups and bounded group homomorphisms.

Equations

• SemiNormedGrp = CategoryTheory.Bundled SeminormedAddCommGroup

instance SemiNormedGrp.bundledHom : CategoryTheory.BundledHom NormedAddGroupHom

Equations

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

instance instSemiNormedGrpLargeCategory : CategoryTheory.LargeCategory SemiNormedGrp

Equations

• instSemiNormedGrpLargeCategory = CategoryTheory.BundledHom.category NormedAddGroupHom

instance SemiNormedGrp.instConcreteCategory : CategoryTheory.ConcreteCategory SemiNormedGrp

Equations

• SemiNormedGrp.instConcreteCategory = id inferInstance

instance SemiNormedGrp.instCoeSortType : CoeSort SemiNormedGrp (Type u_1)

Equations

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

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

Construct a bundled SemiNormedGrp from the underlying type and typeclass.

Equations

• SemiNormedGrp.of M = CategoryTheory.Bundled.of M

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

Equations

• M.instSeminormedAddCommGroupα = M.str

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

Equations

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

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

Equations

• ⋯ = ⋯

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

@[simp]

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

@[simp]

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

@[simp]

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

instance SemiNormedGrp.instInhabited : Inhabited SemiNormedGrp

Equations

• SemiNormedGrp.instInhabited = { default := SemiNormedGrp.of PUnit.{?u.3 + 1} }

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

Equations

• SemiNormedGrp.ofUnique V = i

instance SemiNormedGrp.instZeroHom {M N : SemiNormedGrp} : Zero (M ⟶ N)

Equations

• SemiNormedGrp.instZeroHom = NormedAddGroupHom.zero

@[simp]

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

instance SemiNormedGrp.instHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms SemiNormedGrp

Equations

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

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

instance SemiNormedGrp.hasZeroObject : CategoryTheory.Limits.HasZeroObject SemiNormedGrp

Equations

• SemiNormedGrp.hasZeroObject = ⋯

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

def SemiNormedGrp₁ : Type (u + 1)

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

Equations

• SemiNormedGrp₁ = CategoryTheory.Bundled SeminormedAddCommGroup

instance SemiNormedGrp₁.instCoeSortType : CoeSort SemiNormedGrp₁ (Type u_1)

Equations

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

instance SemiNormedGrp₁.instLargeCategory : CategoryTheory.LargeCategory SemiNormedGrp₁

Equations

• SemiNormedGrp₁.instLargeCategory = CategoryTheory.Category.mk @SemiNormedGrp₁.instLargeCategory.proof_3 @SemiNormedGrp₁.instLargeCategory.proof_4 @SemiNormedGrp₁.instLargeCategory.proof_5

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

Equations

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

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

instance SemiNormedGrp₁.instConcreteCategory : CategoryTheory.ConcreteCategory SemiNormedGrp₁

Equations

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

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

Equations

• ⋯ = ⋯

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

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

Equations

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

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

Equations

• M.instSeminormedAddCommGroupα = M.str

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

Promote a morphism in SemiNormedGrp to a morphism in SemiNormedGrp₁.

Equations

• SemiNormedGrp₁.mkHom f i = ⟨f, i⟩

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

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

Promote an isomorphism in SemiNormedGrp to an isomorphism in SemiNormedGrp₁.

Equations

• SemiNormedGrp₁.mkIso f i i' = { hom := SemiNormedGrp₁.mkHom f.hom i, inv := SemiNormedGrp₁.mkHom f.inv i', hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

instance SemiNormedGrp₁.instHasForget₂SemiNormedGrp : CategoryTheory.HasForget₂ SemiNormedGrp₁ SemiNormedGrp

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

instance SemiNormedGrp₁.instInhabited : Inhabited SemiNormedGrp₁

Equations

• SemiNormedGrp₁.instInhabited = { default := SemiNormedGrp₁.of PUnit.{?u.3 + 1} }

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

Equations

• SemiNormedGrp₁.ofUnique V = i

instance SemiNormedGrp₁.instZeroHom (X Y : SemiNormedGrp₁) : Zero (X ⟶ Y)

Equations

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

@[simp]

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

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

Equations

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

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

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

Equations

• SemiNormedGrp₁.hasZeroObject = ⋯

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