English
Let G be a topological group and consider the class of C^n-smooth maps f from a manifold N into G. The set of such maps is closed under pointwise multiplication, forming a semigroup; if G is a monoid with identity 1_G, this set becomes a monoid with the pointwise identity map (x ↦ 1_G). If G is a commutative monoid, the structure is a commutative monoid. For any natural k, the k-th power f^k is defined by (f^k)(x) = f(x)^k for all x ∈ N, and is again a C^n-smooth map. Moreover, the operation of taking the k-th power is compatible with the differentiable structure, i.e., the map f ↦ f^k is C^n-smooth in the appropriate sense.
Русский
Пусть G — топологическая группа, и рассматривается множество функций C^n(I,N;I',G) от многообразия N в группу G. Это множество замкнуто при точечном произведении и образует полугруппу; если G — моноид, то есть имеется единичный элемент 1_G, данное множество образует моноид. Если G коммутативен, то образуется коммутативный моноид. Для каждого натурального k определим f^k по (f^k)(x) = f(x)^k; f^k снова принадлежит C^n(I,N;I',G). Процесс взятия степени совместим с дифференцируемой структурой и является C^n-смутным по соответствующим условиям.
LaTeX
$$$f^k\in C^n\langle I,N; I',G\rangle ,\quad (f^k)(x)=(f(x))^k \text{ for all } x\in N;\quad f\mapsto f^k\text{ is a }C^n\text{-map.}$$$
Lean4
@[to_additive existing]
instance instPow {G : Type*} [Monoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' n G] :
Pow C^n⟮I, N; I', G⟯ ℕ where pow f n := ⟨(f : N → G) ^ n, (contMDiff_pow n).comp f.contMDiff⟩
