English
Restricting a chart to its source s yields membership in the maximal atlas of the subtype s.
Русский
Ограничение чарта до источника s даёт принадлежность к максимальному атласу подпространства s.
LaTeX
$$e.subtypeRestr hs ∈ G.maximalAtlas s$$
Lean4
/-- Restricting a chart to its source `s ⊆ M` yields a chart in the maximal atlas of `s`. -/
theorem restriction_mem_maximalAtlas_subtype {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M)
(hs : Nonempty e.source) [HasGroupoid M G] [ClosedUnderRestriction G] :
let s := { carrier := e.source, is_open' := e.open_source : Opens M }
let t := { carrier := e.target, is_open' := e.open_target : Opens H }
∀ c' ∈ atlas H t, e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ c' ∈ G.maximalAtlas s :=
by
intro s t c' hc'
have : Nonempty t := nonempty_coe_sort.mpr (e.mapsTo.nonempty (nonempty_coe_sort.mp hs))
obtain ⟨x, hc'⟩ := Opens.chart_eq this hc'
rw [hc', (chartAt_self_eq)]
-- Our expression equals this chart, at least on its source.
rw [OpenPartialHomeomorph.subtypeRestr_def, OpenPartialHomeomorph.trans_refl]
let goal := e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ (t.openPartialHomeomorphSubtypeCoe this)
have : goal ≈ e.subtypeRestr (s := s) hs :=
(goal.eqOnSource_iff (e.subtypeRestr (s := s) hs)).mpr
⟨by
simp only [trans_toPartialEquiv, PartialEquiv.trans_source, Homeomorph.toOpenPartialHomeomorph_source,
toFun_eq_coe, Homeomorph.toOpenPartialHomeomorph_apply, Opens.openPartialHomeomorphSubtypeCoe_source,
preimage_univ, inter_self, subtypeRestr_source, goal, s]
exact Subtype.coe_preimage_self _ |>.symm, by intro _ _; rfl⟩
exact G.mem_maximalAtlas_of_eqOnSource (M := s) this (G.subtypeRestr_mem_maximalAtlas he hs)
