English
For smooth homomorphism φ between abelian groups A and A', there is a left morphism of presheaves between smoothSheafCommGroup IM I M A and smoothSheafCommGroup IM I' M A'.
Русский
Для гладкой гомоморфизмы φ между абелевыми группами A и A' существует морфизм левой композиции между прешефами гладких групп.
LaTeX
$$compLeft (φ) (hφ) : smoothSheafCommGroup IM I M A ⟶ smoothSheafCommGroup IM I' M A'$$
Lean4
/-- For a manifold `M` and a smooth homomorphism `φ` between abelian Lie groups `A`, `A'`, the
'left-composition-by-`φ`' morphism of sheaves from `smoothSheafCommGroup IM I M A` to
`smoothSheafCommGroup IM I' M A'`. -/
@[to_additive /-- For a manifold `M` and a smooth homomorphism `φ` between abelian additive Lie
groups `A`, `A'`, the 'left-composition-by-`φ`' morphism of sheaves from
`smoothSheafAddCommGroup IM I M A` to `smoothSheafAddCommGroup IM I' M A'`. -/
]
noncomputable def compLeft (φ : A →* A') (hφ : ContMDiff I I' ∞ φ) :
smoothSheafCommGroup IM I M A ⟶ smoothSheafCommGroup IM I' M A' :=
CategoryTheory.Sheaf.Hom.mk <|
{ app := fun _ ↦ CommGrpCat.ofHom <| ContMDiffMap.compLeftMonoidHom _ _ φ hφ
naturality := fun _ _ _ ↦ rfl }
