English
Let I be a boundaryless charted space modeled on a complete vector space. An open partial homeomorphism e belongs to the analytic groupoid of I precisely when the maps transported by I, namely I ∘ e ∘ I^{-1} and I ∘ e^{-1} ∘ I^{-1}, are analytic on neighborhoods of the corresponding images.
Русский
Пусть пространства с графами без границ имеют модель I, тождественно совместимую с полным векторным пространством. Тогда частичное открытое гомоморфизмe e принадлежит аналитному групоиоду I тогда и только тогда, когда соответствующие отображения, полученные путём транспонирования через I, аналитичны на окрестностях соответствующих образов (I ∘ e ∘ I^{-1} и I ∘ e^{-1} ∘ I^{-1}).
LaTeX
$$$e \in analyticGroupoid(I) \iff AnalyticOnNhd 𝕜 (I \circ e \circ I^{-1}) (I '' source(e)) \land AnalyticOnNhd 𝕜 (I \circ e^{-1} \circ I^{-1}) (I '' target(e))$$$
Lean4
/-- The analytic groupoid on a boundaryless charted space modeled on a complete vector space
consists of the open partial homeomorphisms which are analytic and have analytic inverse. -/
theorem mem_analyticGroupoid_of_boundaryless [I.Boundaryless] (e : OpenPartialHomeomorph H H) :
e ∈ analyticGroupoid I ↔
AnalyticOnNhd 𝕜 (I ∘ e ∘ I.symm) (I '' e.source) ∧ AnalyticOnNhd 𝕜 (I ∘ e.symm ∘ I.symm) (I '' e.target) :=
by
simp only [mem_analyticGroupoid, I.range_eq_univ, inter_univ, I.image_eq]
rw [IsOpen.analyticOn_iff_analyticOnNhd, IsOpen.analyticOn_iff_analyticOnNhd]
· exact I.continuous_symm.isOpen_preimage _ e.open_target
· exact I.continuous_symm.isOpen_preimage _ e.open_source
