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.

• of :: (
• carrier : Type u

  The underlying seminormed abelian group.

• str : SeminormedAddCommGroup self.carrier
• )

instance SemiNormedGrp.instCoeSortType : CoeSort SemiNormedGrp (Type u_1)

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_iff {M N : SemiNormedGrp} {x y : M.Hom N} : x = y ↔ x.hom' = y.hom'

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

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

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

@[reducible, inline]

abbrev SemiNormedGrp.ofHom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) : { carrier := M, str := inst✝ } ⟶ { carrier := N, str := inst✝¹ }

Typecheck a NormedAddGroupHom as a morphism in SemiNormedGrp.

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.

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₂

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

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

theorem SemiNormedGrp.hom_ext_iff {M N : SemiNormedGrp} {f g : M ⟶ N} : f = g ↔ Hom.hom f = Hom.hom 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 { carrier := M, str := inst✝ }

@[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] : { carrier := V, str := inst✝ }.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

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

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

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)

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

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

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

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

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

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.

• of :: (
• carrier : Type u

  The underlying seminormed abelian group.

• str : SeminormedAddCommGroup self.carrier
• )

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

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_iff {M N : SemiNormedGrp₁} {x y : M.Hom N} : x = y ↔ x.hom' = y.hom'

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₁

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

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

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.

@[reducible, inline]

abbrev SemiNormedGrp₁.mkHom {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (i : f.NormNoninc) : { carrier := M, str := inst✝ } ⟶ { carrier := N, str := inst✝¹ }

Promote a NormedAddGroupHom to a morphism in SemiNormedGrp₁.

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.

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

theorem SemiNormedGrp₁.mkHom_apply {M N : Type u} [SeminormedAddCommGroup M] [SeminormedAddCommGroup N] (f : NormedAddGroupHom M N) (i : f.NormNoninc) (x : { carrier := M, str := inst✝ }.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₂

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

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

theorem SemiNormedGrp₁.hom_ext_iff {M N : SemiNormedGrp₁} {f g : M ⟶ N} : f = g ↔ Hom.hom f = Hom.hom 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 { carrier := M, str := inst✝ }

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

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

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

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

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

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

theorem SemiNormedGrp₁.coe_of (V : Type u) [SeminormedAddCommGroup V] : { carrier := V, str := inst✝ }.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₁

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

@[simp]

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

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

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)