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.
The category of seminormed abelian groups and bounded group homomorphisms.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- SemiNormedGrp.instConcreteCategory = id inferInstance
Equations
- SemiNormedGrp.instCoeSortType = { coe := fun (X : SemiNormedGrp) => ↑X }
Equations
- M.instSeminormedAddCommGroupα = M.str
Equations
- SemiNormedGrp.funLike = { coe := (CategoryTheory.forget SemiNormedGrp).map, coe_injective' := ⋯ }
instance
SemiNormedGrp.toAddMonoidHomClass
{V : SemiNormedGrp}
{W : SemiNormedGrp}
:
AddMonoidHomClass (V ⟶ W) ↑V ↑W
Equations
- ⋯ = ⋯
theorem
SemiNormedGrp.ext
{M : SemiNormedGrp}
{N : SemiNormedGrp}
{f₁ : M ⟶ N}
{f₂ : M ⟶ N}
(h : ∀ (x : ↑M), f₁ x = f₂ x)
:
f₁ = f₂
@[simp]
@[simp]
@[simp]
theorem
SemiNormedGrp.coe_comp
{M : SemiNormedGrp}
{N : SemiNormedGrp}
{K : SemiNormedGrp}
(f : M ⟶ N)
(g : N ⟶ K)
:
⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f
Equations
- SemiNormedGrp.instInhabited = { default := SemiNormedGrp.of PUnit.{u_1 + 1} }
instance
SemiNormedGrp.ofUnique
(V : Type u)
[SeminormedAddCommGroup V]
[i : Unique V]
:
Unique ↑(SemiNormedGrp.of V)
Equations
Equations
- SemiNormedGrp.instZeroHom = NormedAddGroupHom.zero
@[simp]
theorem
SemiNormedGrp.iso_isometry_of_normNoninc
{V : SemiNormedGrp}
{W : SemiNormedGrp}
(i : V ≅ W)
(h1 : NormedAddGroupHom.NormNoninc i.hom)
(h2 : NormedAddGroupHom.NormNoninc i.inv)
:
Isometry ⇑i.hom
SemiNormedGrp₁
is a type synonym for SemiNormedGrp
,
which we shall equip with the category structure consisting only of the norm non-increasing maps.
Instances For
Equations
- SemiNormedGrp₁.instCoeSortType = { coe := fun (X : SemiNormedGrp₁) => ↑X }
theorem
SemiNormedGrp₁.hom_ext
{M : SemiNormedGrp₁}
{N : SemiNormedGrp₁}
(f : M ⟶ N)
(g : M ⟶ N)
(w : ⇑f = ⇑g)
:
f = g
Equations
- One or more equations did not get rendered due to their size.
instance
SemiNormedGrp₁.toAddMonoidHomClass
{V : SemiNormedGrp₁}
{W : SemiNormedGrp₁}
:
AddMonoidHomClass (V ⟶ W) ↑V ↑W
Equations
- ⋯ = ⋯
Equations
- M.instSeminormedAddCommGroupα = M.str
def
SemiNormedGrp₁.mkHom
{M : SemiNormedGrp}
{N : SemiNormedGrp}
(f : M ⟶ N)
(i : NormedAddGroupHom.NormNoninc f)
:
Promote a morphism in SemiNormedGrp
to a morphism in SemiNormedGrp₁
.
Equations
- SemiNormedGrp₁.mkHom f i = ⟨f, i⟩
Instances For
theorem
SemiNormedGrp₁.mkHom_apply
{M : SemiNormedGrp}
{N : SemiNormedGrp}
(f : M ⟶ N)
(i : NormedAddGroupHom.NormNoninc f)
(x : ↑(SemiNormedGrp₁.of ↑M))
:
(SemiNormedGrp₁.mkHom f i) x = f x
@[simp]
theorem
SemiNormedGrp₁.mkIso_hom
{M : SemiNormedGrp}
{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
@[simp]
theorem
SemiNormedGrp₁.mkIso_inv
{M : SemiNormedGrp}
{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'
def
SemiNormedGrp₁.mkIso
{M : SemiNormedGrp}
{N : SemiNormedGrp}
(f : M ≅ N)
(i : NormedAddGroupHom.NormNoninc f.hom)
(i' : NormedAddGroupHom.NormNoninc f.inv)
:
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 := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
@[simp]
theorem
SemiNormedGrp₁.coe_comp
{M : SemiNormedGrp₁}
{N : SemiNormedGrp₁}
{K : SemiNormedGrp₁}
(f : M ⟶ N)
(g : N ⟶ K)
:
⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f
Equations
- SemiNormedGrp₁.instInhabited = { default := SemiNormedGrp₁.of PUnit.{u_1 + 1} }
instance
SemiNormedGrp₁.ofUnique
(V : Type u)
[SeminormedAddCommGroup V]
[i : Unique V]
:
Unique ↑(SemiNormedGrp₁.of V)
Equations
Equations
- X.instZeroHom Y = { zero := ⟨0, ⋯⟩ }
@[simp]
theorem
SemiNormedGrp₁.iso_isometry
{V : SemiNormedGrp₁}
{W : SemiNormedGrp₁}
(i : V ≅ W)
:
Isometry ⇑i.hom