The category of seminormed groups #
We define SemiNormedGroup
, the category of seminormed groups and normed group homs between them,
as well as SemiNormedGroup₁
, the subcategory of norm non-increasing morphisms.
The category of seminormed abelian groups and bounded group homomorphisms.
Instances for SemiNormedGroup
- SemiNormedGroup.large_category
- SemiNormedGroup.concrete_category
- SemiNormedGroup.has_coe_to_sort
- SemiNormedGroup.inhabited
- SemiNormedGroup.category_theory.limits.has_zero_morphisms
- SemiNormedGroup.has_zero_object
- SemiNormedGroup₁.SemiNormedGroup.category_theory.has_forget₂
- SemiNormedGroup.category_theory.limits.has_equalizers
- SemiNormedGroup.category_theory.limits.has_cokernels
- SemiNormedGroup.category_theory.preadditive
@[protected, instance]
Equations
- SemiNormedGroup.bundled_hom = {to_fun := normed_add_group_hom.to_fun, id := normed_add_group_hom.id, comp := normed_add_group_hom.comp, hom_ext := normed_add_group_hom.coe_inj, id_to_fun := SemiNormedGroup.bundled_hom._proof_1, comp_to_fun := SemiNormedGroup.bundled_hom._proof_2}
@[protected, instance]
@[protected, instance]
@[protected, instance]
Construct a bundled SemiNormedGroup
from the underlying type and typeclass.
Equations
Instances for ↥SemiNormedGroup.of
@[protected, instance]
Equations
@[simp]
theorem
SemiNormedGroup.coe_of
(V : Type u)
[seminormed_add_comm_group V] :
↥(SemiNormedGroup.of V) = V
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
- SemiNormedGroup.category_theory.limits.has_zero_morphisms = {has_zero := λ (X Y : SemiNormedGroup), normed_add_group_hom.has_zero, comp_zero' := SemiNormedGroup.category_theory.limits.has_zero_morphisms._proof_1, zero_comp' := SemiNormedGroup.category_theory.limits.has_zero_morphisms._proof_2}
@[protected, instance]
theorem
SemiNormedGroup.iso_isometry_of_norm_noninc
{V W : SemiNormedGroup}
(i : V ≅ W)
(h1 : normed_add_group_hom.norm_noninc i.hom)
(h2 : normed_add_group_hom.norm_noninc i.inv) :
SemiNormedGroup₁
is a type synonym for SemiNormedGroup
,
which we shall equip with the category structure consisting only of the norm non-increasing maps.
Instances for SemiNormedGroup₁
- SemiNormedGroup₁.has_coe_to_sort
- SemiNormedGroup₁.category_theory.large_category
- SemiNormedGroup₁.category_theory.concrete_category
- SemiNormedGroup₁.SemiNormedGroup.category_theory.has_forget₂
- SemiNormedGroup₁.inhabited
- SemiNormedGroup₁.category_theory.limits.has_zero_morphisms
- SemiNormedGroup₁.has_zero_object
- SemiNormedGroup₁.category_theory.limits.has_cokernels
@[protected, instance]
@[protected, instance]
Equations
- SemiNormedGroup₁.category_theory.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : SemiNormedGroup₁), {f // f.norm_noninc}}, id := λ (X : SemiNormedGroup₁), ⟨normed_add_group_hom.id ↥X (SemiNormedGroup.seminormed_add_comm_group X), _⟩, comp := λ (X Y Z : SemiNormedGroup₁) (f : X ⟶ Y) (g : Y ⟶ Z), ⟨↑g.comp ↑f, _⟩}, id_comp' := SemiNormedGroup₁.category_theory.large_category._proof_3, comp_id' := SemiNormedGroup₁.category_theory.large_category._proof_4, assoc' := SemiNormedGroup₁.category_theory.large_category._proof_5}
@[ext]
@[protected, instance]
Equations
- SemiNormedGroup₁.category_theory.concrete_category = category_theory.concrete_category.mk {obj := λ (X : SemiNormedGroup₁), ↥X, map := λ (X Y : SemiNormedGroup₁) (f : X ⟶ Y), ⇑f, map_id' := SemiNormedGroup₁.category_theory.concrete_category._proof_1, map_comp' := SemiNormedGroup₁.category_theory.concrete_category._proof_2}
Construct a bundled SemiNormedGroup₁
from the underlying type and typeclass.
Equations
Instances for ↥SemiNormedGroup₁.of
@[protected, instance]
Equations
def
SemiNormedGroup₁.mk_hom
{M N : SemiNormedGroup}
(f : M ⟶ N)
(i : normed_add_group_hom.norm_noninc f) :
Promote a morphism in SemiNormedGroup
to a morphism in SemiNormedGroup₁
.
Equations
- SemiNormedGroup₁.mk_hom f i = ⟨f, i⟩
@[simp]
theorem
SemiNormedGroup₁.mk_hom_apply
{M N : SemiNormedGroup}
(f : M ⟶ N)
(i : normed_add_group_hom.norm_noninc f)
(x : ↥(SemiNormedGroup₁.of ↥M)) :
⇑(SemiNormedGroup₁.mk_hom f i) x = ⇑f x
@[simp]
theorem
SemiNormedGroup₁.mk_iso_inv
{M N : SemiNormedGroup}
(f : M ≅ N)
(i : normed_add_group_hom.norm_noninc f.hom)
(i' : normed_add_group_hom.norm_noninc f.inv) :
(SemiNormedGroup₁.mk_iso f i i').inv = SemiNormedGroup₁.mk_hom f.inv i'
@[simp]
theorem
SemiNormedGroup₁.mk_iso_hom
{M N : SemiNormedGroup}
(f : M ≅ N)
(i : normed_add_group_hom.norm_noninc f.hom)
(i' : normed_add_group_hom.norm_noninc f.inv) :
(SemiNormedGroup₁.mk_iso f i i').hom = SemiNormedGroup₁.mk_hom f.hom i
noncomputable
def
SemiNormedGroup₁.mk_iso
{M N : SemiNormedGroup}
(f : M ≅ N)
(i : normed_add_group_hom.norm_noninc f.hom)
(i' : normed_add_group_hom.norm_noninc f.inv) :
Promote an isomorphism in SemiNormedGroup
to an isomorphism in SemiNormedGroup₁
.
Equations
- SemiNormedGroup₁.mk_iso f i i' = {hom := SemiNormedGroup₁.mk_hom f.hom i, inv := SemiNormedGroup₁.mk_hom f.inv i', hom_inv_id' := _, inv_hom_id' := _}
@[protected, instance]
Equations
- SemiNormedGroup₁.SemiNormedGroup.category_theory.has_forget₂ = {forget₂ := {obj := λ (X : SemiNormedGroup₁), X, map := λ (X Y : SemiNormedGroup₁) (f : X ⟶ Y), f.val, map_id' := SemiNormedGroup₁.SemiNormedGroup.category_theory.has_forget₂._proof_1, map_comp' := SemiNormedGroup₁.SemiNormedGroup.category_theory.has_forget₂._proof_2}, forget_comp := SemiNormedGroup₁.SemiNormedGroup.category_theory.has_forget₂._proof_3}
@[simp]
theorem
SemiNormedGroup₁.coe_of
(V : Type u)
[seminormed_add_comm_group V] :
↥(SemiNormedGroup₁.of V) = V
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
- SemiNormedGroup₁.category_theory.limits.has_zero_morphisms = {has_zero := λ (X Y : SemiNormedGroup₁), {zero := ⟨0, _⟩}, comp_zero' := SemiNormedGroup₁.category_theory.limits.has_zero_morphisms._proof_2, zero_comp' := SemiNormedGroup₁.category_theory.limits.has_zero_morphisms._proof_3}
@[protected, instance]