instAddCommGroupHom — Mathlib

English

For topological modules X,Y, the Hom-set (X ⟶ Y) inherits an additive commutative group structure via φ1 + φ2 := ofHom (φ1.hom + φ2.hom) and zero := ofHom 0, compatible with the category structure.

Русский

Для топологических модулей X, Y множество гомоморфизмов (X ⟶ Y) наследует аддитивную коммутативную группу: сумма φ1 + φ2 задаётся как ofHom(φ1.hom + φ2.hom), ноль — как ofHom 0; совместимо с категорной структурой.

LaTeX

$$$ (X \to Y) \text{ имеет структуру AddCommGroup} \\ (f,g) \mapsto \operatorname{ofHom}(f.\\hom + g.\\hom), \ 0 := \operatorname{ofHom}(0)$$$

Lean4

instance {X Y : TopModuleCat R} : AddCommGroup (X ⟶ Y)
    where
  add f g := ofHom (f.hom + g.hom)
  zero := ofHom 0
  __ := Equiv.addCommGroup CategoryTheory.ConcreteCategory.homEquiv

Похожие утверждения