English
For a manifold M and a smooth homomorphism φ between abelian Lie groups A and A', there is a left-composition morphism of the smooth sheaf from A to A'.
Русский
Для многообразия M и гладкой гомоморфизм φ между абелевыми группами A и A' существует морфизм левой композиции оболочки из A в A'.
LaTeX
$$compLeft (φ) (hφ) : smoothSheafCommGroup IM I M A ⟶ smoothSheafCommGroup IM I' M A'$$
Lean4
/-- The presheaf of smooth functions from `M` to `G`, for `G` a Lie group, as a presheaf of groups.
-/
@[to_additive /-- The presheaf of smooth functions from `M` to `G`, for `G` an additive Lie group,
as a presheaf of additive groups. -/
]
noncomputable def smoothPresheafGroup : TopCat.Presheaf GrpCat.{u} (TopCat.of M) :=
{ obj := fun U ↦ GrpCat.of ((smoothSheaf IM I M G).presheaf.obj U)
map := fun h ↦ GrpCat.ofHom <| ContMDiffMap.restrictMonoidHom IM I G <| CategoryTheory.leOfHom h.unop
map_id := fun _ ↦ rfl
map_comp := fun _ _ ↦ rfl }
