English
The left composition morphism is defined by composing smooth maps pointwise with φ, preserving the presheaf structure.
Русский
Левая композиция определяется композициями гладких отображений по точкам с φ и сохраняет структуру прешефа.
LaTeX
$$compLeft (φ) (hφ) = ...$$
Lean4
/-- The sheaf of smooth functions from `M` to `G`, for `G` a Lie group, as a sheaf of
groups. -/
@[to_additive /-- The sheaf of smooth functions from `M` to `G`, for `G` an additive Lie group, as a
sheaf of additive groups. -/
]
noncomputable def smoothSheafGroup : TopCat.Sheaf GrpCat.{u} (TopCat.of M) :=
{ val := smoothPresheafGroup IM I M G
cond := by
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget GrpCat)]
exact CategoryTheory.Sheaf.cond (smoothSheaf IM I M G) }
