English
Given a monoid homomorphism φ: G'→G'' and a contMDiff map hφ: ContMDiff I' I'' n φ, the map sending f to φ∘f defines a monoid homomorphism between the corresponding C^n-maps spaces.
Русский
Дано гомоморфизм моноидов φ: G'→G'' и гладкое отображение hφ, тогда отображение f↦φ∘f задаёт моноид-гомоморфизм между соответствующими пространствами C^n-отображений.
LaTeX
$$$\text{If }φ:G'\to G''\text{ is a monoid homomorphism and }hφ:\ ContMDiff I' I'' n φ,\;\;
(f\mapsto φ\circ f)\;:\; C^n(I,N;I',G')\to C^n(I,N;I'',G'')$ is a monoid homomorphism.$$
Lean4
/-- For a manifold `N` and a `C^n` homomorphism `φ` between Lie groups `G'`, `G''`, the
'left-composition-by-`φ`' group homomorphism from `C^n⟮I, N; I', G'⟯` to `C^n⟮I, N; I'', G''⟯`. -/
@[to_additive /-- For a manifold `N` and a `C^n` homomorphism `φ` between additive Lie groups `G'`,
`G''`, the 'left-composition-by-`φ`' group homomorphism from `C^n⟮I, N; I', G'⟯` to
`C^n⟮I, N; I'', G''⟯`. -/
]
def compLeftMonoidHom {G' : Type*} [Monoid G'] [TopologicalSpace G'] [ChartedSpace H' G'] [ContMDiffMul I' n G']
{G'' : Type*} [Monoid G''] [TopologicalSpace G''] [ChartedSpace H'' G''] [ContMDiffMul I'' n G''] (φ : G' →* G'')
(hφ : ContMDiff I' I'' n φ) : C^n⟮I, N; I', G'⟯ →* C^n⟮I, N; I'', G''⟯
where
toFun f := ⟨φ ∘ f, hφ.comp f.contMDiff⟩
map_one' := by ext; change φ 1 = 1; simp
map_mul' f g := by ext x; change φ (f x * g x) = φ (f x) * φ (g x); simp
