SemiNormedGroupCat₁.hom_ext
theorem SemiNormedGroupCat₁.hom_ext : ∀ {M N : SemiNormedGroupCat₁} (f g : M ⟶ N), ⇑f = ⇑g → f = g
This theorem states that for any two objects `M` and `N` in the category `SemiNormedGroupCat₁` (which is equipped with the category structure consisting only of the norm non-increasing maps), if two morphisms `f` and `g` from `M` to `N` are such that their underlying functions (obtained by applying the coercion to function, `⇑`) are equal, then the morphisms `f` and `g` themselves are equal. In other words, this expresses the principle that morphisms in `SemiNormedGroupCat₁` are determined by their action on elements.
More concisely: In the category of semi-normed groups `SemiNormedGroupCat₁`, two morphisms with equal underlying functions are equal.
|
SemiNormedGroupCat.ext
theorem SemiNormedGroupCat.ext : ∀ {M N : SemiNormedGroupCat} {f₁ f₂ : M ⟶ N}, (∀ (x : ↑M), f₁ x = f₂ x) → f₁ = f₂ := by
sorry
This theorem states that for any two objects `M` and `N` in the category of seminormed abelian groups, if we have two morphisms `f₁` and `f₂` from `M` to `N`, then `f₁` equals `f₂` if they are equal at every element of the underlying set of `M`. In other words, this theorem is saying that two bounded group homomorphisms between seminormed abelian groups are the same if they map every element of a seminormed abelian group to the same element in another seminormed abelian group.
More concisely: Given two bounded group homomorphisms between seminormed abelian groups, they are equal if and only if they map every element to the same image.
|
SemiNormedGroupCat₁.zero_apply
theorem SemiNormedGroupCat₁.zero_apply : ∀ {V W : SemiNormedGroupCat₁} (x : ↑V), 0 x = 0
The theorem `SemiNormedGroupCat₁.zero_apply` states that for any two objects `V` and `W` in the category `SemiNormedGroupCat₁` (i.e., a category whose objects are seminormed add commutative groups and whose morphisms are norm non-increasing maps), and for any element `x` from the underlying set of `V`, the zero map applied to `x` results in the zero element. In other words, within the context of `SemiNormedGroupCat₁`, the zero map always sends any element to zero.
More concisely: For any seminormed add commutative group `V` in `SemiNormedGroupCat₁` and any of its elements `x`, the zero map `0` applied to `x` equals the additive identity `0` of `V`.
|