English
Each chart yields a corresponding Structomorph between subtype charts.
Русский
Каждый чарт порождает соответствующий Structomorph между подтипами чартов.
LaTeX
$$toStructomorph_repeat$$
Lean4
/-- Each chart of a charted space is a structomorphism between its source and target. -/
def toStructomorph {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) [HasGroupoid M G] [ClosedUnderRestriction G] :
let s : Opens M := { carrier := e.source, is_open' := e.open_source }
let t : Opens H := { carrier := e.target, is_open' := e.open_target }
Structomorph G s t :=
by
intro s t
by_cases h : Nonempty e.source
·
exact
{ e.toHomeomorphSourceTarget with
mem_groupoid :=
-- The atlas of H on itself has only one chart, hence c' is the inclusion.
-- Then, compatibility of `G` *almost* yields our claim --- except that `e` is a chart
-- on `M` and `c` is one on `s`: we need to show that restricting `e` to `s` and composing
-- with `c'` yields a chart in the maximal atlas of `s`.
fun c c' hc hc' ↦
G.compatible_of_mem_maximalAtlas (G.subset_maximalAtlas hc)
(G.restriction_mem_maximalAtlas_subtype he h c' hc') }
· push_neg at h
have : IsEmpty t :=
isEmpty_coe_sort.mpr (by convert e.image_source_eq_target ▸ image_eq_empty.mpr (isEmpty_coe_sort.mp h))
exact
{ Homeomorph.empty with
-- `c'` cannot exist: it would be the restriction of `chartAt H x` at some `x ∈ t`.
mem_groupoid := fun _ c' _ ⟨_, ⟨x, _⟩, _⟩ ↦ (this.false x).elim }
