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.instCoeSortType = { coe := fun (X : SemiNormedGrp) => ↑X }
Construct a bundled SemiNormedGrp
from the underlying type and typeclass.
Instances For
Equations
- SemiNormedGrp.funLike = { coe := (CategoryTheory.forget SemiNormedGrp).map, coe_injective' := ⋯ }
Equations
- SemiNormedGrp.instInhabited = { default := SemiNormedGrp.of PUnit.{?u.3 + 1} }
theorem
SemiNormedGrp.iso_isometry_of_normNoninc
{V W : SemiNormedGrp}
(i : V ≅ W)
(h1 : NormedAddGroupHom.NormNoninc i.hom)
(h2 : NormedAddGroupHom.NormNoninc i.inv)
:
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 }
Equations
- X.instFunLike Y = { coe := fun (f : X ⟶ Y) => (↑f).toFun, coe_injective' := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Construct a bundled SemiNormedGrp₁
from the underlying type and typeclass.
Instances For
Promote a morphism in SemiNormedGrp
to a morphism in SemiNormedGrp₁
.
Instances For
theorem
SemiNormedGrp₁.mkHom_apply
{M N : SemiNormedGrp}
(f : M ⟶ N)
(i : NormedAddGroupHom.NormNoninc f)
(x : ↑(of ↑M))
:
def
SemiNormedGrp₁.mkIso
{M 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
@[simp]
theorem
SemiNormedGrp₁.mkIso_hom
{M N : SemiNormedGrp}
(f : M ≅ N)
(i : NormedAddGroupHom.NormNoninc f.hom)
(i' : NormedAddGroupHom.NormNoninc f.inv)
:
@[simp]
theorem
SemiNormedGrp₁.mkIso_inv
{M N : SemiNormedGrp}
(f : M ≅ N)
(i : NormedAddGroupHom.NormNoninc f.hom)
(i' : NormedAddGroupHom.NormNoninc f.inv)
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- SemiNormedGrp₁.instInhabited = { default := SemiNormedGrp₁.of PUnit.{?u.3 + 1} }
Equations
- X.instZeroHom Y = { zero := ⟨0, ⋯⟩ }