English
For abelian Lie group A, the stalk ((smoothSheaf IM I M A).presheaf.obj U) is a commutative group.
Русский
Для абелевой группы A, сталк ((smoothSheaf IM I M A).presheaf.obj U) образует коммутативную группу.
LaTeX
$$CommGroup ((smoothSheaf IM I M A).presheaf.obj U)$$
Lean4
/-- The sheaf of smooth functions from `M` to `A`, for `A` an abelian Lie group, as a
sheaf of abelian groups. -/
@[to_additive /-- The sheaf of smooth functions from `M` to
`A`, for `A` an abelian additive Lie group, as a sheaf of abelian additive groups. -/
]
noncomputable def smoothSheafCommGroup : TopCat.Sheaf CommGrpCat.{u} (TopCat.of M) :=
{ val := smoothPresheafCommGroup IM I M A
cond := by
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget CommGrpCat)]
exact CategoryTheory.Sheaf.cond (smoothSheaf IM I M A) }
