English
The singleton charted space again carries HasGroupoid with closure under restriction.
Русский
Единичное чартовое пространство снова поддерживает HasGroupoid с замыканием на ограничение.
LaTeX
$$singleton_hasGroupoid$$
Lean4
/-- Restricting a chart of `M` to an open subset `s` yields a chart in the maximal atlas of `s`.
NB. We cannot deduce membership in `atlas H s` in general: by definition, this atlas contains
precisely the restriction of each preferred chart at `x ∈ s` --- whereas `atlas H M`
can contain more charts than these. -/
theorem subtypeRestr_mem_maximalAtlas {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) {s : Opens M}
(hs : Nonempty s) {G : StructureGroupoid H} [HasGroupoid M G] [ClosedUnderRestriction G] :
e.subtypeRestr hs ∈ G.maximalAtlas s := by
intro e' he'
obtain ⟨x, this⟩ := Opens.chart_eq hs he'
rw [this]
-- The transition functions between the unrestricted charts lie in the groupoid,
-- the transition functions of the restriction are the restriction of the transition function.
exact ⟨G.trans_restricted he (chart_mem_atlas H (x : M)) hs, G.trans_restricted (chart_mem_atlas H (x : M)) he hs⟩
