English
For open sets U⊆V in N, restricting C^n-maps from V to U yields a monoid homomorphism ContMDiffMap.restrictMonoidHom I I' G h, which acts by composition with the inclusion map and preserves multiplication.
Русский
Для открытых подмножества U⊆V отображения C^n из V в G ограничиваются до U; это даёт моноид-гомоморфизм и сохраняет умножение.
LaTeX
$$$\text{For }U\subseteq V,\; h: U\to V,\;\; C^n(I,V;I',G)\to C^n(I,U;I',G),\; f\mapsto f\circ i_{h}$ является моноид-гомоморфизм.$$
Lean4
/-- For a Lie group `G` and open sets `U ⊆ V` in `N`, the 'restriction' group homomorphism from
`C^n⟮I, V; I', G⟯` to `C^n⟮I, U; I', G⟯`. -/
@[to_additive /-- For an additive Lie group `G` and open sets `U ⊆ V` in `N`, the 'restriction'
group homomorphism from `C^n⟮I, V; I', G⟯` to `C^n⟮I, U; I', G⟯`. -/
]
def restrictMonoidHom (G : Type*) [Monoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' n G]
{U V : Opens N} (h : U ≤ V) : C^n⟮I, V; I', G⟯ →* C^n⟮I, U; I', G⟯
where
toFun f := ⟨f ∘ Set.inclusion h, f.contMDiff.comp (contMDiff_inclusion h)⟩
map_one' := rfl
map_mul' _ _ := rfl
