English
For Opens N, a restriction homomorphism of C^n(I,V; I',R) exists when restricting to smaller opens via h: U ⊆ V, yielding a ring homomorphism that preserves the ring structure via the composed functions.
Русский
Существуют ограничения кольцевых отображений C^n(I,V;I',R) к меньших открытых подмножеств U⊆V, образующие кольцевой гомоморфизм.
LaTeX
$$$\text{restrictRingHom }(I,N) : C^n(I,V;I',R)\to C^n(I,U;I',R)\text{ for }U\le V$ is a ring homomorphism.$$
Lean4
/-- For a "`C^n` ring" `R` and open sets `U ⊆ V` in `N`, the "restriction" ring homomorphism from
`C^n⟮I, V; I', R⟯` to `C^n⟮I, U; I', R⟯`. -/
def restrictRingHom (R : Type*) [Ring R] [TopologicalSpace R] [ChartedSpace H' R] [ContMDiffRing I' n R] {U V : Opens N}
(h : U ≤ V) : C^n⟮I, V; I', R⟯ →+* C^n⟮I, U; I', R⟯ :=
{ ContMDiffMap.restrictMonoidHom I I' R h, ContMDiffMap.restrictAddMonoidHom I I' R h with
toFun := fun f => ⟨f ∘ Set.inclusion h, f.contMDiff.comp (contMDiff_inclusion h)⟩ }
