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.

structure SemiNormedGrp : Type (u + 1)

The category of seminormed abelian groups and bounded group homomorphisms.

• carrier : Type u

  The underlying seminormed abelian group.

• str : SeminormedAddCommGroup self.carrier

instance SemiNormedGrp.instCoeSortType : CoeSort SemiNormedGrp (Type u_1)

Equations

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

@[reducible, inline]

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

Construct a bundled SemiNormedGrp from the underlying type and typeclass.

Equations

• SemiNormedGrp.of M = SemiNormedGrp.mk M

structure SemiNormedGrp.Hom (M N : SemiNormedGrp) : Type u

The type of morphisms in SemiNormedGrp

• hom' : NormedAddGroupHom M.carrier N.carrier

  The underlying NormedAddGroupHom.

theorem SemiNormedGrp.Hom.ext {M N : SemiNormedGrp} {x y : M.Hom N} (hom' : x.hom' = y.hom') : x = y

instance SemiNormedGrp.instLargeCategory : CategoryTheory.LargeCategory SemiNormedGrp

Equations

• SemiNormedGrp.instLargeCategory = CategoryTheory.Category.mk @SemiNormedGrp.instLargeCategory.proof_1 @SemiNormedGrp.instLargeCategory.proof_2 @SemiNormedGrp.instLargeCategory.proof_3

instance SemiNormedGrp.instConcreteCategoryNormedAddGroupHomCarrier : CategoryTheory.ConcreteCategory SemiNormedGrp fun (x1 x2 : SemiNormedGrp) => NormedAddGroupHom x1.carrier x2.carrier

Equations

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

@[reducible, inline]

abbrev SemiNormedGrp.Hom.hom {M N : SemiNormedGrp} (f : M.Hom N) : NormedAddGroupHom M.carrier N.carrier

Turn a morphism in SemiNormedGrp back into a NormedAddGroupHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev SemiNormedGrp.ofHom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) : of M ⟶ of N

Typecheck a NormedAddGroupHom as a morphism in SemiNormedGrp.

Equations

• SemiNormedGrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def SemiNormedGrp.Hom.Simps.hom (M N : SemiNormedGrp) (f : M.Hom N) : NormedAddGroupHom M.carrier N.carrier

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• SemiNormedGrp.Hom.Simps.hom M N f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

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

@[simp]

theorem SemiNormedGrp.hom_id {M : SemiNormedGrp} : Hom.hom (CategoryTheory.CategoryStruct.id M) = NormedAddGroupHom.id M.carrier

theorem SemiNormedGrp.id_apply (M : SemiNormedGrp) (r : M.carrier) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) r = r

@[simp]

theorem SemiNormedGrp.hom_comp {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem SemiNormedGrp.comp_apply {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O) (r : M.carrier) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) r = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) r)

theorem SemiNormedGrp.hom_ext {M N : SemiNormedGrp} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

@[simp]

theorem SemiNormedGrp.hom_ofHom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) : Hom.hom (ofHom f) = f

@[simp]

theorem SemiNormedGrp.ofHom_hom {M N : SemiNormedGrp} (f : M ⟶ N) : ofHom (Hom.hom f) = f

@[simp]

theorem SemiNormedGrp.ofHom_id {M : Type u} [SeminormedAddCommGroup M] : ofHom (NormedAddGroupHom.id M) = CategoryTheory.CategoryStruct.id (of M)

@[simp]

theorem SemiNormedGrp.ofHom_comp {M N O : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] [SeminormedAddCommGroup O] (f : NormedAddGroupHom M N) (g : NormedAddGroupHom N O) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem SemiNormedGrp.ofHom_apply {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (r : M) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) r = f r

theorem SemiNormedGrp.inv_hom_apply {M N : SemiNormedGrp} (e : M ≅ N) (r : M.carrier) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) r) = r

theorem SemiNormedGrp.hom_inv_apply {M N : SemiNormedGrp} (e : M ≅ N) (s : N.carrier) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

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

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

theorem SemiNormedGrp.coe_comp {M N K : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ K) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom 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 (of V).carrier

Equations

• SemiNormedGrp.ofUnique V = i

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

Equations

• SemiNormedGrp.instZeroHom = { zero := SemiNormedGrp.ofHom 0 }

@[simp]

theorem SemiNormedGrp.hom_zero {V W : SemiNormedGrp} : Hom.hom 0 = 0

theorem SemiNormedGrp.zero_apply {V W : SemiNormedGrp} (x : V.carrier) : (CategoryTheory.ConcreteCategory.hom 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.carrier] : CategoryTheory.Limits.IsZero V

instance SemiNormedGrp.hasZeroObject : CategoryTheory.Limits.HasZeroObject SemiNormedGrp

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

instance SemiNormedGrp.Hom.add {M N : SemiNormedGrp} : Add (M ⟶ N)

Equations

• SemiNormedGrp.Hom.add = { add := fun (f g : M ⟶ N) => SemiNormedGrp.ofHom (SemiNormedGrp.Hom.hom f + SemiNormedGrp.Hom.hom g) }

@[simp]

theorem SemiNormedGrp.hom_add {V W : SemiNormedGrp} (f g : V ⟶ W) : Hom.hom (f + g) = Hom.hom f + Hom.hom g

instance SemiNormedGrp.Hom.neg {M N : SemiNormedGrp} : Neg (M ⟶ N)

Equations

• SemiNormedGrp.Hom.neg = { neg := fun (f : M ⟶ N) => SemiNormedGrp.ofHom (-SemiNormedGrp.Hom.hom f) }

@[simp]

theorem SemiNormedGrp.hom_neg {V W : SemiNormedGrp} (f : V ⟶ W) : Hom.hom (-f) = -Hom.hom f

instance SemiNormedGrp.Hom.sub {M N : SemiNormedGrp} : Sub (M ⟶ N)

Equations

• SemiNormedGrp.Hom.sub = { sub := fun (f g : M ⟶ N) => SemiNormedGrp.ofHom (SemiNormedGrp.Hom.hom f - SemiNormedGrp.Hom.hom g) }

@[simp]

theorem SemiNormedGrp.hom_sub {V W : SemiNormedGrp} (f g : V ⟶ W) : Hom.hom (f - g) = Hom.hom f - Hom.hom g

instance SemiNormedGrp.Hom.nsmul {M N : SemiNormedGrp} : SMul ℕ (M ⟶ N)

Equations

• SemiNormedGrp.Hom.nsmul = { smul := fun (n : ℕ) (f : M ⟶ N) => SemiNormedGrp.ofHom (n • SemiNormedGrp.Hom.hom f) }

@[simp]

theorem SemiNormedGrp.hom_nsum {V W : SemiNormedGrp} (n : ℕ) (f : V ⟶ W) : Hom.hom (n • f) = n • Hom.hom f

instance SemiNormedGrp.Hom.zsmul {M N : SemiNormedGrp} : SMul ℤ (M ⟶ N)

Equations

• SemiNormedGrp.Hom.zsmul = { smul := fun (n : ℤ) (f : M ⟶ N) => SemiNormedGrp.ofHom (n • SemiNormedGrp.Hom.hom f) }

@[simp]

theorem SemiNormedGrp.hom_zsum {V W : SemiNormedGrp} (n : ℤ) (f : V ⟶ W) : Hom.hom (n • f) = n • Hom.hom f

instance SemiNormedGrp.Hom.addCommGroup {V W : SemiNormedGrp} : AddCommGroup (V ⟶ W)

Equations

• SemiNormedGrp.Hom.addCommGroup = Function.Injective.addCommGroup CategoryTheory.ConcreteCategory.hom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

structure 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.

• carrier : Type u

  The underlying seminormed abelian group.

• str : SeminormedAddCommGroup self.carrier

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

Equations

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

@[reducible, inline]

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

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

Equations

• SemiNormedGrp₁.of M = SemiNormedGrp₁.mk M

structure SemiNormedGrp₁.Hom (M N : SemiNormedGrp₁) : Type u

The type of morphisms in SemiNormedGrp₁

• hom' : NormedAddGroupHom M.carrier N.carrier

  The underlying NormedAddGroupHom.

• normNoninc : self.hom'.NormNoninc

theorem SemiNormedGrp₁.Hom.ext {M N : SemiNormedGrp₁} {x y : M.Hom N} (hom' : x.hom' = y.hom') : x = y

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 : SemiNormedGrp₁) (Y : SemiNormedGrp₁) : FunLike { f : NormedAddGroupHom X.carrier Y.carrier // f.NormNoninc } X.carrier Y.carrier

Equations

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

instance SemiNormedGrp₁.instConcreteCategorySubtypeNormedAddGroupHomCarrierNormNoninc : CategoryTheory.ConcreteCategory SemiNormedGrp₁ fun (X Y : SemiNormedGrp₁) => { f : NormedAddGroupHom X.carrier Y.carrier // f.NormNoninc }

Equations

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

instance SemiNormedGrp₁.instAddMonoidHomClassSubtypeNormedAddGroupHomCarrierNormNoninc (X : SemiNormedGrp₁) (Y : SemiNormedGrp₁) : AddMonoidHomClass { f : NormedAddGroupHom X.carrier Y.carrier // f.NormNoninc } X.carrier Y.carrier

@[reducible, inline]

abbrev SemiNormedGrp₁.Hom.hom {M N : SemiNormedGrp₁} (f : M.Hom N) : { f : NormedAddGroupHom M.carrier N.carrier // f.NormNoninc }

Turn a morphism in SemiNormedGrp₁ back into a norm-nonincreasing NormedAddGroupHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev SemiNormedGrp₁.mkHom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (i : f.NormNoninc) : of M ⟶ of N

Promote a NormedAddGroupHom to a morphism in SemiNormedGrp₁.

Equations

• SemiNormedGrp₁.mkHom f i = CategoryTheory.ConcreteCategory.ofHom ⟨f, i⟩

def SemiNormedGrp₁.Hom.Simps.hom (M N : SemiNormedGrp₁) (f : M.Hom N) : NormedAddGroupHom M.carrier N.carrier

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• SemiNormedGrp₁.Hom.Simps.hom M N f = ↑f.hom

instance SemiNormedGrp₁.instCoeFunHomForallCarrier (X Y : SemiNormedGrp₁) : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => X.carrier → Y.carrier

Equations

• X.instCoeFunHomForallCarrier Y = { coe := fun (f : X ⟶ Y) => ⇑↑(SemiNormedGrp₁.Hom.hom f) }

theorem SemiNormedGrp₁.mkHom_apply {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (i : f.NormNoninc) (x : (of M).carrier) : ↑(Hom.hom (mkHom f i)) x = f x

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

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

@[simp]

theorem SemiNormedGrp₁.hom_id {M : SemiNormedGrp₁} : ↑(Hom.hom (CategoryTheory.CategoryStruct.id M)) = NormedAddGroupHom.id M.carrier

theorem SemiNormedGrp₁.id_apply (M : SemiNormedGrp₁) (r : M.carrier) : ↑(Hom.hom (CategoryTheory.CategoryStruct.id M)) r = r

@[simp]

theorem SemiNormedGrp₁.hom_comp {M N O : SemiNormedGrp₁} (f : M ⟶ N) (g : N ⟶ O) : ↑(Hom.hom (CategoryTheory.CategoryStruct.comp f g)) = (↑(Hom.hom g)).comp ↑(Hom.hom f)

theorem SemiNormedGrp₁.comp_apply {M N O : SemiNormedGrp₁} (f : M ⟶ N) (g : N ⟶ O) (r : M.carrier) : ↑(Hom.hom (CategoryTheory.CategoryStruct.comp f g)) r = ↑(Hom.hom g) (↑(Hom.hom f) r)

theorem SemiNormedGrp₁.hom_ext {M N : SemiNormedGrp₁} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) : f = g

@[simp]

theorem SemiNormedGrp₁.hom_mkHom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (hf : f.NormNoninc) : ↑(Hom.hom (mkHom f hf)) = f

@[simp]

theorem SemiNormedGrp₁.mkHom_hom {M N : SemiNormedGrp₁} (f : M ⟶ N) : mkHom ↑(Hom.hom f) ⋯ = f

@[simp]

theorem SemiNormedGrp₁.mkHom_id {M : Type u} [SeminormedAddCommGroup M] : mkHom (NormedAddGroupHom.id M) ⋯ = CategoryTheory.CategoryStruct.id (of M)

@[simp]

theorem SemiNormedGrp₁.mkHom_comp {M N O : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] [SeminormedAddCommGroup O] (f : NormedAddGroupHom M N) (g : NormedAddGroupHom N O) (hf : f.NormNoninc) (hg : g.NormNoninc) (hgf : (g.comp f).NormNoninc) : mkHom (g.comp f) hgf = CategoryTheory.CategoryStruct.comp (mkHom f hf) (mkHom g hg)

@[simp]

theorem SemiNormedGrp₁.inv_hom_apply {M N : SemiNormedGrp₁} (e : M ≅ N) (r : M.carrier) : ↑(Hom.hom e.inv) (↑(Hom.hom e.hom) r) = r

@[simp]

theorem SemiNormedGrp₁.hom_inv_apply {M N : SemiNormedGrp₁} (e : M ≅ N) (s : N.carrier) : ↑(Hom.hom e.hom) (↑(Hom.hom e.inv) s) = s

instance SemiNormedGrp₁.instSeminormedAddCommGroupCarrier (M : SemiNormedGrp₁) : SeminormedAddCommGroup M.carrier

Equations

• M.instSeminormedAddCommGroupCarrier = M.str

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

theorem SemiNormedGrp₁.coe_comp {M N K : SemiNormedGrp₁} (f : M ⟶ N) (g : N ⟶ K) : ⇑↑(Hom.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑↑(Hom.hom g) ∘ ⇑↑(Hom.hom 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 (of V).carrier

Equations

• SemiNormedGrp₁.ofUnique V = i

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

Equations

• X.instZeroHom Y = { zero := { hom' := 0, normNoninc := ⋯ } }

@[simp]

theorem SemiNormedGrp₁.zero_apply {V W : SemiNormedGrp₁} (x : V.carrier) : ↑(Hom.hom 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.carrier] : CategoryTheory.Limits.IsZero V

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

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