analysis.normed.group.SemiNormedGroup

SemiNormedGroup₁ is a type synonym for SemiNormedGroup, which we shall equip with the category structure consisting only of the norm non-increasing maps.

Equations

SemiNormedGroup₁ = category_theory.bundled seminormed_add_comm_group

Instances for SemiNormedGroup₁

source

@[protected, instance]

def SemiNormedGroup₁.has_coe_to_sort :

has_coe_to_sort SemiNormedGroup₁ (Type u)

Equations

SemiNormedGroup₁.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

@[protected, instance]

noncomputable def SemiNormedGroup₁.category_theory.large_category :

category_theory.large_category SemiNormedGroup₁

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}

source

@[ext]

theorem SemiNormedGroup₁.hom_ext {M N : SemiNormedGroup₁} (f g : M ⟶ N) (w : ⇑f = ⇑g) :

f = g

source

@[protected, instance]

def SemiNormedGroup₁.category_theory.concrete_category :

category_theory.concrete_category SemiNormedGroup₁

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}

source

def SemiNormedGroup₁.of (M : Type u) [seminormed_add_comm_group M] :

SemiNormedGroup₁

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

Equations

SemiNormedGroup₁.of M = category_theory.bundled.of M

Instances for ↥SemiNormedGroup₁.of

SemiNormedGroup₁.of_unique

source

@[protected, instance]

def SemiNormedGroup₁.seminormed_add_comm_group (M : SemiNormedGroup₁) :

seminormed_add_comm_group ↥M

Equations

M.seminormed_add_comm_group = M.str

source

def SemiNormedGroup₁.mk_hom {M N : SemiNormedGroup} (f : M ⟶ N) (i : normed_add_group_hom.norm_noninc f) :

SemiNormedGroup₁.of ↥M ⟶ SemiNormedGroup₁.of ↥N

Promote a morphism in SemiNormedGroup to a morphism in SemiNormedGroup₁.

Equations

SemiNormedGroup₁.mk_hom f i = ⟨f, i⟩

source

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

source

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

source

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

source

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) :

SemiNormedGroup₁.of ↥M ≅ SemiNormedGroup₁.of ↥N

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' := _}

source

@[protected, instance]

def SemiNormedGroup₁.SemiNormedGroup.category_theory.has_forget₂ :

category_theory.has_forget₂ SemiNormedGroup₁ SemiNormedGroup

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}

source

@[simp]

theorem SemiNormedGroup₁.coe_of (V : Type u) [seminormed_add_comm_group V] :

↥(SemiNormedGroup₁.of V) = V

source

@[simp]

theorem SemiNormedGroup₁.coe_id (V : SemiNormedGroup₁) :

⇑(𝟙 V) = id

source

@[simp]

theorem SemiNormedGroup₁.coe_comp {M N K : SemiNormedGroup₁} (f : M ⟶ N) (g : N ⟶ K) :

⇑(f ≫ g) = ⇑g ∘ ⇑f

source

@[simp]

theorem SemiNormedGroup₁.coe_comp' {M N K : SemiNormedGroup₁} (f : M ⟶ N) (g : N ⟶ K) :

↑(f ≫ g) = ↑g.comp ↑f

source

@[protected, instance]

def SemiNormedGroup₁.inhabited :

inhabited SemiNormedGroup₁

Equations

SemiNormedGroup₁.inhabited = {default := SemiNormedGroup₁.of punit normed_add_comm_group.to_seminormed_add_comm_group}

source

@[protected, instance]

def SemiNormedGroup₁.of_unique (V : Type u) [seminormed_add_comm_group V] [i : unique V] :

unique ↥(SemiNormedGroup₁.of V)

Equations

SemiNormedGroup₁.of_unique V = i

source

@[protected, instance]

def SemiNormedGroup₁.category_theory.limits.has_zero_morphisms :

category_theory.limits.has_zero_morphisms SemiNormedGroup₁

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}

source

@[simp]

theorem SemiNormedGroup₁.zero_apply {V W : SemiNormedGroup₁} (x : ↥V) :

⇑0 x = 0

source

theorem SemiNormedGroup₁.is_zero_of_subsingleton (V : SemiNormedGroup₁) [subsingleton ↥V] :

category_theory.limits.is_zero V

source

@[protected, instance]

def SemiNormedGroup₁.has_zero_object :

category_theory.limits.has_zero_object SemiNormedGroup₁

source

theorem SemiNormedGroup₁.iso_isometry {V W : SemiNormedGroup₁} (i : V ≅ W) :

isometry ⇑(i.hom)

mathlib documentation

The category of seminormed groups #